SCP 4 : Verification of Protocols
| Parameterized cache coherence protocols: |
Parameterized protocols for multithreaded Java programs: |
More parameterized protocols: |
It is not a good idea to see this Web-page in a small window.
On specification of the cache coherence protocols: G. Delzanno specifies a class of parameterized cache coherence protocols with global correctness conditions in terms of Extended Finite State Machines (EFSM), which are essentially transition systems with data variables ranging over non-negative numbers. EFSM-transitions are linear transformations with the guards expressed as linear constraints. We find it convenient to consider such models as non-deterministic pebble games, where variables and their values are represented by locations (baskets) and numbers of pebbles in baskets, respectively. Then evolution of EFSM can be thought of as non-deterministic movement of pebbles between baskets and safety properties of the protocols are expressed as systems of linear inequalities imposed on the numbers of the pebbles in the baskets.
As an example consider MESI protocol given below.
Here modified, exclusive, shared, invalid are non-negative integer variables of EFSM model, which
represent counting abstraction of original parameterised automata model: the names denote various states
of the automaton (cache) and the values of the variables keep track of the number of automata in corresponding
states. The rules (rh)-(wm) define the dynamic of EFSM model. Starting with some initial evaluation of
the variables, the system may apply non-deterministically any of the rules. In the case the quard of a rule
(its left-hand part) is satisfied in a current state (evaluation of all variables, i.e integer vector), the
update expressed by the right-hand side of the rule is executed. Primed variable names are used in updates
to denote updated values.
| Top | Bottom | REFAL encoding | Result of supercompilation |
Example #1 (Synapse N+1):
(rh)
dirty + valid ≥ 1 —> .
|
(rm)
invalid ≥ 1 —>
|
| dirty' = 0, valid' = valid + 1, invalid' = invalid + dirty - 1. |
(wh1)
dirty ≥ 1 —> .
|
(wh2)
valid ≥ 1 —>
|
| valid' = 0, dirty' = 1, invalid' = invalid + dirty + valid - 1. |
(wm)
invalid ≥ 1 —>
|
| valid' = 0, dirty' = 1, invalid' = invalid + dirty + valid - 1. |
- The parameterized initial configuration is expressed as:
invalid ≥ 1, dirty = 0, valid = 0 - The potentially unsafe states:
(1)invalid ≥ 0, dirty ≥ 1, valid ≥ 1(2)invalid ≥ 0, dirty ≥ 2, valid ≥ 0
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #2 (MSI):
The description of the parameterized MSI protocol is taken from the paper by E.A. Emerson and V. Kahlon.
(PrWr1)
invalid ≥ 1 —>
invalid' = invalid + modified + shared - 1,
modified' = 1, shared' = 0.
|
(PrWr2)
shared ≥ 1 —>
invalid' = invalid + modified + shared - 1,
modified' = 1, shared' = 0.
|
(PrRd)
invalid ≥ 1 —>
invalid' = invalid - 1,
modified' = 0, shared' = 1 + shared + modified.
|
(PrT)
shared ≥ 1, modified ≥ 1 —> .
|
- The parameterized initial configuration is expressed as:
invalid ≥ 1, modified = 0, shared = 0 - The potentially unsafe states:
(1)invalid ≥ 0, modified ≥ 1, shared ≥ 1(2)invalid ≥ 0, modified ≥ 2, shared ≥ 0
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #3 (MOSI):
The description of the parameterized MOSI protocol is taken from the Ph.D. thesis by M.M.K. Martin.
(rh)
modified + owned + shared ≥ 1 —> .
|
(rm)
invalid ≥ 1 —>
|
| invalid' = invalid - 1, modified' = 0, |
| shared' = shared + 1, owned' = modified + owned. |
(wO)
owned ≥ 1 —>
|
| shared' = 0, owned' = 0, modified' = 1, |
| invalid' = owned - 1 + shared + modified + invalid. |
(wI)
invalid ≥ 1 —>
|
| shared' = 0, owned' = 0, modified' = 1, |
| invalid' = owned + shared + modified + invalid - 1. |
(wS)
shared ≥ 1 —>
|
| shared' = 0, owned' = 0, modified' = 1, |
| invalid' = owned + shared - 1 + modified + invalid. |
(se)
shared ≥ 1 —>
|
| shared' = shared - 1, invalid' = invalid + 1. |
(wbM)
modified ≥ 1 —>
|
| modified' = modified - 1, invalid' = invalid + 1. |
(wbO)
owned ≥ 1 —>
|
| owned' = owned - 1, invalid' = invalid + 1. |
- The parameterized initial configuration is expressed as:
invalid ≥ 1, owned = 0, shared = 0, modified = 0 - The potentially unsafe states:
(1)invalid ≥ 0, shared ≥ 0, owned ≥ 2, modified ≥ 0(2)invalid ≥ 0, shared ≥ 0, owned ≥ 0, modified ≥ 2(3)invalid ≥ 0, shared ≥ 1, owned ≥ 0, modified ≥ 1
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #4 (MESI):
(rh)
modified + shared + exclusive ≥ 1 —> .
|
(rm)
invalid ≥ 1 —>
|
| invalid' = invalid - 1, exclusive' = 0, modified' = 0, |
| shared' = shared + exclusive + modified + 1. |
(wh1)
modified ≥ 1 —> .
|
(wh2)
exclusive ≥ 1 —>
|
| exclusive' = exclusive - 1, modified' = modified + 1. |
(wh3)
shared ≥ 1 —>
|
| shared' = 0, exclusive' = 1, modified' = 0, |
| invalid' = invalid + modified + exclusive + shared - 1. |
(wm)
invalid ≥ 1 —>
|
| shared' = 0, exclusive' = 1, modified' = 0, |
| invalid' = invalid + modified + exclusive + shared - 1. |
- The parameterized initial configuration is expressed as:
invalid ≥ 1, exclusive = 0, shared = 0, modified = 0 - The potentially unsafe states:
(1)invalid ≥ 0, exclusive ≥ 0, shared ≥ 1, modified ≥ 1(2)invalid ≥ 0, exclusive ≥ 0, shared ≥ 0, modified ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #5 (MOESI):
(rh)
modified + owned + shared + exclusive ≥ 1 —> .
|
(rm)
invalid ≥ 1 —>
|
| invalid' = invalid - 1, exclusive' = 0, modified' = 0, |
| shared' = shared + exclusive + 1, owned' = owned + modified. |
(wh1)
modified ≥ 1 —> .
|
(wh2)
exclusive ≥ 1 —>
|
| exclusive' = exclusive - 1, modified' = modified + 1. |
(wh3)
shared + owned ≥ 1 —>
|
| shared' = 0, exclusive' = 1, modified' = 0, owned' = 0, |
| invalid' = invalid + modified + exclusive + shared + owned - 1. |
(wm)
invalid ≥ 1 —>
|
| shared' = 0, exclusive' = 1, modified' = 0, owned' = 0, |
| invalid' = invalid + modified + exclusive + shared + owned - 1. |
- The parameterized initial configuration is expressed as:
invalid ≥ 1, exclusive = 0, shared = 0, modified = 0, owned = 0 - The potentially unsafe states:
(1)exclusive + shared + owned ≥ 1, modified ≥ 1(2)exclusive ≥ 1, shared + owned ≥ 1(3)modified ≥ 2(4)exclusive ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #6 (The University of Illinois):
(r1)
dirty + shared + exclusive ≥ 1 —> .
|
(r2)
invalid ≥ 1, dirty = 0, shared = 0, exclusive = 0 —>
|
| invalid' = invalid - 1, exclusive' = exclusive + 1. |
(r3)
invalid ≥ 1, dirty ≥ 1 —>
|
| invalid' = invalid - 1, dirty' = dirty - 1, shared' = shared + 2. |
(r4)
invalid ≥ 1, shared + exclusive ≥ 1 —>
|
| invalid' = invalid - 1, shared' = shared + exclusive + 1, exclusive' = 0. |
(r5)
dirty ≥ 1 —> .
|
(r6)
exclusive ≥ 1 —> exclusive' = exclusive - 1, dirty' = dirty + 1.
|
(r7)
shared ≥ 1 —>
|
| shared' = 0, invalid' = invalid + shared - 1, dirty' = dirty + 1. |
(r8)
invalid ≥ 1 —>
invalid' = invalid + exclusive + dirty + shared - 1,
|
| exclusive' = 0, shared' = 0, dirty' = 1. |
(r9)
dirty ≥ 1 —> dirty' = dirty - 1, invalid' = invalid + 1.
|
(r10)
shared ≥ 1 —> shared' = shared - 1, invalid' = invalid + 1.
|
(r11)
exclusive ≥ 1 —> exclusive' = exclusive - 1, invalid' = invalid + 1.
|
- The parameterized initial configuration is expressed as:
invalid ≥ 1, exclusive = 0, dirty = 0, shared = 0 - The potentially unsafe states:
(1)invalid ≥ 0, exclusive ≥ 0, dirty ≥ 1, shared ≥ 1(2)invalid ≥ 0, exclusive ≥ 0, dirty ≥ 2, shared ≥ 0
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #7 (Berkley):
(rm)
invalid ≥ 1 —>
|
| invalid' = invalid - 1, unowned' = unowned + 1, exclusive' = 0, |
| non_exclusive' = non_exclusive + exclusive. |
(rh)
non_exclusive + exclusive + unowned ≥ 1 —> .
|
(wm)
invalid ≥ 1 —>
|
| non_exclusive' = 0, unowned' = 0, exclusive' = 1, |
| invalid' = invalid + exclusive + non_exclusive + unowned - 1. |
(wh1)
non_exclusive + unowned ≥ 1 —>
|
| non_exclusive' = 0, unowned' = 0, exclusive' = exclusive + 1, |
| invalid' = invalid + non_exclusive + unowned - 1. |
(wh2)
exclusive ≥ 1 —> .
|
- The parameterized initial configuration is expressed as:
invalid ≥ 1, non_exclusive = 0, unowned = 0, exclusive = 0 - The potentially unsafe states:
(1)exclusive ≥ 1, unowned + non_exclusive ≥ 1(2)exclusive ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #8 (DEC Firefly):
(rh)
dirty + shared + exclusive ≥ 1 —> .
|
(rm1)
invalid ≥ 1, dirty = 0, shared = 0, exclusive = 0 —>
|
| invalid' = invalid - 1, exclusive' = exclusive + 1. |
(rm2)
invalid ≥ 1, dirty ≥ 1 —>
|
| invalid' = invalid - 1, dirty' = dirty - 1, shared' = shared + 2. |
(rm3)
invalid ≥ 1, shared + exclusive ≥ 1 —>
|
| invalid' = invalid - 1, shared' = shared + exclusive + 1, exclusive' = 0. |
(wh1)
dirty ≥ 1 —> .
|
(wh2)
exclusive ≥ 1 —> exclusive' = exclusive - 1, dirty' = dirty + 1.
|
(wh3)
shared = 1 —>
|
| shared' = shared - 1, exclusive' = exclusive + 1. |
(wh4)
shared ≥ 2 —> .
|
(wm)
invalid ≥ 1 —> invalid' = invalid + exclusive + dirty + shared - 1,
|
| exclusive' = 0, shared' = 0, dirty' = 1. |
- The parameterized initial configuration is expressed as:
invalid ≥ 1, exclusive = 0, shared = 0, dirty = 0 - The potentially unsafe states:
(1)dirty ≥ 1, shared + exclusive ≥ 1(2)exclusive ≥ 2(3)dirty ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #9 (IEEE Futurebus+):
(r1)
sharedU + exclusiveU + exclusiveM ≥ 1 —> .
|
(r2)
invalid ≥ 1, pendingW = 0 —>
|
| invalid' = invalid - 1, pendingR' = 1 + pendingR, |
| pendingEMR' = pendingEMR + exclusiveM, pendingSU' = pendingSU + sharedU + exclusiveU, |
| sharedU' = exclusiveU' = exclusiveM' = 0. |
(r3)
pendingEMR ≥ 1 —>
|
| pendingEMR' = pendingEMR - 1, sharedU' = 1 + sharedU + pendingR, pendingR' = 0. |
(r4)
pendingSU ≥ 1 —>
|
| sharedU' = sharedU + pendingR + pendingSU, pendingR' = pendingSU' = 0. |
(r5)
pendingR ≥ 2, pendingSU = 0, pendingEMR = 0 —>
|
| sharedU' = sharedU + pendingR, pendingR' = 0. |
(r6)
pendingR = 1, pendingSU = 0, pendingEMR = 0 —>
|
| pendingR' = pendingR - 1, exclusiveU' = 1 + exclusiveU. |
(wm1)
invalid ≥ 1, pendingW = 0 —>
|
| pendingW' = 1 + pendingW, exclusiveEMW' = exclusiveEMW + exclusiveM, |
| sharedU' = exclusiveU' = exclusiveM' = 0, pendingR' = pendingEMR' = pendingSU' = 0, |
| invalid' = invalid + exclusiveU + sharedU + pendingSU + pendingR + pendingEMR - 1. |
(wm2)
pendingEMW ≥ 1 —>
|
| pendingEMW' = pendingEMW - 1, invalid' = 1 + invalid, |
| exclusiveM' = exclusiveM + pendingW, pendingW' = 0. |
(wm3)
pendingEMW = 0 —>
|
| exclusiveM' = exclusiveM + pendingW, pendingW' = 0. |
(wh1)
exclusiveM ≥ 1 —> .
|
(wh2)
exclusiveU ≥ 1 —>
|
| exclusiveU' = exclusiveU - 1, exclusiveM' = 1 + exclusiveM. |
(wh3)
sharedU ≥ 1 —>
|
| invalid' = invalid + sharedU - 1, exclusiveM' = 1 + exclusiveM, sharedU' = 0. |
- The parameterized initial configuration is expressed as:
invalid ≥ 1, sharedU = 0, exclusiveU = 0, exclusiveM = 0,
pendingR = 0, pendingW = 0, pendingEMR = 0, pendingEMW = 0, pendingSU = 0 - The potentially unsafe states:
(1)sharedU ≥ 1, exclusiveU + exclusiveM ≥ 1(2)exclusiveU + exclusiveM ≥ 2(3)pendingR ≥ 1, pendingW ≥ 1(4)pendingW ≥ 2
Example #10 (Xerox PARC Dragon):
(A) An incorrect specification given by G. Delzanno in [2].
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
(rh)
dirty + shared_clean + exclusive + shared_dirty ≥ 1 —> .
|
(rm1)
invalid ≥ 1, dirty = 0, shared_clean = 0,
shared_dirty = 0, exclusive = 0 —>
|
| invalid' = invalid - 1, exclusive' = exclusive + 1. |
(rm2)
invalid ≥ 1,
dirty + shared_clean + exclusive + shared_dirty ≥ 1 —>
|
| invalid' = invalid - 1, dirty' = 0, exclusive' = 0, |
| shared_dirty' = shared_dirty + dirty, shared_clean' = shared_clean + exclusive + 1. |
(wm1)
invalid ≥ 1, dirty = 0, shared_clean = 0, exclusive = 0,
shared_dirty = 0 —>
|
| invalid' = invalid - 1, dirty' = dirty + 1. |
(wm2)
|
|
|
|
|
(wh1)
|
(wh2)
|
(wh3)
|
(wh4)
|
(wh5)
shared_dirty + shared_clean ≥ 2 —>
|
|
|
- The parameterized initial configuration is expressed as:
invalid ≥ 1, shared_clean = 0, shared_dirty = 0, dirty = 0, exclusive = 0 - The potentially unsafe states:
(1)dirty ≥ 1, exclusive + shared_clean + shared_dirty ≥ 1(2)exclusive ≥ 1, shared_clean + shared_dirty ≥ 1(3)dirty ≥ 2(4)exclusive ≥ 2
(B) The correct specification given by G. Delzanno [3].
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation | Structure of the automatic proof |
(rh)
dirty + shared_clean + exclusive + shared_dirty ≥ 1 —> .
|
(rm1)
invalid ≥ 1, dirty = 0, shared_clean = 0,
shared_dirty = 0, exclusive = 0 —>
|
| invalid' = invalid - 1, exclusive' = exclusive + 1. |
(rm2)
invalid ≥ 1,
dirty + shared_clean + exclusive + shared_dirty ≥ 1 —>
|
| invalid' = invalid - 1, dirty' = 0, exclusive' = 0, |
| shared_dirty' = shared_dirty + dirty, shared_clean' = shared_clean + exclusive + 1. |
(wm1)
invalid ≥ 1, dirty = 0, shared_clean = 0, exclusive = 0,
shared_dirty = 0 —>
|
| invalid' = invalid - 1, dirty' = dirty + 1. |
(wm2)
invalid ≥ 1, dirty + shared_clean + exclusive + shared_dirty ≥ 1 —>
|
| invalid' = invalid - 1, exclusive' = 0, dirty' = 0, |
| shared_clean' = shared_clean + exclusive + shared_dirty + dirty. |
(wh1)
dirty ≥ 1 —>
|
| invalid' = 1 + invalid, dirty' = dirty - 1. |
(wh2)
shared_clean ≥ 1 —>
invalid' = 1 + invalid, shared_clean' = shared_clean - 1.
|
(wh3)
shared_dirty ≥ 1 —>
invalid' = 1 + invalid, shared_dirty' = shared_dirty - 1.
|
(wh4)
exclusive ≥ 1 —>
invalid' = 1 + invalid, exclusive' = exclusive - 1.
|
- The parameterized initial configuration is expressed as:
invalid ≥ 1, shared_clean = 0, shared_dirty = 0, dirty = 0, exclusive = 0 - The potentially unsafe states:
(1)dirty ≥ 1, exclusive + shared_clean + shared_dirty ≥ 1(2)exclusive ≥ 1, shared_clean + shared_dirty ≥ 1(3)dirty ≥ 2(4)exclusive ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #11 (Java Meta-Locking Algorithm):
The description of the parameterized Java Meta-Locking algorithm is taken from the paper by Abhik Roychoudhury, I.V. Ramakrishnan.
(get_fast)
obj_trans_not_busy = TRUE,
idle ≥ 1 —>
|
| obj_trans_not_busy' = FALSE, busy' = 0, idle' = idle - 1, owner' = 1 + owner. |
(put_fast)
obj_trans_not_busy = FALSE, busy = 0,
owner ≥ 1 —>
|
| obj_trans_not_busy' = TRUE, idle' = 1 + idle, owner' = owner - 1. |
(get_slow)
obj_trans_not_busy = FALSE,
idle ≥ 1 —>
|
| busy' = 1 + busy, idle' = idle - 1, handin' = 1 + handin. |
(put_slow)
obj_trans_not_busy = FALSE,
busy ≥ 1, owner ≥ 1 —>
|
| busy' = busy - 1, owner' = owner - 1, handout' = 1 + handout. |
(request)
race = H0,
handin ≥ 1 —>
|
| race' = H1, handin' = handin - 1, wait' = 1 + wait. |
(request)
race = H2,
handin ≥ 1 —>
|
| race' = H3, handin' = handin - 1, wait' = 1 + wait. |
(release)
race = H0,
handout ≥ 1 —>
|
| race' = H2, handout' = handout - 1, idle' = 1 + idle. |
(release)
race = H1,
handout ≥ 1 —>
|
| race' = H3, handout' = handout - 1, idle' = 1 + idle. |
(go)
race = H3,
wait ≥ 1 —>
|
| owner' = 1 + owner, wait' = wait - 1. |
- The parameterized initial configuration is expressed as:
obj_trans_not_busy = TRUE, race = H0, idle ≥ 0, owner = 0, handin = 0, handout = 0, wait = 0 - The potentially unsafe states:
(1)owner + handout ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #12 (Reader-Writer protocol):
The description of the parameterized Reader-Writer protocol is taken from the paper by Laurent Fribourg.
(r1)
x2 ≥ 1, x4 = 0, x7 ≥ 1 —>
x2' = x2 - 1, x3' = 1 + x3.
|
(r2)
x2 ≥ 1, x6 ≥ 1 —>
x4' = 1 + x4.
|
(r3)
x3 ≥ 1 —>
x2' = 1 + x2, x5' = 1 + x5.
|
(r4)
x4 ≥ 1 —>
x5' = 1 + x5.
|
(r5)
x5 ≥ 1 —>
x6' = 1 + x6.
|
(r6)
x5 ≥ 1 —>
x7' = 1 + x7.
|
- The parameterized initial configuration is expressed as:
x2 = 1, x3 = 0, x4 = 0, x5 ≥ 0, x6 = 0, x7 = 0 - The potentially unsafe states:
(1)x3 ≥ 1, x4 ≥ 1
Example #13 (Steve German's directory-based consistency protocol):
The description of the parameterized Steve German's directory-based consistency protocol is taken from the paper by Delzanno G. and Bultan T..
Model I
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
(reqS)
server = IDLE,
null ≥ 1 —>
|
| server' = SERV_S, null' = null - 1, wait_s' = 1 + wait_s. |
(reqE1)
server = IDLE,
null ≥ 1 —>
|
| server' = SERV_E, null' = null - 1, wait_e' = 1 + wait_e. |
(reqE2)
server = IDLE,
shared ≥ 1 —>
|
| server' = SERV_E, shared' = shared - 1, wait_e' = 1 + wait_e. |
(inv)
server = SERV_S, bool = YES,
exclusive ≥ 1 —>
|
| server' = GRANT_S, bool' = NO, |
| exclusive' = exclusive - 1, null' = 1 + null. |
(nonex1)
server = SERV_S, bool = NO —>
server' = GRANT_S.
|
(invS)
server = SERV_E —>
|
| server' = INV_E, null' = null + shared, shared' = 0. |
(invE)
server = INV_E, bool = YES,
exclusive ≥ 1 —>
|
| server' = GRANT_E, bool' = NO, |
| exclusive' = exclusive - 1, null' = 1 + null. |
(nonex2)
server = INV_E, bool = NO —>
server' = GRANT_E.
|
(grantS)
server = GRANT_S,
wait_s ≥ 1 —>
|
| server' = IDLE, wait_s' = wait_s - 1, shared' = 1 + shared. |
(grantE)
server = GRANT_E,
wait_e ≥ 1 —>
|
| server' = IDLE, bool' = YES, |
| wait_e' = wait_e - 1, exclusive' = 1 + exclusive. |
(servG)
server = SERV_E,
shared = 0, exclusive = 0 —>
|
| server' = GRANT_E. |
(ee1)
server = SERV_E,
shared ≥ 1 —>
null' = 1 + null, shared' = shared - 1.
|
(ee2)
server = SERV_E,
exclusive ≥ 1 —>
|
| bool' = NO, null' = 1 + null, exclusive' = exclusive - 1. |
- The parameterized initial configuration is expressed as:
server = IDLE, bool = NO, null ≥ 1, wait_s = 0, shared = 0, wait_e = 0, exclusive = 0 - The potentially unsafe states:
(1)shared ≥ 1, exclusive ≥ 1(2)exclusive ≥ 2
Model B
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
(reqS)
server = IDLE,
null ≥ 1 —>
|
| server' = SERV_S, null' = null - 1, wait_s' = 1 + wait_s. |
(reqE1)
server = IDLE,
null ≥ 1 —>
|
| server' = SERV_E, null' = null - 1, wait_e' = 1 + wait_e. |
(reqE2)
server = IDLE,
shared ≥ 1 —>
|
| server' = SERV_E, shared' = shared - 1, wait_e' = 1 + wait_e. |
(inv)
server = SERV_S, bool = YES,
exclusive ≥ 1 —>
|
| server' = GRANT_S, bool' = NO, |
| exclusive' = exclusive - 1, null' = 1 + null. |
(nonex1)
server = SERV_S, bool = NO —>
server' = GRANT_S.
|
(invS)
server = SERV_E —>
|
| server' = INV_E, null' = null + shared, shared' = 0. |
(invE)
server = INV_E, bool = YES,
exclusive ≥ 1 —>
|
| server' = GRANT_E, bool' = NO, |
| exclusive' = exclusive - 1, null' = 1 + null. |
(nonex2)
server = INV_E, bool = NO —>
server' = GRANT_E.
|
(grantS)
server = GRANT_S,
wait_s ≥ 1 —>
|
| server' = IDLE, wait_s' = wait_s - 1, shared' = 1 + shared. |
(grantE)
server = GRANT_E,
wait_e ≥ 1 —>
|
| server' = IDLE, bool' = YES, |
| wait_e' = wait_e - 1, exclusive' = 1 + exclusive. |
- The parameterized initial configuration is expressed as:
server = IDLE, bool = NO, null ≥ 1, wait_s = 0, shared = 0, wait_e = 0, exclusive = 0 - The potentially unsafe states:
(1)shared ≥ 1, exclusive ≥ 1(2)exclusive ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #14 (Load Balancing Monitor protocol):
The description of the parameterized Load Balancing Monitor protocol
is taken
from the Web-page by Delzanno G.
Here the third assignment in the case (r3) means a non-deterministic
partition of the right part high + low + use
over the variables high', low' of the left part.
(r1)
idle ≥ 1, req ≥ 1 —>
req' = req - 1, use' = 1 + use.
|
(r2)
idle ≥ 1, use ≥ 1 —>
req' = 1 + req, use' = use - 1.
|
(r3)
idle ≥ 1 —>
|
| idle' = idle - 1, busy' = 1 + busy, |
| high' + low' = high + low + use, |
| high' ≥ high, use' = 0. |
(r4)
busy ≥ 1 —>
|
| idle' = 1 + idle, busy' = busy - 1, |
| req' = req + low, use' = use + high, |
| high' = 0, low' = 0. |
- The parameterized initial configuration is expressed as:
idle = 1, busy = 0, req ≥ 0, use = 0, high = 0, low = 0 - The potentially unsafe states:
(1)busy ≥ 1, use ≥ 1
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #15 (Data Race Free Synchronization Model):
The description of the parameterized Data Race Free Synchronization Model is taken from the Web-page by Delzanno G. after F.Pong and M. Dubois "Formal Verification of Delayed Consistency Protocols", IPPS96.
(r1)
out ≥ 1, cs = 0, scs = 0 —>
out' = out - 1, cs' = 1.
|
(r2)
out ≥ 1, cs = 0 —>
out' = out - 1, scs' = 1 + scs.
|
(r3)
cs ≥ 1 —>
out' = 1 + out, cs' = cs - 1.
|
(r4)
scs ≥ 1 —>
out' = 1 + out, scs' = scs - 1.
|
- The parameterized initial configuration is expressed as:
out ≥ 0, cs = 0, scs = 0 - The potentially unsafe states:
(1)cs ≥ 1, scs ≥ 1
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #16 (Control Server Monitor protocol):
The description of the parameterized Control Server Monitor protocol is taken from the web-page by Laurent van Begin.
(REQ)
Think ≥ 1 —>
Think' = Think - 1, WaitC' = WaitC + 1.
|
(USE_C)
WaitC ≥ 1, IdleC ≥ 1 —>WaitC' = WaitC - 1, IdleC' = IdleC - 1, UseC' = 1 + UseC, BusyC' = 1 + BusyC. |
(RELEASE_C1)
UseC ≥ 1, BusyC ≥ 1 —>Think' = 1 + Think, IdleC' = 1 + IdleC, UseC' = UseC - 1, BusyC' = BusyC - 1. |
(RELEASE_C2)
UseC ≥ 1, BusyC ≥ 1 —> WaitD' = 1 + WaitD, IdleC' = 1 + IdleC, UseC' = UseC - 1, BusyC' = BusyC - 1. |
(USE_D)
WaitD ≥ 1, IdleD ≥ 1 —> UseD' = 1 + UseD, BusyD' = 1 + BusyD, WaitD' = WaitD - 1, IdleD' = IdleD - 1. |
(RELEASE_D)
UseD ≥ 1, BusyD ≥ 1 —> WaitC' = 1 + WaitC, IdleD' = 1 + IdleD, UseD' = UseD - 1, BusyD' = BusyD - 1. |
(STOP)
Noint ≥ 1 —> Int' = 1 + Int, Noint' = Noint - 1, Stopped' = UseC + Stopped, IdleC' = IdleC + Pbusy, UseC' = 0, Pbusy' = 0. |
(RETURN)
Int ≥ 1 —> Noint' = 1 + Noint, Int' = Int - 1, Pbusy' = IdleC + Pbusy, UseC' = UseC + Stopped, Stopped' = 0, IdleC' = 0. |
- The parameterized initial configuration is expressed as:
Think ≥ 1, WaitC = 0, UseC = 0, Stopped = 0, WaitD = 0, UseD = 0, IdleD = 1,
BusyD = 0, IdleC = 1, BusyC = 0, Pbusy = 0, Noint = 1, Int = 0- The potentially unsafe states:
(1)UseC ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #17 (Inc/Dec):
This incorrect model of the parameterized "Atomic Increments and decrements on a Point object" protocol is taken from the web-page by Laurent van Begin. For example, the specification part violating the safety property is shown with the red color.
(r1)
whileinc ≥ 1 —>
whileinc' = whileinc - 1, incx' = 1 + incx.
|
(r2)
incx ≥ 1, unlock ≥ 1 —>
incx' = incx - 1, xi' = 1 + xi, unlock' = unlock - 1, lock' = 1 + lock. |
(r3)
xi ≥ 1 —>
xi' = xi - 1, notifyincx' = 1 + notifyincx, xpos' = xpos + notxpos, notxpos' = 0. |
(r4)
notifyincx ≥ 1 —>
notifyincx' = notifyincx - 1, endincx' = 1 + endincx, afterwait1' = afterwait1 + wait1, wait1' = 0, afterwait2' = afterwait2 + wait2, wait2' = 0. |
(r5)
endincx ≥ 1, lock ≥ 1 —>
endincx' = endincx - 1, incy' = 1 + incy, lock' = lock - 1, unlock' = 1 + unlock. |
(r6)
incy ≥ 1, unlock ≥ 1 —>
incy' = incy - 1, yi' = 1 + yi, unlock' = unlock - 1, lock' = 1 + lock. |
(r7)
yi ≥ 1 —>
yi' = yi - 1, notifyincy' = 1 + notifyincy, ypos' = ypos + notypos, notypos' = 0. |
(r8)
notifyincy ≥ 1 —>
notifyincy' = notifyincy - 1, endincy' = 1 + endincy, afterwait1' = afterwait1 + wait1, wait1' = 0, afterwait2' = afterwait2 + wait2, wait2' = 0. |
(r9)
endincy ≥ 1, lock ≥ 1 —>
endincy' = endincy - 1, endinc' = 1 + endinc, lock' = lock - 1, unlock' = 1 + unlock. |
(r10)
endinc ≥ 1 —>
endinc' = endinc - 1,
whileinc' = 1 + whileinc.
|
(r11)
whiledec ≥ 1 —>
whiledec' = whiledec - 1,
decx' = 1 + decx.
|
(r12)
decx ≥ 1, unlock ≥ 1 —>
decx' = decx - 1, while1' = 1 + while1, unlock' = unlock - 1, lock' = 1 + lock. |
(r13)
while1 ≥ 1, lock ≥ 1, notxpos ≥ 1 —>
while1' = while1 - 1, wait1' = 1 + wait1, lock' = lock - 1, unlock' = 1 + unlock. |
(r14)
afterwait1 ≥ 1, unlock ≥ 1 —>
afterwait1' = afterwait1 - 1, while1' = 1 + while1, unlock' = unlock - 1, lock' = 1 + lock. |
(r15)
while1 ≥ 1, xpos ≥ 1 —>
while1' = while1 - 1,
xd' = 1 + xd.
|
(r16)
xd ≥ 1 —>
xd' = xd - 1, enddecx1' = 1 + enddecx1, xpos' = xpos + notxpos, notxpos' = 0. |
(r17)
xd ≥ 1 —>
xd' = xd - 1, enddecx2' = 1 + enddecx2, notxpos' = xpos + notxpos, xpos' = 0. |
(r18)
enddecx1 ≥ 1, lock ≥ 1 —>
enddecx1' = enddecx1 - 1, decy' = 1 + decy, lock' = lock - 1, unlock' = 1 + unlock. |
(r19)
enddecx2 ≥ 1, lock ≥ 1 —>
enddecx2' = enddecx2 - 1, decy' = 1 + decy, lock' = lock - 1, unlock' = 1 + unlock. |
(r20)
decy ≥ 1, unlock ≥ 1 —>
decy' = decy - 1, while2' = 1 + while2, unlock' = unlock - 1, lock' = 1 + lock. |
(r21)
while2 ≥ 1, notypos ≥ 1, lock ≥ 1 —>
while2' = while2 - 1, wait2' = 1 + wait2, lock' = lock - 1, unlock' = 1 + unlock. |
(r22)
afterwait2 ≥ 1, unlock ≥ 1 —>
afterwait2' = afterwait2 - 1, while2' = 1 + while2, unlock' = unlock - 1, lock' = 1 + lock. |
(r23)
while2 ≥ 1, ypos ≥ 1 —>
while2' = while2 - 1,
yd' = 1 + yd.
|
(r24)
yd ≥ 1 —>
yd' = yd - 1, enddecy1' = 1 + enddecy1, ypos' = ypos + notypos, notypos' = 0. |
(r25)
yd ≥ 1 —>
yd' = yd - 1, enddecy2' = 1 + enddecy2, notypos' = ypos + notypos, ypos' = 0. |
(r26)
enddecy1 ≥ 1, lock ≥ 1 —>
enddecy1' = enddecy1 - 1, enddec' = 1 + enddec, lock' = lock - 1, unlock' = 1 + unlock. |
(r27)
enddecy2 ≥ 1, lock ≥ 1 —>
enddecy2' = enddecy2 - 1, enddec' = 1 + enddec, lock' = lock - 1, unlock' = 1 + unlock. |
(r28)
enddec ≥ 1 —>
enddec' = enddec - 1,
whiledec' = 1 + whiledec.
|
- The parameterized initial configuration is expressed as:
whileinc ≥ 1, incx = 0, xi = 0, notifyincx = 0, endincx = 0, incy = 0, yi = 0,
notifyincy = 0, endincy = 0, endinc = 0, whiledec ≥ 1, decx = 0, while1 = 0,
wait1 = 0, afterwait1 = 0, xd = 0, enddecx1 = 0, enddecx2 = 0, decy = 0, while2 = 0,
wait2 = 0, afterwait2 = 0, yd = 0, enddecy1 = 0, enddecy2 = 0, enddec = 0, xpos = 0,
notxpos = 1, ypos = 0, notypos = 1, lock = 0, unlock = 1- The potentially unsafe states:
(1)decy ≥ 2(2)decy ≥ 1, incy ≥ 1(3)incy ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #18 (P/C):
The description of the parameterized Consumer Producer protocol is taken from the web-page by Laurent van Begin.
(c1)
initc ≥ 1 —>
initc' = initc - 1, whilec' = 1 + whilec.
|
(c2)
whilec ≥ 1, notlock ≥ 1 —>
whilec' = whilec - 1, whileget' = 1 + whileget, notlock' = notlock - 1, lock' = 1 + lock. |
(c3)
whileget ≥ 1, notavailable ≥ 1, lock ≥ 1 —>whileget' = whileget - 1, waitget' = 1 + waitget, lock' = lock - 1, notlock' = 1 + notlock. |
(c4)
competec ≥ 1, notlock ≥ 1 —> competec' = competec - 1, whileget' = 1 + whileget, notlock' = notlock - 1, lock' = 1 + lock. |
(c5)
whileget ≥ 1, available ≥ 1 —> whileget' = whileget - 1, notifyc' = 1 + notifyc, notavailable' = 1 + notavailable, available' = available - 1. |
(c6)
notifyc ≥ 1 —> notifyc' = notifyc - 1, endc' = 1 + endc, competec' = competec + waitget, waitget' = 0, competep' = competep + waitput, waitput' = 0. |
(c7)
endc ≥ 1, lock ≥ 1 —> endc' = endc - 1, whilec' = 1 + whilec, lock' = lock - 1, notlock' = 1 + notlock. |
(p1)
initp ≥ 1 —>
initp' = initp - 1, whilep' = 1 + whilep.
|
(p2)
whilep ≥ 1, notlock ≥ 1 —> whilep' = whilep - 1, whileput' = 1 + whileput, notlock' = notlock - 1, lock' = 1 + lock. |
(p3)
whileput ≥ 1, lock ≥ 1, available ≥ 1 —> whileput' = whileput - 1, waitput' = 1 + waitput, lock' = lock - 1, notlock' = 1 + notlock. |
(p4)
competep ≥ 1, notlock ≥ 1 —> competep' = competep - 1, whileput' = 1 + whileput, notlock' = notlock - 1, lock' = 1 + lock. |
(p5)
whileput ≥ 1, notavailable ≥ 1 —> whileput' = whileput - 1, notifyp' = 1 + notifyp, available' = 1 + available, notavailable' = notavailable - 1. |
(p6)
notifyp ≥ 1 —> notifyp' = notifyp - 1, returnp' = 1 + returnp, competec' = competec + waitget, waitget' = 0, competep' = competep + waitput, waitput' = 0. |
(p7)
returnp ≥ 1, lock ≥ 1 —> returnp' = returnp - 1, whilep' = 1 + whilep, lock' = lock - 1, notlock' = 1 + notlock. |
- The parameterized initial configuration is expressed as:
initc ≥ 1, whilec = 0, whileget = 0, waitget = 0, competec = 0, notifyc = 0,
endc = 0, initp ≥ 1, whilep = 0, whileput = 0, waitput = 0, competep = 0,
notifyp = 0, returnp = 0, available = 0, notavailable = 1, lock = 0, notlock = 1- The potentially unsafe states:
(1)waitget ≥ 2, waitput ≥ 2
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #19 (P/C2sansinv):
The description of the parameterized broadcast Consumer-producer protocol is taken from the web-page by Laurent van Begin. The property is that a consumer can consume a resource only when one is available.
(c1)
initc ≥ 1 —>
initc' = initc - 1, whilec' = 1 + whilec.
|
(c2)
whilec ≥ 1, notlock ≥ 1 —> whilec' = whilec - 1, whileget' = 1 + whileget, notlock' = notlock - 1, lock' = 1 + lock. |
(c3)
whileget ≥ 1, notavailable ≥ 1, lock ≥ 1 —>
whileget' = whileget - 1, waitget' = 1 + waitget, lock' = lock - 1, notlock' = 1 + notlock. |
(c4)
competec ≥ 1, notlock ≥ 1 —> competec' = competec - 1, whileget' = 1 + whileget, notlock' = notlock - 1, lock' = 1 + lock. |
(c5)
whileget ≥ 1, available ≥ 1 —>
whileget' = whileget - 1, consume' = 1 + consume. |
(c6)
consume ≥ 1 —>
consume' = consume - 1, notifyc' = 1 + notifyc, notavailable' = 1 + notavailable, available' = available - 1. |
(c7)
notifyc ≥ 1 —>
notifyc' = notifyc - 1, endc' = 1 + endc, competec' = competec + waitget, waitget' = 0, competep' = competep + waitput, waitput' = 0. |
(c8)
endc ≥ 1, lock ≥ 1 —>
endc' = endc - 1, whilec' = 1 + whilec, lock' = lock - 1, notlock' = 1 + notlock. |
(p1)
initp ≥ 1 —>
initp' = initp - 1, whilep' = 1 + whilep.
|
(p2)
whilep ≥ 1, notlock ≥ 1 —>
whilep' = whilep - 1, whileput' = 1 + whileput, notlock' = notlock - 1, lock' = 1 + lock. |
(p3)
whileput ≥ 1, lock ≥ 1, available ≥ 1 —>
whileput' = whileput - 1, waitput' = 1 + waitput, lock' = lock - 1, notlock' = 1 + notlock. |
(p4)
competep ≥ 1, notlock ≥ 1 —>
competep' = competep - 1, whileput' = 1 + whileput, notlock' = notlock - 1, lock' = 1 + lock. |
(p5)
whileput ≥ 1, notavailable ≥ 1 —>
whileput' = whileput - 1, produce' = 1 + produce. |
(p6)
produce ≥ 1 —>
produce' = produce - 1, notifyp' = 1 + notifyp, available' = 1 + available, notavailable' = notavailable - 1. |
(p7)
notifyp ≥ 1 —>
notifyp' = notifyp - 1, returnp' = 1 + returnp, competec' = competec + waitget, waitget' = 0, competep' = competep + waitput, waitput' = 0. |
(p8)
returnp ≥ 1, lock ≥ 1 —>
returnp' = returnp - 1, whilep' = 1 + whilep, lock' = lock - 1, notlock' = 1 + notlock. |
- The parameterized initial configuration is expressed as:
initc ≥ 1, initp ≥ 1, whilec = 0, whileget = 0, waitget = 0, competec = 0,
notifyc = 0, consume = 0, endc = 0, whilep = 0, whileput = 0, waitput = 0,
competep = 0, notifyp = 0, produce = 0, returnp = 0, available = 0,
notavailable = 1, lock = 0, notlock = 1- The potentially unsafe states:
(1)consume ≥ 1, notavailable ≥ 1
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #20 (2P/2C):
The description of the parameterized Two Consumers - Two Producers protocol is taken from the web-page by Laurent van Begin.
(ci1)
c2while1 ≥ 1 —>
c2while1' = c2while1 - 1, c2getwa' = 1 + c2getwa.
|
(ci2)
c2getwa ≥ 1, unlock ≥ 1 —>
c2getwa' = c2getwa - 1, c2while2' = 1 + c2while2, unlock' = unlock - 1, lock' = 1 + lock. |
(ci3)
c2while2 ≥ 1, isack ≥ 1 & lock ≥ 1 —>
c2while2' = c2while2 - 1, c2wait1' = 1 + c2wait1, lock' = lock - 1, unlock' = 1 + unlock. |
(ci4)
c2while2 ≥ 1, notaskforack ≥ 1, lock ≥ 1 —>
c2while2' = c2while2 - 1, c2wait1' = 1 + c2wait1, lock' = lock - 1, unlock' = 1 + unlock. |
(ci5)
c2afterwait1 ≥ 1, unlock ≥ 1 —>
c2afterwait1' = c2afterwait1 - 1, c2while2' = 1 + c2while2, unlock' = unlock - 1, lock' = 1 + lock. |
(ci6)
c2while2 ≥ 1, notisack ≥ 1, askforack ≥ 1 —>
c2while2' = c2while2 - 1, c2return' = 1 + c2return, notaskforack' = 1 + notaskforack, askforack' = askforack - 1, needack' = needack + notneedack, notneedack' = 0, c2afterwait1' = c2afterwait1 + c2wait1, c2wait1' = 0, c2afterwait2' = c2afterwait2 + c2wait2, c2wait2' = 0, p2afterwait1' = p2afterwait1 + p2wait1, p2wait1' = 0, p2afterwait2' = p2afterwait2 + p2wait2, p2wait2' = 0, cafterwait' = cafterwait + cwait, cwait' = 0, pafterwait' = pafterwait+ pwait, pwait' = 0. |
(ci7)
c2return ≥ 1, lock ≥ 1 —>
c2return' = c2return - 1, c2putack' = 1 + c2putack, lock' = lock - 1, unlock' = 1 + unlock. |
(ci8)
c2putack ≥ 1, unlock ≥ 1 —>
c2putack' = c2putack - 1, c2while3' = 1 + c2while3, unlock' = unlock - 1, lock' = 1 + lock. |
(ci9)
c2while3 ≥ 1, available ≥ 1, lock ≥ 1 —>
c2while3' = c2while3 - 1, c2wait2' = 1 + c2wait2, lock' = lock - 1, unlock' = 1 + unlock. |
(ci10)
c2afterwait2 ≥ 1, unlock ≥ 1 —>
c2afterwait2' = c2afterwait2 - 1, c2while3' = 1 + c2while3, unlock' = unlock - 1, lock' = 1 + lock. |
(ci11)
c2while3 ≥ 1, notavailable ≥ 1 —>
c2while3' = c2while3 - 1, c2end' = 1 + c2end, notavailable' = notavailable - 1, available' = 1 + available, isack' = isack + notisack, notisack' = 0, c2afterwait1' = c2afterwait1 + c2wait1, c2wait1' = 0, c2afterwait2' = c2afterwait2 + c2wait2, c2wait2' = 0, p2afterwait1' = p2afterwait1 + p2wait1, p2wait1' = 0, p2afterwait2' = p2afterwait2 + p2wait2, p2wait2' = 0, cafterwait' = cafterwait + cwait, cwait' = 0, pafterwait' = pafterwait + pwait, pwait' = 0. |
(ci12)
c2end ≥ 1, lock ≥ 1 —>
c2end' = c2end - 1, c2while1'= 1 + c2while1, lock' = lock - 1, unlock' = 1 + unlock. |
(p2_1)
p2while1 ≥ 1 —>
p2while1' = p2while1 - 1, p2putwa' = 1 + p2putwa.
|
(p2_2)
p2putwa ≥ 1, unlock ≥ 1 —>
p2putwa' = p2putwa - 1, p2while2' = 1 + p2while2, unlock' = unlock - 1, lock' = lock + 1. |
(p2_3)
p2while2 ≥ 1, lock ≥ 1, available ≥ 1 —>
p2while2' = p2while2 - 1, p2wait1' = 1 + p2wait1, lock' = lock - 1, unlock' = 1 + unlock. |
(p2_4)
p2while2 ≥ 1, lock ≥ 1, needack ≥ 1 —>
p2while2' = p2while2 - 1, p2wait1' = 1 + p2wait1, lock' = lock - 1, unlock' = 1 + unlock. |
(p2_5)
p2afterwait1 ≥ 1, unlock ≥ 1 —>
p2afterwait1' = p2afterwait1 - 1, p2while2' = 1 + p2while2, unlock' = unlock - 1, lock' = 1 + lock. |
(p2_6)
p2while2 ≥ 1, notavailable ≥ 1, notneedack ≥ 1 —>
p2while2' = p2while2 - 1, p2end' = 1 + p2end, askforack' = askforack + notaskforack, notaskforack' = 0, c2afterwait1' = c2afterwait1 + c2wait1, c2wait1' = 0, c2afterwait2' = c2afterwait2 + c2wait2, c2wait2' = 0, p2afterwait1' = p2afterwait1 + p2wait1, p2wait1' = 0, p2afterwait2' = p2afterwait2 + p2wait2, p2wait2' = 0, cafterwait' = cafterwait + cwait, cwait' = 0, pafterwait' = pafterwait + pwait, pwait' = 0. |
(p2_7)
p2end ≥ 1, lock ≥ 1 —>
p2end' = p2end - 1, p2getack' = 1 + p2getack, lock' = lock - 1, unlock' = 1+ unlock. |
(p2_8)
p2getack ≥ 1, unlock ≥ 1 —>
p2getack' = p2getack - 1, p2while3' = 1 + p2while3, unlock' = unlock - 1, lock' = 1 + lock. |
(p2_9)
p2while3 ≥ 1, lock ≥ 1, notisack ≥ 1 —>
p2while3' = p2while3 - 1, p2wait2' = 1 + p2wait2, lock' = lock - 1, unlock' = 1 + unlock. |
(p2_10)
p2afterwait2 ≥ 1, unlock ≥ 1 —>
p2afterwait2' = p2afterwait2 - 1, p2while3' = 1 + p2while3, unlock' = unlock - 1, lock' = 1 + lock. |
(p2_11)
p2while3 ≥ 1, isack ≥ 1 —>
p2while3' = p2while3 - 1, p2return' = 1 + p2return, notisack' = 1 + notisack, isack' = isack - 1, notavailable' = notavailable + available, available' = 0, notneedack' = notneedack + needack, needack' = 0, c2afterwait1' = c2afterwait1 + c2wait1, c2wait1' = 0, c2afterwait2' = c2afterwait2 + c2wait2, c2wait2' = 0, p2afterwait1' = p2afterwait1 + p2wait1, p2wait1' = 0, p2afterwait2' = p2afterwait2 + p2wait2, p2wait2' = 0, cafterwait' = cafterwait + cwait, cwait' = 0. pafterwait' = pafterwait + pwait, pwait'= 0. |
(p2_12)
p2return ≥ 1, lock ≥ 1 —>
p2return' = p2return - 1, p2while1' = 1 + p2while1, lock' = lock - 1, unlock' = 1 + unlock. |
(c1)
cwhile1 ≥ 1 —>
cwhile1' = cwhile1 - 1, get' = 1 + get.
|
(c2)
get ≥ 1, unlock ≥ 1 —>
get' = get - 1, cwhile2' = 1 + cwhile2, unlock' = unlock - 1, lock' = 1 + lock. |
(c3)
cwhile2 ≥ 1, lock ≥ 1, notavailable ≥ 1 —>
cwhile2' = cwhile2 - 1, cwait' = 1 + cwait, lock' = lock - 1, unlock' = 1 + unlock. |
(c4)
cwhile2 ≥ 1, lock ≥ 1, askforack ≥ 1 —>
cwhile2' = cwhile2 - 1, cwait' = 1 + cwait, lock' = lock - 1, unlock' = 1 + unlock. |
(c5)
cafterwait ≥ 1, unlock ≥ 1 —>
cafterwait' = cafterwait - 1, cwhile2' = 1 + cwhile2, unlock' = unlock - 1, lock' = 1 + lock. |
(c6)
cwhile2 ≥ 1, available ≥ 1, notaskforack ≥ 1 —>
cwhile2' = cwhile2 - 1, creturn' = 1 + creturn, notavailable' = 1 + notavailable, available' = available - 1, c2afterwait1' = c2afterwait1 + c2wait1, c2wait1' = 0, c2afterwait2' = c2afterwait2 + c2wait2, c2wait2' = 0, p2afterwait1' = p2afterwait1 + p2wait1, p2wait1' = 0, p2afterwait2' = p2afterwait2 + p2wait2, p2wait2' = 0, cafterwait' = cafterwait + cwait, cwait' = 0, pafterwait' = pafterwait + pwait, pwait' = 0. |
(c7)
creturn ≥ 1, lock ≥ 1 —>
creturn' = creturn - 1, cwhile1' = 1 + cwhile1, lock' = lock - 1, unlock' = 1 + unlock. |
(p1)
pwhile1 ≥ 1 —>
pwhile1' = pwhile1 - 1, put' = 1 + put.
|
(p2)
put ≥ 1, unlock ≥ 1 —>
put' = put - 1, pwhile2' = 1 + pwhile2 unlock' = unlock - 1, lock' = 1 + lock. |
(p3)
pwhile2 ≥ 1, lock ≥ 1, available ≥ 1 —>
pwhile2' = pwhile2 - 1, pwait' = 1 + pwait, lock' = lock - 1, unlock' = 1 + unlock. |
(p4)
pafterwait ≥ 1, unlock ≥ 1 —>
pafterwait' = pafterwait - 1, pwhile2' = 1 + pwhile2, unlock' = unlock - 1, lock' = 1 + lock. |
(p5)
pwhile2 ≥ 1, notavailable ≥ 1 —>
pwhile2' = pwhile2 - 1, pend' = 1 + pend, available' = 1 + available, notavailable' = notavailable - 1, c2afterwait1' = c2afterwait1 + c2wait1, c2wait1' = 0, c2afterwait2' = c2afterwait2 + c2wait2, c2wait2' = 0, p2afterwait1' = p2afterwait1 + p2wait1, p2wait1' = 0, p2afterwait2' = p2afterwait2 + p2wait2, p2wait2' = 0, cafterwait' = cafterwait + cwait, cwait' = 0, pafterwait' = pafterwait + pwait, pwait' = 0. |
(p6)
pend ≥ 1, lock ≥ 1 —>
pend' = pend - 1, pwhile1' = 1 + pwhile1, lock' = lock - 1, unlock' = 1 + unlock. |
- The parameterized initial configuration is expressed as:
c2while1 ≥ 1, p2while1 ≥ 1, cwhile1 ≥ 1, pwhile1 ≥ 1,
unlock = 1, lock = 0, available = 0, notavailable = 1, askforack = 0,
notaskforack = 0, needack = 0, notneedack = 1, isack = 0, notisack = 1,
c2getwa = 0, c2while2 = 0, c2wait1 = 0, c2afterwait1 = 0, c2return = 0,
c2putack = 0, c2while3 = 0, c2wait2 = 0, c2afterwait2 = 0, c2end = 0,
p2putwa = 0, p2while2 = 0, p2wait1 = 0, p2afterwait1 = 0, p2return = 0,
p2getack = 0, p2while3 = 0, p2wait2 = 0, p2afterwait2 = 0, p2end = 0,
cwhile2 = 0, get = 0, cwait = 0, cafterwait = 0, creturn = 0, put = 0,
pwhile2 = 0, pwait = 0, pafterwait = 0, pend = 0- The potentially unsafe states:
(1)notavailable ≥ 1, isack ≥ 1
| Top | Bottom | On specification | REFAL encoding | Result of supercompilation |
Example #21 (SPS2):
The incorrect specification of the parameterized SPS2 protocol is taken from the paper by X. Zhao, K. Sammut, F. He, Sh. Qin and made more precise (but still incorrect) by Xuemei Zhao in an e-mail message.
(r1)
SIS + OIS + MII ≥ 1 —> .
|
(r2)
III ≥ 1, MII = 0, IMI = 0 —>
III' = 0, SIS' = 1 + SIS, IIS' = IIS + III - 1. |
(r3)
III ≥ 1, MII ≥ 1 —>
III' = 0, SIS' = 1 + SIS, MII' = MII - 1, OIS' = 1 + OIS, IIS' = IIS + III - 1. |
(r4)
III ≥ 1, IMI ≥ 1 —>
III' = 0, SIS' = 1 + SIS, IMI' = IMI - 1, IOS' = 1 + IOS, IIS' = IIS + III - 1. |
(r5)
IIS ≥ 1 —>
IIS' = IIS - 1, SIS' = 1 + SIS.
|
(r6)
IMI ≥ 1 —>
MII' = 1 + MII, IMI' = IMI - 1.
|
(r7)
IOS ≥ 1 —>
OIS' = 1 + OIS, IOS' = IOS - 1.
|
(wh8)
MII ≥ 1 —> .
|
(wh9)
IMI ≥ 1 —>
IMI' = IMI - 1, MII' = 1 + MII.
|
(wm10)
OIS ≥ 1 —>
MII' = 1, OIS' = 0,
IIS' = 0, IMI' = 0,
IOS' = 0, SIS' = 0, III' = III + IIS + (OIS-1) + MII + IMI + IOS + SIS. |
(wm11)
IOS ≥ 1 —>
MII' = 1, IOS' = 0,
IIS' = 0, IMI' = 0, OIS' = 0,
SIS' = 0, III' = III + IIS + OIS + MII + IMI + (IOS-1) + SIS. |
(wm12)
SIS ≥ 1 —>
MII' = 1, SIS' = 0,
IIS' = 0, IMI' = 0, IOS' = 0,
OIS' = 0, III' = III + IIS + OIS + MII + IMI + IOS + (SIS-1). |
(wm13)
III ≥ 1 —>
MII' = 1,
IIS' = 0, IMI' = 0, IOS' = 0, SIS' = 0,
OIS' = 0, III' = (III-1) + IIS + OIS + MII + IMI + IOS + SIS. |
(wm14)
IIS ≥ 1 —>
MII' = 1, IIS' = 0,
IIS' = 0, IMI' = 0, IOS' = 0,
SIS' = 0, III' = III + IIS + (OIS-1) + MII + IMI + IOS + SIS. |
(rp1-r15)
MII ≥ 1 —>
MII' = MII - 1, IMI' = 1 + IMI.
|
(rp1-r16)
OIS ≥ 1 —>
OIS' = OIS - 1, IOS' = 1 + IOS.
|
(rp1-r17)
SIS ≥ 1 —>
SIS' = SIS - 1, IIS' = 1 + IIS.
|
(rp2-r18)
IOS ≥ 1 —>
IOS' = IOS - 1, IIS' = 1 + IIS.
|
(rp2-r19)
IMI ≥ 1 —>
IMI' = IMI - 1, III' = 1 + III.
|
(repS-r20)
IOS ≥ 1 —>
IOS' = IOS - 1, IMI' = 1 + IMI.
|
(repS-r21)
IIS ≥ 1 —>
IIS' = IIS - 1, III' = 1 + III.
|
(repS-r22)
SIS ≥ 1 —>
SIS' = SIS - 1, III' = 1 + III.
|
- The parameterized initial configuration is expressed as:
III ≥ 1, IIS = 0, SIS = 0, MII = 0, IMI = 0, OIS = 0, IOS = 0 - The potentially unsafe states:
(1)OIS ≥ 1, MII ≥ 1(2)OIS ≥ 2(3)IIS ≥ 1, IMI ≥ 1(4)MII ≥ 2
| Top | REFAL encoding | Result of supercompilation |