SPIN VERIFICATION EXAMPLES AND EXERCISES

Included in this memo are some verification exercises that can help new users to get acquainted with Spin. A few example models for standard verification problems are included at the end. All examples are also available as Promela files in the Test directory of the Spin distribution (they are bundled in the shell archive Test/examples in the main distribution).

1. Evaluating Search Complexity

This first exercise is meant to give an indication of the nature of the state space explosion phenomenon, and how Spin deals with it. It consists of eight small problems that are solved using Spin. The problems are numbered [1.a] through [1.h]. At each step, it is best to first try to predict what should happen, to write down these predictions, to then perform the experiment, and explain the results.
[1.a] How many reachable states do you predict will the following naive Promela model generate?
init { /* file: ex.1a */ byte i = 0; do :: i = i+1 od }
Try a simulation run:
$ spin -p -l ex.1a # print out local vars at every step ...
Will the simulation terminate? []
[1.b] Estimate the total number of reachable states that should be inspected in an exhaustive verification. Is it a finite number? Will a verification run terminate? Try it as follows.
$ spin -a ex.1a $ cc -o pan pan.c $ pan ...
Explain the output. []
[1.c] What would happen if you had declared the variable to be a short instead of a byte ? What if you use an int ? [Hint: use Table 1 in Manual.html]
Try either of them with a verification run. How do you explain the result? [Hint: check the analyzer's defaults by saying pan -? ] []
[1.d] Next, predict how many reachable states there are for the following system. Write them down as a complete reachability tree.
#define N 2 init { /* file: ex.1b */ chan dummy = [N] of { byte }; do :: dummy!85 :: dummy!170 od }
Check your prediction as follows. We're only interested in the size of the state space, not in the obvious problems caused by buffer overflow, so we use the -m option from Spin to define that buffer overflow is to be ignored. (Messages appended to a full buffer are then lost.)
$ spin -m -a ex.1b # use -m to ignore buffer overflow $ cc -o pan pan.c $ pan ...
Explain the result. []
[1.e] What happens if you set N to 3 ? Express the number of states as a function of N. Use the formula to calculate how many states there will be if you set N to 14 ? Check your prediction as follows.
$ spin -m -a ex.1b # use -m to ignore buffer overflow $ cc -o pan pan.c # optional: use the optimizer -O $ time pan ...

Write down: T: the sum of user time plus system time for the run S: the number of states stored G: the number of total number of states generated and analyzed V: the vector-size (the amount of memory needed to store one state) G/T gives you a measure for the efficiency of the run, and S*V gives you the amount of memory that is needed to store the state space without compression.
This is not the only place where memory that is used during the search (the stack also consumes memory) but it is typically the largest memory requirement. []
[1.f] The efficiency of the conventional reachability analysis is determined by the state space storage functions. To study this, repeat the last verification run with a smaller and a bigger hash table for storing reachable states:
$ time pan -w10 # hash table with 2¹⁰ slots ... $ time pan -w20 # hash table with 2²⁰ slots ...
Explain the results. [Hint: compare the number of hash conflicts.] []
[1.g] How much memory would you need to do a run with N=20 ? (Warning: both the number of reachable states and the number of bytes per state goes up with N. Estimate about 30 bytes per state for N=20.) Assuming that you have about 8 Megabyte on your system, what maximal fraction of the state-space would you expect to be able to analyze ?
Now set N to 20 and use the bitstate storage option, as follows.
$ spin -m -a ex.1b # as before $ cc -DBITSTATE -o pan pan.c # different $ time pan ...
If you did the calculation, you probably estimated that there should be 2,097,151 reachable system states for N=20. What percentage of these states was reached in the new run? How much memory was used [Hint: cf. [1.h] below] ? (Compare to the earlier estimated maximal coverage for a conventional verification and explain the difference.) []
[1.h] The default bitstate space, used above, has 2²² bits (i.e., 2¹⁸ bytes, or about one quarter Megabyte) repeat the run with different amount of memory to get different coverage. Check what percentage of the number of states is reached when you use the 8 Megabyte state space on which your first estimate for maximal coverage in a full state space search was based (2²³ bytes is 2²⁶ bits, which means a runtime flag -w26 )
You should be able to get close to 99% coverage and between 4,000 and 40,000 states analyzed per second. For comparison, the speed on a DEC/VAX-8550 is roughly 16,000 s/s.; on a 30 MIPS Silicon Graphics machine 40,000 s/s; on a Sun 3/60 4,500 s/s. []
2. Verification of a Protocol

Figure 2 shows a protocol specification given by Bartlett et al. as Figure 3c in their paper introducing the alternating-bit protocol. []

The Promela version of this protocol is shown below. Use Spin to check if it has the property that ``Every message fetched by A is received error-free at least once and accepted at most once by B.''

1 #define MAX 4 /* file ex.2 */ 2 proctype A(chan in, out) 3 { byte mt; /* message data */ 4 bit vr; 5 S1: mt = (mt+1)%MAX; 6 out!mt,1; 7 goto S2; 8 S2: in?vr; 9 if 10 :: (vr == 1) -> goto S1 11 :: (vr == 0) -> goto S3 12 :: printf("MSC: AERROR1\n") -> goto S5 13 fi; 14 S3: out!mt,1; 15 goto S2; 16 S4: in?vr; 17 if 18 :: goto S1 19 :: printf("MSC: AERROR2\n"); goto S5 20 fi; 21 S5: out!mt,0; 22 goto S4 23 } 24 proctype B(chan in, out) 25 { byte mr, lmr; 26 bit ar; 27 goto S2; /* initial state */ 28 S1: assert(mr == (lmr+1)%MAX); 29 lmr = mr; 30 out!1; 31 goto S2; 32 S2: in?mr,ar; 33 if 34 :: (ar == 1) -> goto S1 35 :: (ar == 0) -> goto S3 36 :: printf("MSC: ERROR1\n"); goto S5 37 fi; 38 S3: out!1; 39 goto S2; 40 S4: in?mr,ar; 41 if 42 :: goto S1 43 :: printf("MSC: ERROR2\n"); goto S5 44 fi; 45 S5: out!0; 46 goto S4 47 } 48 init { 49 chan a2b = [2] of { bit }; 50 chan b2a = [2] of { byte, bit }; 51 atomic { 52 run A(a2b, b2a); 53 run B(b2a, a2b) 54 } 55 }

3. Verification of an Interface Standard

CCITT Recommendation X.21 was one of the first protocols shown to be incompletely specified with an automated analysis. The verification was performed in 1977 by Colin West.

What in 1977 was described as a ``reasonably complex protocol'' is today a rather simple litmus test for automated protocol verifiers, that shouldn't take more than a few milli-seconds of CPU time. The Promela model below is derived from Figure 3, which is based on the specification used by West. (``all'' in Figure 3 means ``all other states.'')
1 mtype = { a, b, c, d, e, i, l, m, n, q, r, u, v }; 2 /* file ex.3 */ 3 chan dce = [0] of { mtype }; 4 chan dte = [0] of { mtype }; 5 6 active proctype dte_proc() 7 { 8 state01: 9 do 10 :: dce!b -> /* state21 */ dce!a 11 :: dce!i -> /* state14 */ 12 if 13 :: dte?m -> goto state19 14 :: dce!a 15 fi 16 :: dte?m -> goto state18 17 :: dte?u -> goto state08 18 :: dce!d -> break 19 od; 20 21 /* state02: */ 22 if 23 :: dte?v 24 :: dte?u -> goto state15 25 :: dte?m -> goto state19 26 fi; 27 state03: 28 dce!e; 29 /* state04: */ 30 if 31 :: dte?m -> goto state19 32 :: dce!c 33 fi; 34 /* state05: */ 35 if 36 :: dte?m -> goto state19 37 :: dte?r 38 fi; 39 /* state6A: */ 40 if 41 :: dte?m -> goto state19 42 :: dte?q 43 fi; 44 state07: 45 if 46 :: dte?m -> goto state19 47 :: dte?r 48 fi; 49 /* state6B: */ 50 if /* non-deterministic select */ 51 :: dte?q -> goto state07 52 :: dte?q 53 :: dte?m -> goto state19 54 fi; 55 /* state10: */ 56 if 57 :: dte?m -> goto state19 58 :: dte?r 59 fi; 60 state6C: 61 if 62 :: dte?m -> goto state19 63 :: dte?l 64 fi; 65 /* state11: */ 66 if 67 :: dte?m -> goto state19 68 :: dte?n 69 fi; 70 /* state12: */ 71 if 72 :: dte?m -> goto state19 73 :: dce!b -> goto state16 74 fi; 75 state15: 76 if 77 :: dte?v -> goto state03 78 :: dte?m -> goto state19 79 fi; 80 state08: 81 if 82 :: dce!c 83 :: dce!d -> goto state15 84 :: dte?m -> goto state19 85 fi; 86 /* state09: */ 87 if 88 :: dte?m -> goto state19 89 :: dte?q 90 fi; 91 /* state10B: */ 92 if 93 :: dte?r -> goto state6C 94 :: dte?m -> goto state19 95 fi; 96 state18: 97 if 98 :: dte?l -> goto state01 99 :: dte?m -> goto state19 100 fi; 101 state16: 102 dte?m; 103 /* state17: */ 104 dte?l; 105 /* state21: */ 106 dce!a; goto state01; 107 state19: 108 dce!b; 109 /* state20: */ 110 dte?l; 111 /* state21: */ 112 dce!a; goto state01 113 } 114 active proctype dce_proc() 115 { 116 state01: 117 do 118 :: dce?b -> /* state21 */ dce?a 119 :: dce?i -> /* state14 */ 120 if 121 :: dce?b -> goto state16 122 :: dce?a 123 fi 124 :: dte!m -> goto state18 125 :: dte!u -> goto state08 126 :: dce?d -> break 127 od; 128 129 /* state02: */ 130 if 131 :: dte!v 132 :: dte!u -> goto state15 133 :: dce?b -> goto state16 134 fi; 135 state03: 136 dce?e; 137 /* state04: */ 138 if 139 :: dce?b -> goto state16 140 :: dce?c 141 fi; 142 /* state05: */ 143 if 144 :: dce?b -> goto state16 145 :: dte!r 146 fi; 147 /* state6A: */ 148 if 149 :: dce?b -> goto state16 150 :: dte!q 151 fi; 152 state07: 153 if 154 :: dce?b -> goto state16 155 :: dte!r 156 fi; 157 /* state6B: */ 158 if /* non-deterministic select */ 159 :: dte!q -> goto state07 160 :: dte!q 161 :: dce?b -> goto state16 162 fi; 163 /* state10: */ 164 if 165 :: dce?b -> goto state16 166 :: dte!r 167 fi; 168 state6C: 169 if 170 :: dce?b -> goto state16 171 :: dte!l 172 fi; 173 /* state11: */ 174 if 175 :: dce?b -> goto state16 176 :: dte!n 177 fi; 178 /* state12: */ 179 if 180 :: dce?b -> goto state16 181 :: dte!m -> goto state19 182 fi; 183 state15: 184 if 185 :: dte!v -> goto state03 186 :: dce?b -> goto state16 187 fi; 188 state08: 189 if 190 :: dce?c 191 :: dce?d -> goto state15 192 :: dce?b -> goto state16 193 fi; 194 /* state09: */ 195 if 196 :: dce?b -> goto state16 197 :: dte!q 198 fi; 199 /* state10B: */ 200 if 201 :: dte!r -> goto state6C 202 :: dce?b -> goto state16 203 fi; 204 state18: 205 if 206 :: dte!l -> goto state01 207 :: dce?b -> goto state16 208 fi; 209 state16: 210 dte!m; 211 /* state17: */ 212 dte!l; 213 /* state21: */ 214 dce?a; goto state01; 215 state19: 216 dce?b; 217 /* state20: */ 218 dte!l; 219 /* state21: */ 220 dce?a; goto state01 221 }
Verify the X.21 protocol using Spin. []
4. Verification of Mutual Exclusion Algorithms

If two or more concurrent processes execute the same code and access the same data, there is a potential problem that they may overwrite each others results and corrupt the data. The mutual exclusion problem is the problem of restricting access to a critical section in the code to a single process at a time, assuming only the indivisibility of read and write instructions. (The problem disappears if one can assume an indivisible test-and-set instruction.) The problem and a first solution were first published by Dijkstra.
[4.a] The following `improved' solution appeared one year later in the same journal (Comm. of the ACM, Vol. 9, No. 1, p. 45) by another author. It is reproduced here as it was published (in pseudo Algol).
1 Boolean array b(0;1) integer k, i, j, 2 comment process i, with i either 0 or 1 and j = 1-i; 3 C0: b(i) := false; 4 C1: if k != i then begin 5 C2: if not (b(j) then go to C2; 6 else k := i; go to C1 end; 7 else critical section; 8 b(i) := true; 9 remainder of program; 10 go to C0; 11 end
Model the solution in Promela, and proof or disproof the correctness of the algorithm. []
[4.b] The problem continues to be popular. For an overview solution attempts up to roughly 1984, see Raynal or Lamport. For two processes, for instance, a particularly elegant solution was published by Peterson. In Promela the solution can be modeled as follows. The predefined variable \(CW_pid contains the id of the running process: in this case either 0 or 1.
1 #define true 1 /* file ex.4b */ 2 #define false 0 3 bool flag[2]; 4 bool turn; 5 active [2] proctype user() 6 { flag[_pid] = true; 7 turn = _pid; 8 (flag[1-_pid] == false || turn == 1-_pid); 9 crit: skip; /* critical section */ 10 flag[_pid] = false 11 }
Prove Peterson's algorithm correct with Spin. []
[4.c] Despite all the publications, there is no shortage of faulty solutions to the mutual exclusion problem. The next version was recommended by a computer manufacturer to a customer.
1 byte in; /* file ex.4c */ 2 byte x, y, z; 3 active [2] proctype user() 4 { byte me = _pid+1; /* me is 1 or 2 */ 5 L1: x = me; 6 L2: if 7 :: (y != 0 && y != me) -> goto L1 /* try again */ 8 :: (y == 0 || y == me) 9 fi; 10 L3: z = me; 11 L4: if 12 :: (x != me) -> goto L1 /* try again */ 13 :: (x == me) 14 fi; 15 L5: y = me; 16 L6: if 17 :: (z != me) -> goto L1 /* try again */ 18 :: (z == me) 19 fi; 20 L7: /* success */ 21 in = in+1; 22 assert(in == 1); 23 in = in - 1; 24 goto L1 25 }
First try to find a scenario that leads to the assertion violation by studying the algorithm. Next generate the counter-example with Spin. []
5. Verification of Petri Nets

It is often easier to build an little verification model and mechanically verify it than it is to write or to check a manual proof of correctness.

Petri Nets are relatively easy to model as Promela verification models. A Promela model for the net in Figure 4, for instance, is shown below.
1 #define Place byte /* assume < 256 tokens per place */ 2 /* file ex.5a */ 3 Place p1, p2, p3; 4 Place p4, p5, p6; 5 #define inp1(x) (x>0) -> x=x-1 6 #define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1 7 #define out1(x) x=x+1 8 #define out2(x,y) x=x+1; y=y+1 9 init 10 { p1 = 1; p4 = 1; /* initial marking */ 11 do 12 /*t1*/ :: atomic { inp1(p1) -> out1(p2) } 13 /*t2*/ :: atomic { inp2(p2,p4) -> out1(p3) } 14 /*t3*/ :: atomic { inp1(p3) -> out2(p1,p4) } 15 /*t4*/ :: atomic { inp1(p4) -> out1(p5) } 16 /*t5*/ :: atomic { inp2(p1,p5) -> out1(p6) } 17 /*t6*/ :: atomic { inp1(p6) -> out2(p4,p1) } 18 od 19 }

For this exercise, consider the Petri Net model below, which first appeared as Figure 1 in Berthelot et al.. The net was proven to be deadlock free with a manual reduction and proof technique. Verify the result with Spin. []
1 #define Place byte /* assume < 256 tokens per place */ 2 /* file ex.5b */ 3 Place P1, P2, P4, P5, RC, CC, RD, CD; 4 Place p1, p2, p4, p5, rc, cc, rd, cd; 5 6 #define inp1(x) (x>0) -> x=x-1 7 #define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1 8 #define out1(x) x=x+1 9 #define out2(x,y) x=x+1; y=y+1 10 11 init 12 { P1 = 1; p1 = 1; /* initial marking */ 13 do 14 :: atomic { inp1(P1) -> out2(rc,P2) } /* DC */ 15 :: atomic { inp2(P2,CC) -> out1(P4) } /* CA */ 16 :: atomic { inp1(P4) -> out2(P5,rd) } /* DD */ 17 :: atomic { inp2(P5,CD) -> out1(P1) } /* FD */ 18 :: atomic { inp2(P1,RC) -> out2(P4,cc) } /* AC */ 19 :: atomic { inp2(P4,RD) -> out2(P1,cd) } /* AD */ 20 :: atomic { inp2(P5,RD) -> out1(P1) } /* DA */ 21 22 :: atomic { inp1(p1) -> out2(RC,p2) } /* dc */ 23 :: atomic { inp2(p2,cc) -> out1(p4) } /* ca */ 24 :: atomic { inp1(p4) -> out2(p5,RD) } /* dd */ 25 :: atomic { inp2(p5,cd) -> out1(p1) } /* fd */ 26 :: atomic { inp2(p1,rc) -> out2(p4,CC) } /* ac */ 27 :: atomic { inp2(p4,rd) -> out2(p1,CD) } /* ad */ 28 :: atomic { inp2(p5,rd) -> out1(p1) } /* da */ 29 od 30 }

6. The Cambridge Ring Protocol

The model below is based on the description in Needham and Herbert's book.
1 #define LOSS 0 /* enable or disable message loss */ 2 /* file ex.6 */ 3 #define QSZ 5 /* length of message queues */ 4 5 mtype = { RDY, NOTRDY, DATA, NODATA, RESET }; 6 7 chan sender = [QSZ] of { mtype, byte }; 8 chan recv = [QSZ] of { mtype, byte }; 9 10 active proctype Sender() 11 { short n = -1; byte t,m; 12 13 xr sender; 14 xs recv; 15 16 I: /* Idle State */ 17 do 18 #if LOSS==1 19 :: sender?_,_ -> progress2: skip 20 #endif 21 :: sender?RESET,0 -> 22 ackreset: recv!RESET,0; /* stay in idle */ 23 n = -1; 24 goto I 25 26 /* E-rep: protocol error */ 27 28 :: sender?RDY,m -> /* E-exp */ 29 assert(m == (n+1)%4); 30 advance: n = (n+1)%4; 31 if 32 /* buffer */ :: atomic { 33 printf("MSC: NEW\n"); 34 recv!DATA,n; 35 goto E 36 } 37 /* no buffer */ :: recv!NODATA,n; 38 goto N 39 fi 40 41 :: sender?NOTRDY,m -> /* N-exp */ 42 expected: assert(m == (n+1)%4); 43 goto I 44 45 /* Timeout */ 46 /* ignored (p.154, in [Needham'82]) */ 47 48 :: goto reset /* spontaneous reset */ 49 od; 50 E: /* Essential element sent, ack expected */ 51 do 52 #if LOSS==1 53 :: sender?_,_ -> progress0: skip 54 #endif 55 :: sender?RESET,0 -> 56 goto ackreset 57 58 :: sender?RDY,m -> 59 if 60 :: (m == n) -> /* E-rep */ 61 goto retrans 62 :: (m == (n+1)%4) -> /* E-exp */ 63 goto advance 64 fi 65 66 :: sender?NOTRDY,m -> /* N-exp */ 67 goto expected 68 69 /* Timeout */ 70 /* a proper behaved timeout leaves part of the 71 protocol specification unreachable; to check 72 less well-behaved timeout behavior, replace 73 the timeout keyword below with "empty(sender)" 74 to allow the retransmission at any time when the 75 sender queue is empty. even more mis-behaved 76 timeouts can be checked by replacing timeout with 77 "skip" (i.e., unconditionally executable) 78 */ 79 :: timeout -> 80 printf("MSC: STO\n"); 81 retrans: recv!DATA,n /* retransmit */ 82 83 :: goto reset 84 od; 85 N: /* Non-essential element sent */ 86 do 87 #if LOSS==1 88 :: sender?_,_ -> progress1: skip 89 #endif 90 :: sender?RESET,0 -> 91 goto ackreset 92 93 :: sender?RDY,m -> /* E-rep */ 94 assert(m == n) /* E-exp: protocol error */ 95 -> recv!NODATA,n /* retransmit and stay in N */ 96 97 :: recv!DATA,n; /* buffer ready event */ 98 goto E 99 100 :: goto reset 101 102 /* Timeout */ 103 /* ignored (p.154, in [Needham'82]) */ 104 od; 105 106 reset: recv!RESET,0; 107 do 108 #if LOSS==1 109 :: sender?_,_ -> progress3: skip 110 #endif 111 :: sender?t,m -> 112 if 113 :: t == RESET -> n = -1; goto I 114 :: else /* ignored, p. 152 */ 115 fi 116 :: timeout -> 117 goto reset 118 od 119 } 120 active proctype Receiver() 121 { byte t, n, m, Nexp; 122 123 xr recv; 124 xs sender; 125 126 I: /* Idle State */ 127 do 128 #if LOSS==1 129 :: recv?_,_ -> progress2: skip 130 #endif 131 :: recv?RESET,0 -> 132 ackreset: sender!RESET,0; /* stay in idle */ 133 n = 0; Nexp = 0; 134 goto I 135 136 :: atomic { recv?DATA(m) -> /* E-exp */ 137 assert(m == n); 138 advance: printf("MSC: EXP\n"); 139 n = (n+1)%4; 140 assert(m == Nexp); 141 Nexp = (m+1)%4; 142 if 143 :: sender!RDY,n; goto E 144 :: sender!NOTRDY,n; goto N 145 fi 146 } 147 148 :: recv?NODATA(m) -> /* N-exp */ 149 assert(m == n) 150 151 /* Timeout: ignored */ 152 153 /* only the receiver can initiate a data 154 transfer; p. 156 [Needham'82] 155 this is modeled by the statement below: 156 */ 157 :: empty(recv) -> sender!RDY,n; goto E 158 159 :: goto reset 160 od; 161 E: 162 do 163 #if LOSS==1 164 :: recv?_,_ -> progress1: skip 165 #endif 166 :: recv?RESET,0 -> 167 goto ackreset 168 169 :: atomic { recv?DATA(m) -> 170 if 171 :: ((m+1)%4 == n) -> /* E-rep */ 172 printf("MSC: REP\n"); 173 goto retrans 174 :: (m == n) -> /* E-exp */ 175 goto advance 176 fi 177 } 178 179 :: recv?NODATA(m) -> /* N-exp */ 180 assert(m == n); 181 goto I 182 183 /* see also the matching code in the sender model; 184 to check less well-behaved timeout behavior for 185 the receiver process, replace the timeout keyword 186 below with "empty(recv)" (or "skip" for a real 187 torture test, with significant extra complexity) 188 */ 189 :: timeout -> 190 printf("MSC: RTO\n"); 191 retrans: sender!RDY,n; 192 goto E 193 194 :: goto reset 195 od; 196 N: 197 do 198 #if LOSS==1 199 :: recv?_,_ -> progress0: skip 200 #endif 201 :: recv?RESET,0 -> 202 goto ackreset 203 204 :: recv?DATA(m) -> /* E-rep */ 205 assert((m+1)%4 == n); /* E-exp and N-exp: error */ 206 printf("MSC: REP\n"); 207 sender!NOTRDY,n /* retransmit and stay in N */ 208 209 :: sender!RDY,n -> /* buffer ready event */ 210 goto E 211 212 /* Timeout: ignored */ 213 214 :: goto reset 215 od; 216 progress: 217 reset: sender!RESET,0; 218 do 219 #if LOSS==1 220 :: recv?_,_ -> progress3: skip 221 #endif 222 :: recv?t,m -> 223 if 224 :: t == RESET -> n = 0; Nexp = 0; goto I 225 :: else /* ignored, p. 152 */ 226 fi 227 :: timeout -> 228 goto reset 229 od 230 }

7. Sleep-Wakeup Process Scheduling

The model below for implementing sleep and wakeup routines in a distributed operating systems kernel is based on Ruane's description. The model contains an error that can be detected as a fair non-progress cycle (use runtime options -l and -f). Try to determine the cause of the error, and how to fix it. (It can be repaired by the addition of one single statement in the client process.)
1 mtype = { Wakeme, Running }; /* file ex.7 */ 2 3 bit lk, sleep_q; 4 bit r_lock, r_want; 5 mtype State = Running; 6 7 active proctype client() 8 { 9 sleep: /* sleep routine */ 10 atomic { (lk == 0) -> lk = 1 }; /* spinlock(&lk) */ 11 do /* while r->lock */ 12 :: (r_lock == 1) -> /* r->lock == 1 */ 13 r_want = 1; 14 State = Wakeme; 15 lk = 0; /* freelock(&lk) */ 16 (State == Running); /* wait for wakeup */ 17 :: else -> /* r->lock == 0 */ 18 break 19 od; 20 progress: 21 assert(r_lock == 0); /* should still be true */ 22 r_lock = 1; /* consumed resource */ 23 lk = 0; /* freelock(&lk) */ 24 goto sleep 25 } 26 27 active proctype server() /* interrupt routine */ 28 { 29 wakeup: /* wakeup routine */ 30 r_lock = 0; /* r->lock = 0 */ 31 (lk == 0); /* waitlock(&lk) */ 32 if 33 :: r_want -> /* someone is sleeping */ 34 atomic { /* spinlock on sleep queue */ 35 (sleep_q == 0) -> sleep_q = 1 36 }; 37 r_want = 0; 38 #ifdef PROPOSED_FIX 39 (lk == 0); /* waitlock(&lk) */ 40 #endif 41 if 42 :: (State == Wakeme) -> 43 State = Running; 44 :: else -> 45 fi; 46 sleep_q = 0 47 :: else -> 48 fi; 49 goto wakeup 50 }

8. A Leader Election Algorithm

The model below follows the description of the leader election protocol in a unidirectional ring from Dolev et al. as it is discussed and formalized by Raynal.
1 #define N 5 /* nr of processes (use 5 for demos) */ 2 #define I 3 /* node given the smallest number */ 3 #define L 10 /* size of buffer (>= 2*N) */ 4 /* file ex.8 */ 5 mtype = { one, two, winner }; 6 chan q[N] = [L] of { mtype, byte}; 7 8 byte nr_leaders = 0; 9 10 proctype node (chan in, out; byte mynumber) 11 { bit Active = 1, know_winner = 0; 12 byte nr, maximum = mynumber, neighbourR; 13 14 xr in; /* exclusive recv access to channel in */ 15 xs out; /* exclusive send access to channel out */ 16 17 printf("MSC: %d\n", mynumber); 18 out!one(mynumber); 19 end: do 20 :: in?one(nr) -> 21 if 22 :: Active -> 23 if 24 :: nr != maximum -> 25 out!two(nr); 26 neighbourR = nr 27 :: else -> 28 /* max is greatest number */ 29 assert(nr == N); 30 know_winner = 1; 31 out!winner,nr; 32 fi 33 :: else -> 34 out!one(nr) 35 fi 36 37 :: in?two(nr) -> 38 if 39 :: Active -> 40 if 41 :: neighbourR > nr && neighbourR > maximum -> 42 maximum = neighbourR; 43 out!one(neighbourR) 44 :: else -> 45 Active = 0 46 fi 47 :: else -> 48 out!two(nr) 49 fi 50 :: in?winner,nr -> 51 if 52 :: nr != mynumber -> 53 printf("MSC: LOST\n"); 54 :: else -> 55 printf("MSC: LEADER\n"); 56 nr_leaders++; 57 assert(nr_leaders == 1) 58 fi; 59 if 60 :: know_winner 61 :: else -> out!winner,nr 62 fi; 63 break 64 od 65 } 66 67 init { 68 byte proc; 69 atomic { 70 proc = 1; 71 do 72 :: proc <= N -> 73 run node (q[proc-1], q[proc%N], (N+I-proc)%N+1); 74 proc++ 75 :: proc > N -> 76 break 77 od 78 } 79 }

9. A Go-Back-N Sliding Window Protocol

This go-back-n sliding window protocol follows the description from Tanenbaum. The model below includes some annotations to facilitate simulations.
1 #define MaxSeq 3 /* window size */ 2 #define Wrong(x) x = (x+1) % (MaxSeq) 3 #define Right(x) x = (x+1) % (MaxSeq + 1) 4 #define inc(x) Right(x) 5 /* file ex.9 */ 6 chan q[2] = [MaxSeq] of { byte, byte }; /* message passing channel */ 7 8 active [2] proctype p5() /* starts two copies of proctype p5 */ 9 { byte NextFrame, AckExp, FrameExp, r, s, nbuf, i; 10 chan in, out; 11 in = q[_pid]; 12 out = q[1-_pid]; 13 xr in; xs out; /* partial order reduction claims */ 14 15 do 16 :: nbuf < MaxSeq -> /* outgoing messages */ 17 nbuf++; 18 out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 19 inc(NextFrame) 20 21 :: q[_pid]?r,s -> /* incoming messages */ 22 if 23 :: r == FrameExp -> 24 printf("MSC: accept %d\n", r); 25 inc(FrameExp) 26 :: else /* ignore message */ 27 fi; 28 do 29 :: ((AckExp <= s) && (s < NextFrame)) 30 || ((AckExp <= s) && (NextFrame < AckExp)) 31 || ((s < NextFrame) && (NextFrame < AckExp)) -> 32 nbuf--; 33 inc(AckExp) 34 :: else -> break 35 od 36 37 :: timeout -> /* retransmission timeout */ 38 NextFrame = AckExp; 39 printf("MSC: timeout\n"); 40 i = 1; 41 do 42 :: i <= nbuf -> 43 out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 44 inc(NextFrame); 45 i++ 46 :: else -> break 47 od 48 od 49 }
When running the verification with partial order reduction enabled (the default), the verifier will complain about a suspected violation of the exclusive channel access assertions (the xr and xs statements). In this case, the complaint is unjustified. It is caused by the attempt to make the code for sender and receiver equal, and the use of a channel array q[]. The complaint can be supressed by compiling as follows:
$ spin -a ex.9 $ cc -DSAFETY -DXUSAFE -o pan pan.c $ pan -m40000 . . .
The directive -DSAFETY says that we are only interested in safety properties (not LTL properties or cycles). The directive -DXUSAFE tells the verifier that the xr and xs assertions need not be checked.
To reduce the complexity of the model, without affecting its scope, one can add d_step and atomic sequences to the model, as shown in the modified version of this code below.
1 #define MaxSeq 3 /* file ex.9b */ 2 #define MaxSeq_plus_1 4 3 #define inc(x) x = (x + 1) % (MaxSeq + 1) 4 5 chan q[2] = [MaxSeq] of { byte, byte }; 6 7 active [2] proctype p5() 8 { byte NextFrame, AckExp, FrameExp, 9 r, s, nbuf, i; 10 chan in, out; 11 12 d_step { 13 in = q[_pid]; 14 out = q[1-_pid] 15 }; 16 xr in; 17 xs out; 18 19 do 20 :: atomic { nbuf < MaxSeq -> 21 nbuf++; 22 out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 23 printf("MSC: nbuf: %d\n", nbuf); 24 inc(NextFrame) 25 } 26 :: atomic { in?r,s -> 27 if 28 :: r == FrameExp -> 29 printf("MSC: accept %d\n", r); 30 inc(FrameExp) 31 :: else 32 -> printf("MSC: reject\n") 33 fi 34 }; 35 d_step { 36 do 37 :: ((AckExp <= s) && (s < NextFrame)) 38 || ((AckExp <= s) && (NextFrame < AckExp)) 39 || ((s < NextFrame) && (NextFrame < AckExp)) -> 40 nbuf--; 41 printf("MSC: nbuf: %d\n", nbuf); 42 inc(AckExp) 43 :: else -> 44 printf("MSC: %d %d %d\n", AckExp, s, NextFrame); 45 break 46 od; skip 47 } 48 :: timeout -> 49 d_step { 50 NextFrame = AckExp; 51 printf("MSC: timeout\n"); 52 i = 1; 53 do 54 :: i <= nbuf -> 55 out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 56 inc(NextFrame); 57 i++ 58 :: else -> 59 break 60 od; i = 0 61 } 62 od 63 }
Next, we may want to verify that this protocol correctly transfers data, without loss or reordering. The model can be modified as follows to perform these checks. The verifications are based on Wolper's data independence method, using three colored messages (balls). To reduce complexity, we make sure that only one sender transmits the colored balls, and the other checks that they are accepted in the proper sequence. The return direction transmits only dummy balls, and accepts them without check.
1 #define MaxSeq 3 /* file: ex.9c */ 2 #define MaxSeq_plus_1 4 3 #define inc(x) x = (x + 1) % (MaxSeq + 1) 4 5 #define CHECKIT 6 7 #ifdef CHECKIT 8 mtype = { red, white, blue }; /* Wolper's test */ 9 chan source = [0] of { mtype }; 10 chan q[2] = [MaxSeq] of { mtype, byte, byte }; 11 mtype rcvd = white; 12 mtype sent = white; 13 #else 14 chan q[2] = [MaxSeq] of { byte, byte }; 15 #endif 16 17 active [2] proctype p5() 18 { byte NextFrame, AckExp, FrameExp, 19 r, s, nbuf, i; 20 chan in, out; 21 #ifdef CHECKIT 22 mtype ball; 23 byte frames[MaxSeq_plus_1]; 24 #endif 25 26 d_step { 27 in = q[_pid]; 28 out = q[1-_pid] 29 }; 30 31 xr in; 32 xs out; 33 34 do 35 :: atomic { 36 nbuf < MaxSeq -> 37 nbuf++; 38 #ifdef CHECKIT 39 if 40 :: _pid%2 -> source?ball 41 :: else 42 fi; 43 frames[NextFrame] = ball; 44 out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 45 if 46 :: _pid%2 -> sent = ball; 47 :: else 48 fi; 49 #else 50 out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 51 #endif 52 #ifdef VERBOSE 53 printf("MSC: nbuf: %d\n", nbuf); 54 #endif 55 inc(NextFrame) 56 } 57 #ifdef CHECKIT 58 :: atomic { in?ball,r,s -> 59 #else 60 :: atomic { in?r,s -> 61 #endif 62 if 63 :: r == FrameExp -> 64 #ifdef VERBOSE 65 printf("MSC: accept %d\n", r); 66 #endif 67 #ifdef CHECKIT 68 if 69 :: _pid%2 70 :: else -> rcvd = ball 71 fi; 72 #endif 73 inc(FrameExp) 74 :: else 75 #ifdef VERBOSE 76 -> printf("MSC: reject\n") 77 #endif 78 fi 79 }; 80 d_step { 81 do 82 :: ((AckExp <= s) && (s < NextFrame)) 83 || ((AckExp <= s) && (NextFrame < AckExp)) 84 || ((s < NextFrame) && (NextFrame < AckExp)) -> 85 nbuf--; 86 #ifdef VERBOSE 87 printf("MSC: nbuf: %d\n", nbuf); 88 #endif 89 inc(AckExp) 90 :: else -> 91 #ifdef VERBOSE 92 printf("MSC: %d %d %d\n", AckExp, s, NextFrame); 93 #endif 94 break 95 od; 96 skip 97 } 98 :: timeout -> 99 d_step { 100 NextFrame = AckExp; 101 #ifdef VERBOSE 102 printf("MSC: timeout\n"); 103 #endif 104 i = 1; 105 do 106 :: i <= nbuf -> 107 #ifdef CHECKIT 108 if 109 :: _pid%2 -> ball = frames[NextFrame] 110 :: else 111 fi; 112 out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 113 #else 114 out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); 115 #endif 116 inc(NextFrame); 117 i++ 118 :: else -> 119 break 120 od; 121 i = 0 122 } 123 od 124 } 125 #ifdef CHECKIT 126 active proctype Source() 127 { 128 do 129 :: source!white 130 :: source!red -> break 131 od; 132 do 133 :: source!white 134 :: source!blue -> break 135 od; 136 end: do 137 :: source!white 138 od 139 } 140 141 #define sw (sent == white) 142 #define sr (sent == red) 143 #define sb (sent == blue) 144 145 #define rw (rcvd == white) 146 #define rr (rcvd == red) 147 #define rb (rcvd == blue) 148 149 #define LTL 3 150 #if LTL==1 151 152 never { /* ![](sr -> <> rr) */ 153 /* the claims were produced by spin -f and edited */ 154 do 155 :: 1 156 :: !rr && sr -> goto accept 157 od; 158 accept: 159 if 160 :: !rr -> goto accept 161 fi 162 } 163 164 #endif 165 #if LTL==2 166 167 never { /* !rr U rb */ 168 do 169 :: !rr 170 :: rb -> break /* move to implicit 2nd state */ 171 od 172 } 173 174 #endif 175 #if LTL==3 176 177 never { /* (![](sr -> <> rr)) || (!rr U rb) */ 178 179 if 180 :: 1 -> goto T0_S5 181 :: !rr && sr -> goto accept_S8 182 :: !rr -> goto T0_S2 183 :: rb -> goto accept_all 184 fi; 185 accept_S8: 186 if 187 :: !rr -> goto T0_S8 188 fi; 189 T0_S2: 190 if 191 :: !rr -> goto T0_S2 192 :: rb -> goto accept_all 193 fi; 194 T0_S8: 195 if 196 :: !rr -> goto accept_S8 197 fi; 198 T0_S5: 199 if 200 :: 1 -> goto T0_S5 201 :: !rr && sr -> goto accept_S8 202 fi; 203 accept_all: 204 skip 205 } 206 #endif 207 208 #endif

References

Bartlett, K.A., Scantlebury, R.A., and Wilkinson, P.T. `A note on reliable full-duplex transmission over half-duplex lines,' Comm. of the ACM, 1969, Vol. 12, No. 5, 260-265, Figure 3c.
C.H. West, `General technique for communications protocol validation,' IBM J. Res. Develop., 1978, Vol. 22, No. 3, pp. 393-404.
E.W. Dijkstra, `Solution to a problem in concurrent programming control,' Comm. of the ACM, 1965, Vol 8, No. 9, p. 569.
M. Raynal, Algorithms for Mutual Exclusion, MIT Press, Cambridge, Mass., 1986, 107 pgs. (The 1986 edition is a translation from the original French version published in 1984.)
L. Lamport, `The mutual exclusion problem -- parts I and II,' Journal of the ACM, Vol. 33, No. 2, April 1986, pp. 313-347.
G.L. Peterson, `Myths about the mutual exclusion problem,' Inf. Proc. Letters, 1981, Vol. 12, No. 3, pp. 115-116.
G. Berthelot, and R. Terrat, `Petri Net Theory for the correctness of protocols,' IEEE Trans. on Comm., Vol COM-30, No. 12, Dec. 1982, pp. 2497-2505.
R.M. Needham, A.J. Herbert, The Cambridge Distributed Computing System, Addison-Wesley Publ., London, 1982, p. 154.
L.M. Ruane, `Process synchronization in the UTS kernel,' Computing Systems, (Usenix, Summer 1990), Vol. 3, No. 3, pp. 387--421.
D. Dolev, M. Klawe, and M. Rodeh, `An O(n log n) unidirectional distributed algorithm for extrema finding in a circle,' Journal of Algorithms, Vol 3. (1982), pp. 245-260.
M. Raynal, Distributed algorithms and protocols, John Wiley and Sons, New York, 1992.
A. Tanenbaum, Computer Networks, 2nd Ed., Prentice Hall, Englewood Cliffs, NJ., 1989, p. 214, 232-233.
P. Wolper, ``Specifying interesting properties of programs in propositional temporal logic,'' Proc. 13th ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Fla., January 1986, pp. 148-193.

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage (Page Updated: 26 August 1997)