![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to spin.ms CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10dc / vol2 / spin|
Return to spin.ms CVS log | Up to [Research Unix] / researchv10dc / vol2 / spin |
1.1 root 1: .so ../ADM/mac
2: .XX spin 429 "Spin \(em A Protocol Analyzer"
3: .nr dP 2
4: .nr dV 3p
5: .EQ
6: delim @@
7: .EN
8: .de IH \" makes a bold italic sub heading
9: .NH 2
10: \\$1
11: ..
12: .ds P \\s-2PROMELA\\s0
13: .ds S \fISpin\fP
14: .ds s \fIspin\fP
15: .TL
16: Spin \(em A Protocol Analyzer
17: .AU "MH 2C-521" 6335
18: Gerard J. Holzmann
19: .AI
20: .MH
21: .AB
22: \*S is a tool for analyzing the logical consistency of
23: concurrent systems, specifically of data communication protocols.
24: The system is described in a modeling language called \*P.
25: The language allows for the dynamic creation of concurrent processes.
26: Communication via message channels can be defined to be synchronous
27: (i.e., rendez-vous), or asynchronous (i.e., buffered).
28: .PP
29: Given a model system specified in \*P, \*s
30: can either perform random simulations of the system's execution
31: or it can generate a C program that performs a fast exhaustive
32: validation of the system state space.
33: During simulations and validations \*s checks for the absence of deadlocks,
34: unspecified receptions, and unexecutable code.
35: The validator can also be used to verify the correctness of
36: system invariants, and it can find non-progress execution cycles.
37: .PP
38: The validator is setup to be extremely fast and to use
39: only a minimal amount of memory.
40: The exhaustive validations performed by \*s are conclusive,
41: They establish with certainty whether or not a given behavior
42: is error-free.
43: Very large validation runs, that can ordinarily not be
44: performed with automated techniques, can be
45: done in \*s with a novel ``bit state space'' technique.
46: With this method the state space is collapsed to a single
47: bit per system state stored, with minimal side-effects.
48: .PP
49: The first part of this memo gives an introduction to \*P,
50: the second part discusses the usage of \*s, and
51: the third part contains a brief reference manual for \*P.
52: In the appendix an example is used to illustrate the construction
53: of a basic \*P model for \*s validations.
54: .AE
55: .2C
56: .NH
57: Introduction to \*P
58: .PP
59: \*P is a validation modeling language.
60: It provides a vehicle for making abstractions of protocols
61: (or distributed systems in general) that suppress details
62: that are unrelated to process interaction.
63: The intended use of \*s is to validate fractions of process
64: behavior, that for one reason or another is considered suspect.
65: The relevant behavior is modeled in \*P and validated.
66: A complete validation is therefore typically performed in a series of steps,
67: with the construction of increasingly detailed \*P models.
68: Each model can be validated with \*s under different types of
69: assumptions about the environment (e.g., message loss, message
70: duplications etc).
71: Once the correctness of a model has been established with \*s, that
72: fact can be used in the construction and validation of all
73: subsequent models.
74: .PP
75: \*P programs consist of \f2processes\f1,
76: message \f2channels\f1, and \f2variables\f1.
77: Processes are global objects.
78: Message channels and variables can be declared either globally
79: or locally within a process.
80: Processes specify behavior; channels and global variables
81: define the environment in which the processes run.
82: .IH Executability
83: .PP
84: In \*P there is no difference between conditions and
85: statements, even isolated boolean conditions can be used as statements.
86: The execution of every statement is conditional on its
87: .I executability .
88: Statements are either executable or blocked.
89: The executability is the basic means of synchronization.
90: A process can wait for an event to happen by waiting
91: for a statement to become executable.
92: For instance, instead of writing a busy wait loop:
93: .P1 0
94: while (a != b)
95: skip /* wait for a==b */
96: .P2
97: one can achieve the same effect in \*P with the statement
98: .P1 0
99: (a == b)
100: .P2
101: A condition can only be executed (passed) when it holds.
102: If the condition does not hold, execution blocks until it does.
103: .PP
104: Variables are used to store either global information about the
105: system as a whole, or information local to one specific process,
106: depending on where the declaration for the variable is placed.
107: The declarations
108: .P1 0
109: bool flag;
110: int state;
111: byte msg;
112: .P2
113: define variables that can store integer values in
114: three different ranges.
115: The scope of a variable is global if it is declared outside all
116: process declarations, and local if it is declared within a process
117: declaration.
118: .IH "Data Types"
119: .PP
120: Table 1 summarizes the basic data types, sizes,
121: and the corresponding value ranges (on a DEC VAX computer).
122: .KS
123: .SP .5
124: .ps -1
125: .vs -2
126: .TS
127: center;
128: l l l l
129: lFCW n r c.
130: =
131: Name Size (bits) Usage Range
132: _
133: bit 1 unsigned 0..1
134: bool 1 unsigned 0..1
135: byte 8 unsigned 0..255
136: short 16 signed @-2 sup 15@..@{2 sup 15} - 1@
137: int 32 signed @-2 sup 31@..@{2 sup 31} - 1@
138: _
139: .TE
140: .ps +1
141: .vs +2
142: .SP .5
143: .ce
144: \fBTable 1.\fP Data Types
145: .SP
146: .KE
147: The names
148: .CW bit
149: and
150: .CW bool
151: are synonyms for a single bit of information.
152: A
153: .CW byte
154: is an unsigned quantity that can store a value between
155: .CW 0
156: and
157: .CW 255 .
158: .CW short s
159: and
160: .CW int s
161: are signed quantities that
162: differ only in the range of values they can hold.
163: .IH "Array Variables"
164: .PP
165: Variables can be declared as arrays.
166: For instance,
167: .P1 0
168: byte state[N]
169: .P2
170: declares an array of
171: .CW N
172: bytes that can be accessed in statements such as
173: .P1 0
174: state[0] = state[3] + 5 * state[3*2/n]
175: .P2
176: where
177: .CW n
178: is a constant or a variable declared elsewhere.
179: The index to an array can be any expression that
180: determines a unique integer value.
181: The effect of an index value outside the range
182: .CW "0 .. N-1"
183: is undefined; most likely it will cause a runtime error.
184: .PP
185: So far we have seen examples of variable declarations
186: and of two types of statements: boolean conditions and
187: assignments.
188: Declarations and assignments are always \f2executable\f1.
189: Conditions are only executable when they hold.
190: .IH "Process Types"
191: .PP
192: The state of a variable or of a message channel
193: can only be changed or inspected by processes.
194: The behavior of a process is defined in a
195: .CW proctype
196: declaration.
197: The following, for instance, declares a process with one local variable
198: .CW state .
199: .P1 0
200: proctype A()
201: { byte state;
202:
203: state = 3
204: }
205: .P2
206: The process type is named
207: .CW A .
208: The body of the declaration is enclosed in curly braces.
209: The declaration body consists of a list of zero or more
210: declarations of local variables and/or statements.
211: The declaration above contains one local variable declaration
212: and a single statement: an assignment of the
213: value 3 to variable
214: .CW state .
215: .PP
216: The semicolon is a statement \f2separator\f1 (not a statement terminator,
217: hence there is no semicolon after the last statement).
218: \*P accepts two different statement separators:
219: .CW `->'
220: (arrow) and
221: .CW `;' .
222: The two statement separators are equivalent.
223: The arrow is sometimes used as an informal way to indicate a causal
224: relation between two statements.
225: Consider the following example.
226: .P1 0
227: byte state = 2;
228:
229: proctype A()
230: { (state == 1) -> state = 3
231: }
232: .P3
233: proctype B()
234: { state = state \- 1
235: }
236: .P2
237: In this example we declared two types of processes,
238: .CW A
239: and
240: .CW B .
241: Variable
242: .CW state
243: is now a global, initialized to the value two.
244: Process type
245: .CW A
246: contains two statements, separated by an arrow.
247: In the example, process declaration
248: .CW B
249: contains a single statement that decrements
250: the value of the state variable by one.
251: Since the assignment is always executable,
252: processes of type
253: .CW B
254: can always complete without delay.
255: Processes of type
256: .CW A ,
257: however, are delayed at the condition until
258: the variable
259: .CW state
260: contains the proper value.
261: ......
262: .IH "Process Instantiation"
263: .PP
264: A
265: .CW proctype
266: definition only declares process behavior, it
267: does not execute it.
268: Initially, in the \*P model, just one process will be executed:
269: a process of type
270: .CW init ,
271: that must be declared explicitly in every \*P specification.
272: The smallest possible \*P specification, therefore, is:
273: .P1 0
274: init { skip }
275: .P2
276: where
277: .CW skip
278: is a dummy, null statement.
279: More interestingly, however,
280: the initial process can initialize global variables,
281: and instantiate processes.
282: An
283: .CW init
284: declaration for the above system, for instance, could look as follows.
285: .P1 0
286: init
287: { run A(); run B()
288: }
289: .P2
290: .PP
291: .CW run
292: is used as a unary operator that takes the name of a process type (e.g.
293: .CW A ).
294: It is executable only if a process of
295: the type specified can be instantiated.
296: It is unexecutable if this cannot be done,
297: for instance if too many processes are already running.
298: .PP
299: The
300: .CW run
301: statement can pass parameter values of all basic
302: data types to the new process.
303: The declarations are then written, for instance, as follows:
304: .P1 0
305: proctype A(byte state; short foo)
306: {
307: (state == 1) -> state = foo
308: }
309: .P3
310: init
311: {
312: run A(1, 3)
313: }
314: .P2
315: Data arrays or process types can not be passed as parameters.
316: As we will see below, there is just one other data type that
317: can be used as a parameter: a message channel.
318: .PP
319: .CW Run
320: statements can be used in any process to spawn new processes,
321: not just in the initial process.
322: Processes are created with the
323: .CW run
324: statements.
325: An executing process disappears again when it terminates
326: (i.e., reaches the end of the body of its
327: process type declaration), but not before all processes
328: that it started have terminated.
329: .PP
330: With the
331: .CW run
332: statement we can create any number of copies of the process types
333: .CW A
334: and
335: .CW B .
336: If, however, more than one concurrent process is allowed to both read and
337: write the value of a global variable a well-known set of problems
338: can result; for example see |reference(dijkstra concurrent).
339: Consider, for instance, the following system of
340: two processes, sharing access to the global variable
341: .CW state .
342: .P1 0
343: byte state = 1;
344:
345: proctype A()
346: { (state==1) -> state = state+1
347: }
348: .P3
349: proctype B()
350: { (state==1) -> state = state\-1
351: }
352: .P3
353: init
354: { run A(); run B()
355: }
356: .P2
357: If one of the two processes completes before its competitor has
358: started, the other process will block forever on the initial condition.
359: If both pass the condition simultaneously, both will complete, but
360: the resulting value of
361: .CW state
362: is unpredictable.
363: It can be any of the values
364: .CW 0 ,
365: .CW 1 ,
366: or
367: .CW 2 .
368: .PP
369: Many solutions to this problem have been considered, ranging from
370: an abolishment of global variables to the provision of special
371: machine instructions that can guarantee an indivisible test and
372: set sequence on a shared variable.
373: The example below was one of the first solutions published.
374: It is due to the Dutch mathematician Dekker.
375: It grants two processes mutually exclusion access to an arbitrary
376: .I
377: critical section
378: .R
379: in their code, by manipulation three additional global variables.
380: The first four lines in the \*P specification
381: below are C-style macro definitions.
382: The first two macros define
383: .CW true
384: to be a constant value equal to
385: .CW 1
386: and
387: .CW false
388: to be a constant
389: .CW 0 .
390: Similarly,
391: .CW Aturn
392: and
393: .CW Bturn
394: are defined as constants.
395: .P1 0
396: #define true 1
397: #define false 0
398: #define Aturn false
399: #define Bturn true
400:
401: bool x, y, t;
402: .P3
403:
404: proctype A()
405: { x = true;
406: t = Bturn;
407: (y == false || t == Aturn);
408: /* critical section */
409: x = false
410: }
411: .P3
412: proctype B()
413: { y = true;
414: t = Aturn;
415: (x == false || t == Bturn);
416: /* critical section */
417: y = false
418: }
419: .P3
420: init
421: { run A(); run B()
422: }
423: .P2
424: The algorithm can be executed repeatedly and is independent of
425: the relative speeds of the two processes.
426: .IH "Atomic Sequences"
427: .PP
428: In \*P there is also another way to avoid the \f2test and set\f1
429: problem:
430: .CW atomic
431: sequences.
432: By prefixing a sequence of statements enclosed in curly
433: braces with the keyword
434: .CW atomic
435: the user can indicate that the sequence is to be executed
436: as one indivisible unit, non-interleaved with any other
437: processes.
438: It causes a run-time error if any statement, other than
439: the first statement, blocks in an atomic sequence.
440: This is how we can use atomic sequences to protect the
441: concurrent access to the global variable
442: .CW state
443: in the earlier example.
444: .P1 0
445: byte state = 1;
446:
447: proctype A()
448: { atomic {
449: (state==1) -> state = state+1
450: }
451: }
452: .P3
453: proctype B()
454: { atomic {
455: (state==1) -> state = state\-1
456: }
457: }
458: .P3
459: init
460: { run A(); run B()
461: }
462: .P2
463: In this case the final value of
464: .CW state
465: is guaranteed to be zero, though during the execution of
466: .CW A
467: and
468: .CW B
469: the intermediate value can be either
470: .CW 0
471: or
472: .CW 2 .
473: .PP
474: Atomic sequences can be an important tool in reducing
475: the complexity of validation models.
476: Note that atomic sequence restricts the amount of
477: interleaving that is allowed in a distributed system.
478: Otherwise untractable models can be made tractable
479: by, for instance, labeling all manipulations of local variables
480: with atomic sequences.
481: The reduction in complexity can be dramatic.
482: .IH "Message Passing"
483: .PP
484: Message channels are used to model the transfer of data
485: from one process to another.
486: They are declared either locally or globally,
487: for instance as follows:
488: .P1 0
489: chan qname[16] of { short }
490: .P2
491: This declares a channel that can store up
492: to 16 messages of type
493: .CW short .
494: Channel names can be passed from one process to another via
495: channels or as parameters in process instantiations.
496: If the messages to be passed by the channel have more than
497: one field, the declaration may look as follows:
498: .P1 0
499: chan qname[16] of { byte, int, chan, byte }
500: .P2
501: This time each message in the channel stores up to
502: sixteen messages, each consisting of two 8-bit values,
503: one 32-bit value, and a channel name.
504: .PP
505: .Tm ! S
506: .Tm ? S
507: The statement
508: .P1 0
509: qname!expr
510: .P2
511: sends the value of expression
512: .CW expr
513: to the channel that we just created, that is:
514: it appends the value to the tail of the channel.
515: .P1 0
516: qname?msg
517: .P2
518: receives the message, it retrieves it from the head of the channel,
519: and stores it in a variable
520: .CW msg .
521: The channels pass messages in first-in-first-out order.
522: In the above cases only a single value
523: is passed through the channel.
524: If more than one value is to be transferred per message,
525: they are specified in a comma separated list
526: .P1 0
527: qname!expr1,expr2,expr3
528: qname?var1,var2,var3
529: .P2
530: If more parameters are sent per message then the message channel
531: can store, the redundant parameters are lost without warning.
532: If fewer parameters are sent then the message channel can store,
533: the value of the remaining parameters is undefined.
534: Similarly, if the receive operation tries to retrieve more
535: parameters than available, the value of the extra parameters is
536: undefined; if it receives fewer than the number of parameters
537: that was sent, the extra information is lost.
538: .PP
539: By convention, the first message field is often
540: used to specify the message type (i.e. a constant).
541: An alternative, and equivalent, notation for the
542: send and receive operations is therefore to specify the
543: message type, followed by a list of message fields
544: enclosed in braces.
545: In general:
546: .P1 0
547: qname!expr1(expr2,expr3)
548: qname?var1(var2,var3)
549: .P2
550: .PP
551: The send operation is executable only when the channel addressed is not full.
552: The receive operation, similarly, is only executable
553: when the channel is non empty.
554: Optionally, some of the arguments of the receive operation
555: can be constants:
556: .P1 0
557: qname?cons1,var2,cons2
558: .P2
559: in this case, a further condition on the executability of the
560: receive operation is that the value of all message fields that are
561: specified as constants match the value of the corresponding fields
562: in the message that is at the head of the channel.
563: Again, nothing bad will happen if a statement happens to be non-executable.
564: The process trying to execute it will be delayed until the
565: statement, or, more likely, an alternative statement, becomes executable.
566: .PP
567: Here is an example that uses some of the mechanisms introduced
568: so far.
569: .P1 0
570: proctype A(chan q1)
571: { chan q2;
572: q1?q2;
573: q2!123
574: }
575: .P3
576: proctype B(chan qforb)
577: { int x;
578: qforb?x;
579: printf("x = %d\n", x)
580: }
581: .P3
582: init {
583: chan qname[1] of { chan };
584: chan qforb[1] of { int };
585: run A(qname);
586: run B(qforb);
587: qname!qforb
588: }
589: .P2
590: The value printed will be
591: .CW 123 .
592: .PP
593: A predefined function
594: .CW len(qname)
595: returns the number of messages currently
596: stored in channel
597: .CW qname .
598: Note that if
599: .CW len
600: is used as a statement, rather than on
601: the right hand side of an assignment, it will be unexecutable if
602: the channel is empty: it returns a zero result, which by definition
603: means that the statement is temporarily unexecutable.
604: Composite conditions such as
605: .P1 0
606: (qname?var == 0)
607: .P2
608: or
609: .P1 0
610: (a > b && qname!123)
611: .P2
612: are invalid in \*P (note that these conditions can not be evaluated
613: without side-effects).
614: For a receive statement there is an alternative, using square
615: brackets around the clause behind the question mark.
616: .P1 0
617: qname?[ack,var]
618: .P2
619: is evaluated as a condition.
620: It returns
621: .CW 1
622: if the corresponding receive statement
623: .P1 0
624: qname?ack,var
625: .P2
626: is executable, i.e., if there is indeed a message
627: .CW ack
628: at the head of the channel.
629: It returns
630: .CW 0
631: otherwise.
632: In neither case has the evaluation of a statement such as
633: .P1 0
634: qname?[ack,var]
635: .P2
636: any side-effects: the receive is evaluated, not executed.
637: .PP
638: Note carefully that in non-atomic sequences of two statements such as
639: .P1 0
640: (len(qname) < MAX) -> qname!msgtype
641: .P2
642: or
643: .P1 0
644: qname?[msgtype] -> qname?msgtype
645: .P2
646: the second statement is not \f2necessarily\f1 executable
647: after the first one has been executed.
648: There may be race conditions if access to the channels
649: is shared between several processes.
650: In the first case
651: another process can send a message to channel
652: .CW qname
653: just after this process determined that the channel was not full.
654: In the second case, the other process can steal away the
655: message just after our process determined its presence.
656: .IH "Rendez-Vous Communication"
657: .PP
658: So far we have talked about asynchronous communication between processes
659: via message channels, declared in statements such as
660: .P1 0
661: chan qname [N] of { byte }
662: .P2
663: where
664: .CW N
665: is a positive constant that defines the buffer size.
666: A logical extension is to allow for the declaration
667: .P1 0
668: chan port [0] of { byte }
669: .P2
670: to define a rendez-vous port that can pass single byte messages.
671: The channel size is zero, that is, the channel
672: .CW port
673: can pass, but can not store messages.
674: Message interactions via such rendez-vous ports are
675: by definition synchronous.
676: Consider the following example.
677: .P1 0
678: #define msgtype 33
679:
680: chan name [0] of { byte, byte };
681:
682: proctype A()
683: { name!msgtype(124);
684: name!msgtype(121)
685: }
686: .P3
687: proctype B()
688: { byte state;
689: name?msgtype(state)
690: }
691: .P3
692: init
693: { atomic { run A(); run B() }
694: }
695: .P2
696: Channel
697: .CW name
698: is a global rendez-vous port.
699: The two processes will synchronously execute their first statement:
700: a handshake on message
701: .CW msgtype
702: and a transfer of the value 124 to local variable
703: .CW state .
704: The second statement in process
705: .CW A
706: will be unexecutable,
707: because there is no matching receive operation in process
708: .CW B .
709: .PP
710: If the channel
711: .CW name
712: is defined with a non-zero buffer capacity,
713: the behavior is different.
714: If the buffer size is at least 2, the process of type
715: .CW A
716: can complete its execution, before its peer even starts.
717: If the buffer size is 1, the sequence of events is as follows.
718: The process of type
719: .CW A
720: can complete its first send action, but it blocks on the
721: second, because the channel is now filled to capacity.
722: The process of type
723: .CW B
724: can then retrieve the first message and complete.
725: At this point
726: .CW A
727: becomes executable again and completes,
728: leaving its last message as a residual in the channel.
729: .PP
730: Rendez-vous communication is binary: only two processes,
731: a sender and a receiver, can be synchronized in a
732: rendez-vous handshake.
733: We will see an example of a way to exploit this to
734: build a semaphore below.
735: But first, let us introduce a few more control flow structures
736: that may be useful.
737: .NH 2
738: Control Flow
739: .PP
740: Between the lines, we have already introduced three ways of
741: defining control flow: concatenation of statements
742: within a process, parallel execution of processes, and
743: atomic sequences.
744: There are three other control flow constructs in \*P to be discussed.
745: They are case selection,
746: repetition, and
747: unconditional jumps.
748: .NH 3
749: Case Selection
750: .PP
751: The simplest construct is the selection structure.
752: Using the relative values of two variables
753: .CW a
754: and
755: .CW b
756: to choose between two options, for instance, we can write:
757: .P1 0
758: if
759: :: (a != b) -> option1
760: :: (a == b) -> option2
761: fi
762: .P2
763: The selection structure contains two execution sequences,
764: each preceded by a double colon.
765: Only one sequence from the list will be executed.
766: A sequence can be selected only if its first statement is executable.
767: The first statement is therefore called a \f2guard\f1.
768: .PP
769: In the above example the guards are mutually exclusive, but they
770: need not be.
771: If more than one guard is executable, one of the corresponding sequences
772: is selected nondeterministically.
773: If all guards are unexecutable the process will block until at least
774: one of them can be selected.
775: There is no restriction on the type of statements that can be used
776: as a guard.
777: The following example, for instance, uses input statements.
778: .P1 0
779: #define a 1
780: #define b 2
781:
782: chan ch[1] of { byte };
783:
784: proctype A()
785: { ch!a
786: }
787: .P3
788: proctype B()
789: { ch!b
790: }
791: .P3
792: proctype C()
793: { if
794: :: ch?a
795: :: ch?b
796: fi
797: }
798: .P3
799: init
800: { atomic { run A(); run B(); run C() }
801: }
802: .P2
803: The example defines three processes and one channel.
804: The first option in the selection structure of the process
805: of type
806: .CW C
807: is executable if the channel contains
808: a message
809: .CW a ,
810: where
811: .CW a
812: is a constant with value
813: .CW 1 ,
814: defined in a macro definition at the start of the program.
815: The second option is executable if it contains a message
816: .CW b ,
817: where, similarly,
818: .CW b
819: is a constant.
820: Which message will be available depends on the unknown
821: relative speeds of the processes.
822: .PP
823: A process of the following type will either increment
824: or decrement the value of variable
825: .CW count
826: once.
827: .P1 0
828: byte count;
829:
830: proctype counter()
831: {
832: if
833: :: count = count + 1
834: :: count = count \- 1
835: fi
836: }
837: .P2
838: .NH 3
839: Repetition
840: .PP
841: A logical extension of the selection structure is
842: the repetition structure.
843: We can modify the above program as follows, to obtain
844: a cyclic program that randomly changes the value of
845: the variable up or down.
846: .P1 0
847: byte count;
848:
849: proctype counter()
850: {
851: do
852: :: count = count + 1
853: :: count = count \- 1
854: :: (count == 0) -> break
855: od
856: }
857: .P2
858: .PP
859: Only one option can be selected for execution at a time.
860: After the option completes, the execution of the structure
861: is repeated.
862: The normal way to terminate the repetition structure is
863: with a
864: .CW break
865: statement.
866: In the example, the loop can be
867: broken when the count reaches zero.
868: Note, however, that it need
869: not terminate since the other two options always remain executable.
870: To force termination we could modify the program as follows.
871: .P1 0
872: proctype counter()
873: {
874: do
875: :: (count != 0) ->
876: if
877: :: count = count + 1
878: :: count = count \- 1
879: fi
880: :: (count == 0) -> break
881: od
882: }
883: .P2
884: .NH 3
885: Unconditional Jumps
886: .PP
887: Another way to break the loop is with an unconditional jump:
888: the infamous
889: .CW goto
890: statement.
891: This is illustrated in the following implementation of Euclid's algorithm for
892: finding the greatest common divisor of two non-zero, positive numbers:
893: .P1 0
894: proctype Euclid(int x, y)
895: {
896: do
897: :: (x > y) -> x = x \- y
898: :: (x < y) -> y = y \- x
899: :: (x == y) -> goto done
900: od;
901: done:
902: skip
903: }
904: .P2
905: The
906: .CW goto
907: in this example jumps to a label named
908: .CW done .
909: A label can only appear before a statement.
910: Above we want to jump to the end of the program.
911: In this case a dummy statement
912: .CW skip
913: is useful: it is a place holder that
914: is always executable and has no effect.
915: The
916: .CW goto
917: is also always executable.
918: .PP
919: The following example specifies a filter that receives
920: messages from a channel
921: .CW in
922: and divides them over two channels
923: .CW large
924: and
925: .CW small
926: depending on the values attached.
927: The constant
928: .CW N
929: is defined to be
930: .CW 128
931: and
932: .CW size
933: is defined to be
934: .CW 16
935: in the two macro definitions.
936: .P1 0
937: #define N 128
938: #define size 16
939: .P3
940:
941: chan in [size] of { short };
942: chan large [size] of { short };
943: chan small [size] of { short };
944: .P3
945:
946: proctype split()
947: { short cargo;
948:
949: do
950: :: in?cargo ->
951: if
952: :: (cargo >= N) ->
953: large!cargo
954: :: (cargo < N) ->
955: small!cargo
956: fi
957: od
958: }
959: .P3
960: init
961: { run split()
962: }
963: .P2
964: A process type that merges the two streams back into one, most
965: likely in a different order, and writes it back
966: into the channel
967: .CW in
968: could be specified as follows.
969: .P1 0
970: proctype merge()
971: { short cargo;
972:
973: do
974: :: if
975: :: large?cargo
976: :: small?cargo
977: fi;
978: in!cargo
979: od
980: }
981: .P2
982: If we now modify the
983: .CW init
984: process as follows, the
985: split and merge processes could busily perform their
986: duties forever on.
987: .P1 0
988: init
989: { in!345; in!12; in!6777;
990: in!32; in!0;
991: run split();
992: run merge()
993: }
994: .P2
995: .PP
996: As a final example, consider the following implementation of
997: a Dijkstra semaphore, using binary rendez-vous communication.
998: .P1 0
999: #define p 0
1000: #define v 1
1001:
1002: chan sema[0] of { bit };
1003: .P3
1004: proctype dijkstra()
1005: { byte count = 1;
1006:
1007: do
1008: :: (count == 1) \->
1009: sema!p; count = 0
1010: :: (count == 0) \->
1011: sema?v; count = 1
1012: od
1013: }
1014: .P3
1015: proctype user()
1016: { do
1017: :: sema?p;
1018: /* critical section */
1019: sema!v;
1020: /* non-critical section */
1021: od
1022: }
1023: .P3
1024: init
1025: { run dijkstra();
1026: run user();
1027: run user();
1028: run user()
1029: }
1030: .P2
1031: The semaphore guarantees that only one of the user processes
1032: can enter its critical section at a time.
1033: It does not necessarily prevent the monopolization of
1034: the access to the critical section by one of the processes.
1035: .IH "Modeling Procedures and Recursion"
1036: .PP
1037: Procedures can be modeled as processes, even recursive ones.
1038: The return value can be passed back to the calling process
1039: via a global variable, or via a message.
1040: The following program illustrates this.
1041: .P1 0
1042: proctype fact(int n; chan p)
1043: { chan child[1] of { int };
1044: int result;
1045:
1046: if
1047: :: (n <= 1) -> p!1
1048: :: (n >= 2) ->
1049: run fact(n-1, child);
1050: child?result;
1051: p!n*result
1052: fi
1053: }
1054: init
1055: { chan child [1] of { int };
1056: int result;
1057:
1058: run fact(7, child);
1059: child?result;
1060: printf("result: %d\n", result)
1061: }
1062: .P2
1063: The process
1064: .I "fact(n, p)"
1065: recursively calculates the factorial of
1066: .I n ,
1067: communicating the result via a message to its parent process
1068: .I p .
1069: .IH "Timeouts"
1070: .PP
1071: We have already discussed two types of statement
1072: with a predefined meaning in \*P:
1073: .CW skip ,
1074: and
1075: .CW break .
1076: Another predefined statement is
1077: .CW timeout .
1078: The
1079: .CW timeout
1080: models a special condition that allows a process to
1081: abort the waiting for a condition that may never become true, e.g.
1082: an input from an empty channel.
1083: The timeout keyword is a modeling feature in \*P that provides an
1084: escape from a hang state.
1085: The timeout condition becomes true only when no other
1086: statements within the distributed system is executable.
1087: Note that we deliberately abstract from absolute timing
1088: considerations, which is crucial in validation work,
1089: and we do not specify how the timeout should be implemented.
1090: A simple example is the following process that will send
1091: a reset message to a channel named \f2guard\f1 whenever the
1092: system comes to a standstill.
1093: .P1 0
1094: proctype watchdog()
1095: {
1096: do
1097: :: timeout -> guard!reset
1098: od
1099: }
1100: .P2
1101: .IH "Assertions"
1102: .PP
1103: Another important language construct in \*P that
1104: needs little explanation is the
1105: .CW assert
1106: statement.
1107: Statements of the form
1108: .P1 0
1109: assert(any_boolean_condition)
1110: .P2
1111: are always executable.
1112: If the boolean condition specified holds, the statement has no effect.
1113: If, however, the condition does not necessarily hold,
1114: the statement will produce an error report during validations with \*s.
1115: .NH 2
1116: More Advanced Usage
1117: .PP
1118: The modeling language has a few features that specifically address
1119: the validation aspects.
1120: It shows up in the way labels are used, in the
1121: semantics of the \*P
1122: .CW timeout
1123: statement, and in the usage of statements such as
1124: \f(CWassert\f1 that we discuss next.
1125: .NH 3
1126: End-State Labels
1127: .PP
1128: When \*P is used as a validation language the user must
1129: be able to make very specific assertions about the behavior
1130: that is being modeled.
1131: In particular, if a \*P is checked for the presence of
1132: deadlocks, the validator must be able to distinguish a normal \f2end state\f1
1133: from an abnormal one.
1134: .PP
1135: A normal end state could be a state in which every \*P process
1136: that was instantiated has properly reached the end of the
1137: defining program body, and all message channels are empty.
1138: But, not all \*P process are, of course, meant to reach the
1139: end of their program body.
1140: Some may very well linger in an \f(CWIDLE\f1
1141: state, or they may sit patiently in a loop
1142: ready to spring into action when new input arrives.
1143: .PP
1144: To make it clear to the validator that these alternate end states
1145: are legal, and do not constitute a deadlock, a \*P model can use
1146: end state labels.
1147: For instance, if by adding a label to the process type
1148: \f(CWdijkstra()\f1, from section 1.9:
1149: .P1
1150: proctype dijkstra()
1151: { byte count = 1;
1152:
1153: end: do
1154: :: (count == 1) \->
1155: sema!p; count = 0
1156: :: (count == 0) \->
1157: sema?v; count = 1
1158: od
1159: }
1160: .P2
1161: we indicate that it is not an error if, at the end of an
1162: execution sequence, a process of type \f(CWdijkstra()\f1
1163: has not reached its closing curly brace, but waits in the loop.
1164: Of course, such a state could still be part of a deadlock state, but
1165: if so, it is not caused by this particular process.
1166: (It will still be reported if any one of the other processes
1167: in not in a valid end-state).
1168: .PP
1169: There may be more than one end state label per validation model.
1170: If so, all labels that occur within the same process body must
1171: be unique.
1172: The rule is that every label name that \f2starts\f1 with the three
1173: character sequence \f(CW"end"\f1
1174: is an endstate label.
1175: So it is perfectly valid to use variations such as
1176: \f(CWenddne\f1, \f(CWend0\f1, \f(CWend_appel\f1, etc.
1177: .NH 3
1178: Progress-State Labels
1179: .PP
1180: In the same spirit as the end state labels, the user can also
1181: define \f2progress state\f1 labels.
1182: In this case, a progress state labels will mark a state that
1183: \f2must\f1 be executed for the protocol to make progress.
1184: Any infinite cycle in the protocol execution that does not
1185: pass through at least one of these progress states, is a
1186: potential starvation loop.
1187: In the
1188: .CW dijkstra
1189: example, for instance, we can label the
1190: successful passing of a semaphore test as ``progress'' and
1191: ask a validator to make sure that there is no cycle in the
1192: protocol execution where at least one process succeeds in
1193: passing the semaphore guard.
1194: If more than one state carries a progress label,
1195: variations with a common prefix are again valid:
1196: \f(CWprogress0\f1, \f(CWprogress_foo\f1, etc.
1197: .KF
1198: .P1
1199: proctype dijkstra()
1200: { byte count = 1;
1201:
1202: end: do
1203: :: (count == 1) ->
1204: progress: sema!p; count = 0
1205: :: (count == 0) ->
1206: sema?v; count = 1
1207: od
1208: }
1209: .P2
1210: .KE
1211: .PP
1212: .CW "spin -a"
1213: generates analyzers that support (after compilation) a
1214: .CW -l
1215: option, which makes the analyzer use a fast search for non-progress loops,
1216: instead of the default search for deadlocks.
1217: The
1218: .CW -l
1219: search completely avoids the expense of a
1220: full construction of all strongly
1221: connected components in the reachability graph
1222: (the conventional method for doing loop analysis).
1223: The expense is therefore never more than about
1224: twice the time and memory requirements of
1225: a default search for deadlocks.
1226: .IH "Message Type Definitions"
1227: .PP
1228: We have seen how variables are declared and how constants
1229: can be defined using C-style macros.
1230: As a mild form of syntactic sugar, \*P also allows for
1231: message type definitions that look as follows:
1232: .P1 0
1233: mtype = {
1234: ack, nak, err,
1235: next, accept
1236: }
1237: .P2
1238: This is a preferred way of specifying the message types since
1239: it abstracts from the specific values to be used, and it makes
1240: the names of the constants available to an implementation,
1241: which can improve error reporting.
1242: .IH "Pseudo Statements"
1243: .PP
1244: We have now discussed all the basic types of statements defined in \*P:
1245: assignments, conditions, send and receive,
1246: .CW assert ,
1247: .CW timeout ,
1248: .CW goto ,
1249: .CW break
1250: and
1251: .CW skip .
1252: Note that
1253: .CW chan ,
1254: .CW len
1255: and
1256: .CW run
1257: are not really statements but unary operators that can be used in
1258: conditions and assignments.
1259: .PP
1260: The
1261: .CW skip
1262: statement was mentioned in passing as a statement that can be
1263: a useful filler to satisfy syntax requirements, but that really
1264: has no effect.
1265: It is formally not part of the language but a \f2pseudo-statement\f1,
1266: merely a synonym of another statement with the same effect: a
1267: simple condition of a constant value
1268: .CW (1) .
1269: In the same spirit other pseudo-statements could be
1270: defined, such as
1271: \f(CWblock\f1 or \f(CWhang\f1, equivalents of \f(CW(0)\f1,
1272: and
1273: \f(CWhalt\f1, as an equivalent of \f(CWassert(0)\f1..
1274: .IH Example
1275: .PP
1276: Here is a simple example of a (flawed) protocol, modeled in \*P.
1277: .P1 0
1278: mtype = {
1279: ack, nak, err, next, accept
1280: }
1281:
1282: .P3
1283: proctype transfer(chan in,out,chin,chout)
1284: { byte o, i;
1285:
1286: in?next(o);
1287: .P3
1288: do
1289: :: chin?nak(i) ->
1290: out!accept(i);
1291: chout!ack(o)
1292: .P3
1293: :: chin?ack(i) ->
1294: out!accept(i);
1295: in?next(o);
1296: chout!ack(o)
1297: .P3
1298: :: chin?err(i) ->
1299: chout!nak(o)
1300: od
1301: }
1302:
1303: .P3
1304: init
1305: { chan AtoB[1] of { byte, byte };
1306: chan BtoA[1] of { byte, byte };
1307: .P3
1308: chan Ain [2] of { byte };
1309: chan Bin [2] of { byte };
1310: .P3
1311: chan Aout[2] of { byte };
1312: chan Bout[2] of { byte };
1313: .P3
1314: atomic {
1315: run transfer(Ain,Aout, AtoB,BtoA);
1316: run transfer(Bin,Bout, BtoA,AtoB)
1317: };
1318: .P3
1319: AtoB!err(0)
1320: }
1321: .P2
1322: The channels
1323: .CW Ain
1324: and
1325: .CW Bin
1326: are to be filled with
1327: token messages of type
1328: .CW next
1329: and arbitrary values (e.g.
1330: ASCII character values) by unspecified background processes:
1331: the users of the transfer service.
1332: Similarly, these user processes
1333: can read received data from the channels
1334: .CW Aout
1335: and
1336: .CW Bout .
1337: The channels and processes are initialized in a single
1338: atomic statement, and started with the dummy
1339: .CW err
1340: message.
1341: .NH
1342: Introduction to Spin
1343: .PP
1344: Given a model system specified in \*P, \*s
1345: can either perform random simulations of the system's execution
1346: or it can generate a C program that performs a fast exhaustive
1347: validation of the system state space.
1348: The validator can check, for instance, if user specified system
1349: invariants may be violated during a protocol's execution.
1350: .PP
1351: If \*s is invoked without any options it performs a random simulation.
1352: With option
1353: .CW -n\fIN
1354: the seed for the simulation is set explicitly to the integer value
1355: .I N .
1356: .PP
1357: The options
1358: .CW pglrs
1359: controls the amount of information output from the simulation run.
1360: Every line of output normally contains a reference to the source
1361: line in the specification that caused it.
1362: .IP \f(CW-p\f1
1363: Shows the state changes of the \*P
1364: processes at every time step.
1365: .IP \f(CW-g\f1
1366: Shows the current value of global variables at every time step.
1367: .IP \f(CW-l\f1
1368: Shows the current value of local variables, after the
1369: process that owns them has changed state.
1370: It is best used in combination with option
1371: .CW -p .
1372: .IP \f(CW-r\f1
1373: Shows all message receive events.
1374: It shows the process performing the receive, its name and number,
1375: the source line number, the message parameter number (there is
1376: one line for each parameter), the message type and the message
1377: channel number and name.
1378: .IP \f(CW-s\f1
1379: Shows all message send events.
1380: .LP
1381: \*S understands four other options:
1382: .IP \f(CW-a\f1
1383: Generates a protocol specific analyzer.
1384: The output is written into a set of C files, named
1385: .CW pan.[cbhmt] ,
1386: that can be compiled to produce the analyzer
1387: (which is then executed to perform the analysis).
1388: To guarantee an exhaustive exploration of the state space, the
1389: program can be compiled simply as
1390: .RS
1391: .IP
1392: .P1
1393: $ cc -o run pan.c
1394: .P2
1395: .RE
1396: .IP
1397: For larger systems this may, however, exhaust the available memory
1398: on the machine used.
1399: Large to very large systems can still be analyzed by using a
1400: memory efficient bit state space method by
1401: .RS
1402: .IP
1403: .P1
1404: $ cc -DBITSTATE -o run pan.c
1405: .P2
1406: .RE
1407: .IP
1408: An indication of the coverage of such a search can be derived from the
1409: .I "hash factor"
1410: (see below).
1411: The generated executable analyzer, named
1412: .CW run
1413: above, has its own set of options that can be seen by typing
1414: .CW "run -?"
1415: (see also below in ``The Analyzer'').
1416: .IP \f(CW-m\f1
1417: can be used to change the default semantics of send actions.
1418: Normally, a send operation is only executable if the target channel
1419: is non-full.
1420: This imposes an implicit synchronization that can not always
1421: be justified.
1422: Option \f(CW-m\f1 causes send actions to be always executable.
1423: Messages sent to a channel that is full are then dropped.
1424: If this option is combined with \f(CW-a\f1 the semantics of send
1425: in the analyzers generated is similarly altered, and the validations
1426: will take the effects of this type of message loss into consideration.
1427: .IP \f(CW-q\f1
1428: causes \*s to peruse the model for obviously atomicable
1429: sequences, and to label them appropriately, in an effort to
1430: reduce the complexity of large validation runs.
1431: Typically, the user can do better by hand (by being more
1432: daring than \*s can be in this case).
1433: .IP \f(CW-t\f1
1434: is a trail-hunting option.
1435: If the analyzer finds a violation of an assertion, a deadlock or
1436: an unspecified reception, it writes an error trail into a file
1437: named
1438: .CW pan.trail .
1439: The trail can be inspected in detail by invoking \*s with the
1440: .CW -t
1441: option.
1442: In combination with the options
1443: .CW pglrs
1444: different views of the error sequence are then easily obtained.
1445: .PP
1446: For brevity, other features of \*s are not discussed here.
1447: For details see|reference(holzmann spinbook), for a hint of
1448: what else is available, see ``Digging Deeper'' at the end of this manual.
1449: .IH "The Simulator"
1450: .PP
1451: Consider the following example protocol, that we will store in a
1452: file named
1453: .CW lynch .
1454: .P1 0
1455: 1 #define MIN 9
1456: 2 #define MAX 12
1457: 3 #define FILL 99
1458: 4
1459: 5 mtype = { ack, nak, err }
1460: 6
1461: .P3
1462: 7 proctype transfer(chan chin, chout)
1463: 8 { byte o, i, last_i=MIN;
1464: 9
1465: 10 o = MIN+1;
1466: .P3
1467: 11 do
1468: 12 :: chin?nak(i) ->
1469: 13 assert(i == last_i+1);
1470: 14 chout!ack(o)
1471: .P3
1472: 15 :: chin?ack(i) ->
1473: 16 if
1474: 17 :: (o < MAX) -> o = o+1
1475: 18 :: (o >= MAX) -> o = FILL
1476: 19 fi;
1477: 20 chout!ack(o)
1478: .P3
1479: 21 :: chin?err(i) ->
1480: 22 chout!nak(o)
1481: 23 od
1482: 24 }
1483: 25
1484: .P3
1485: 26 proctype channel(chan in, out)
1486: 27 { byte md, mt;
1487: 28 do
1488: 29 :: in?mt,md ->
1489: 30 if
1490: 31 :: out!mt,md
1491: 32 :: out!err,0
1492: 33 fi
1493: 34 od
1494: 35 }
1495: 36
1496: .P3
1497: 37 init
1498: 38 { chan AtoB[1] of { byte, byte };
1499: 39 chan BtoC[1] of { byte, byte };
1500: 40 chan CtoA[1] of { byte, byte };
1501: 41 atomic {
1502: 42 run transfer(AtoB, BtoC);
1503: 43 run channel(BtoC, CtoA);
1504: 44 run transfer(CtoA, AtoB)
1505: 45 };
1506: 46 AtoB!err,0; /* start */
1507: 47 0 /* hang */
1508: 48 }
1509: .P2
1510: The protocol uses three message types: \f2ack\f1, \f2nak\f1, and
1511: a special type \f2err\f1 that is used to model message distortions
1512: on the communication channel between the two transfer processes.
1513: The behavior of the channel is modeled explicitly with a channel
1514: process.
1515: There is also an
1516: .CW assert
1517: statement that claims a (faulty) invariant
1518: relation between two local variables in the transfer processes.
1519: .PP
1520: Running \*s without options gives us a random simulation that
1521: will only provide output when execution terminates, or if
1522: a \f2printf\f1 statement is encountered.
1523: In this case:
1524: .P1 0
1525: $ spin lynch
1526: spin: "lynch" line 13: assertion violated
1527: #processes: 4
1528: proc 3 (transfer) line 11 (state 15)
1529: proc 2 (channel) line 28 (state 6)
1530: proc 1 (transfer) line 13 (state 3)
1531: proc 0 (:init:) line 48 (state 6)
1532: 4 processes created
1533: $
1534: .P2
1535: There are no \f2printf\f1's in the specification, but execution
1536: halts on an assertion violation.
1537: Curious to find out more, we can repeat the run with more verbose
1538: output, e.g. printing all receive events.
1539: The result of that run is shown in Figure 1.
1540: Most output will be self-explanatory.
1541: .PP
1542: The above simulation run ends in the same assertion violation.
1543: Since the simulation resolves nondeterministic choices in a
1544: random manner, this need not always be the case.
1545: To force a reproducible run, the option
1546: .CW -n\fIN
1547: can be used.
1548: For instance:
1549: .P1 0
1550: $ spin -r -n100 lynch
1551: .P2
1552: will seed the random number generator with the integer value 100
1553: and is guaranteed to produce the same output each time it is executed.
1554: .PP
1555: The other options can add still more output to the simulation run,
1556: but the amount of text can quickly become overwhelming.
1557: An easy solution is to filter the output through \f2grep\f1.
1558: For instance, if we are only interested in the behavior of the
1559: channel process in the above example, we say:
1560: .P1 0
1561: $ spin -n100 -r lynch | grep "proc 2"
1562: .P2
1563: The results are shown in Figure 1.
1564: .1C
1565: .KF
1566: .nf
1567: .ps -2
1568: .vs -3p
1569: .ft CW
1570: .TS
1571: box expand;
1572: l
1573: l.
1574: $ spin -r lynch
1575: proc 1 (transfer) line 21, Recv err,0 <- queue 1 (chin)
1576: proc 2 (channel) line 29, Recv nak,10 <- queue 2 (in)
1577: proc 3 (transfer) line 12, Recv nak,10 <- queue 3 (chin)
1578: proc 1 (transfer) line 15, Recv ack,10 <- queue 1 (chin)
1579: \&...
1580: proc 1 (transfer) line 15, Recv ack,12 <- queue 1 (chin)
1581: proc 2 (channel) line 29, Recv ack,99 <- queue 2 (in)
1582: proc 3 (transfer) line 15, Recv ack,99 <- queue 3 (chin)
1583: proc 1 (transfer) line 15, Recv ack,99 <- queue 1 (chin)
1584: proc 2 (channel) line 29, Recv ack,99 <- queue 2 (in)
1585: proc 3 (transfer) line 21, Recv err,0 <- queue 3 (chin)
1586: proc 1 (transfer) line 12, Recv nak,99 <- queue 1 (chin)
1587: spin: "lynch" line 13: assertion violated
1588: #processes: 4
1589: proc 3 (transfer) line 11 (state 15)
1590: proc 2 (channel) line 28 (state 6)
1591: proc 1 (transfer) line 13 (state 3)
1592: proc 0 (:init:) line 48 (state 6)
1593: 4 processes created
1594: $ spin -n100 -r lynch | grep "proc 2"
1595: proc 2 (channel) line 29, Recv nak,10 <- queue 2 (in)
1596: proc 2 (channel) line 29, Recv ack,11 <- queue 2 (in)
1597: proc 2 (channel) line 29, Recv ack,12 <- queue 2 (in)
1598: proc 2 (channel) line 28 (state 6)
1599: .TE
1600: .fi
1601: .ps +2
1602: .vs +3p
1603: .SP .5
1604: .ce
1605: \fBFigure 1.\fR Simulation Run Output
1606: .SP .5
1607: .KE
1608: .2C
1609: ......
1610: .IH "The Analyzer"
1611: .PP
1612: The simulation runs can be useful in quick debugging of
1613: new designs, but by simulation alone we can not prove
1614: that the system is really error free.
1615: A validation of even very large models can be performed with the
1616: .CW -a
1617: and
1618: .CW -t
1619: options of \*s.
1620: .PP
1621: An exhaustive state space searching program for a protocol
1622: model is generated as follows, producing five files, named \f2pan.[bchmt]\f1.
1623: .P1 0
1624: $ spin -a lynch
1625: .P3
1626: $ wc pan.[bchmt]
1627: .P3
1628: 92 326 2041 pan.b
1629: .P3
1630: 854 2502 17524 pan.c
1631: .P3
1632: 147 576 3475 pan.h
1633: .P3
1634: 307 1230 7493 pan.m
1635: .P3
1636: 177 548 3997 pan.t
1637: .P3
1638: 1577 5182 34530 total
1639: .P2
1640: The details are none too interesting: \f2pan.c\f1 contains
1641: most of the C code for the analysis of the protocol.
1642: File \f2pan.t\f1 contains a transition matrix that encodes
1643: the protocol control flow; \f2pan.b\f1 and \f2pan.m\f1 contain
1644: C code for forward and backward transitions and
1645: \f2pan.h\f1 is a general header file.
1646: The program can be compiled in two different ways: with a full
1647: state space or with a bit state space.
1648: .IH "Exhaustive Search"
1649: .PP
1650: The best method, that works up to system state spaces of
1651: roughly 100,000 states, is to use the
1652: default compilation of the program:
1653: .P1 0
1654: $ cc -o run pan.c
1655: .P2
1656: The executable program \f2run\f1 can now be executed to perform
1657: the validation.
1658: The validation is truly exhaustive: it tests all possible
1659: event sequences in all possible orders.
1660: It should, of course, find the same assertion violation.
1661: .P1 0
1662: $ run
1663: assertion violated (i == last_i + 1))
1664: pan: aborted
1665: pan: wrote pan.trail
1666: search interrupted
1667: vector 64 byte, depth reached 56
1668: 61 states, stored
1669: 5 states, linked
1670: 1 states, matched
1671: hash conflicts: 0 (resolved)
1672: (size 2^18 states, stack frames: 0/5)
1673: .P2
1674: The first line of the output announces the assertion violation
1675: and attempts to give a first indication of the invariant that
1676: was violated.
1677: The violation was found after 61 states had been generated.
1678: Hash "conflicts" gives the number
1679: of hash collisions that happened during access to the state space.
1680: As indicated,
1681: all collisions are resolved in full search mode, since all states are
1682: placed in a linked list.
1683: The most relevant piece of output in this case, however, is on the
1684: third line which tells us that a trail file was created that can
1685: be used in combination with the simulator to recreate the error
1686: sequence.
1687: We can now say, for instance
1688: .P1 0
1689: $ spin -t -r lynch | grep "proc 2"
1690: .P2
1691: to determine the cause of the error.
1692: Note carefully that the validator is guaranteed to find the
1693: assertion violation if it is feasible.
1694: If an exhaustive search does not report such a violation, it is
1695: certain that \f2no\f1 execution execution sequence exists that can
1696: violate the assertion.
1697: .IH Options
1698: .PP
1699: The executable analyzer that is generated comes with a modest
1700: number of options that can be checked as follows
1701: .P1 0
1702: $ run -?
1703: -cN stop at Nth error (default=1)
1704: -l find non-progress loops
1705: -mN max depth N (default=10k)
1706: -wN hash table of 2^N entries (default=18)
1707: .P2
1708: Using a zero as an argument to the first option
1709: forces the state space search to continue,
1710: even if errors are found.
1711: An overview of unexecutable (unreachable) code is given with every
1712: complete run: either the default run if it did not find any
1713: errors, or the run with option
1714: .CW -c0 .
1715: In this case the output is:
1716: .P1 0
1717: $ run -c0
1718: assertion violated (i == (last_i + 1))
1719: assertion violated (i == (last_i + 1))
1720: assertion violated (i == (last_i + 1))
1721: assertion violated (i == (last_i + 1))
1722: assertion violated (i == (last_i + 1))
1723: .P3
1724: vector 64 byte, depth reached 60, errors: 5
1725: 165 states, stored
1726: 5 states, linked
1727: 26 states, matched
1728: hash conflicts: 1 (resolved)
1729: (size 2^18 states, stack frames: 0/6)
1730:
1731: unreached code :init: (proc 0):
1732: reached all 9 states
1733: unreached code channel (proc 1):
1734: line 35 (state 9),
1735: reached: 8 of 9 states
1736: unreached code transfer (proc 2):
1737: line 24 (state 18),
1738: reached: 17 of 18 states
1739: .P2
1740: There were five assertion violations, and some 165 unique
1741: system states were generated.
1742: Each state description (the \f2vector size\f1) took up 64 bytes
1743: of memory; the longest non-cyclic execution sequence was 60.
1744: There is one unreachable state both in the channel process and in
1745: the transfer process.
1746: In both cases the unreachable state is the control flow point
1747: just after the do-loop in each process.
1748: Note that both loops are indeed meant to be non-terminating.
1749: .PP
1750: The \f(CW-l\f1 option will cause the analyzer to search for
1751: non-progress loops rather than deadlocks or assertion violations.
1752: The option is explained in the section on ``More Advanced Usage.''
1753: .PP
1754: The executable analyzer has two other options.
1755: By default the search depth is restricted to a rather
1756: arbitrary 10,000 steps.
1757: If the depth limit is reached, the search is truncated, making
1758: the validation less than exhaustive.
1759: To make certain that the search is exhaustive, make sure that the
1760: "depth reached" notice is within the maximum search depth, and
1761: if not, repeat the analysis with an explicit
1762: .CW -m
1763: argument.
1764: .PP
1765: The
1766: .CW -m
1767: option can of course also be used to truncate
1768: the search explicitly, in an effort to find the shortest possible
1769: execution sequence that violates a given assertion.
1770: Such a truncated search, however, is not guaranteed to find every
1771: possible violation, even within the search depth.
1772: .PP
1773: The last option
1774: .CW -w\fIN
1775: can only affect the run time, not
1776: the scope, of an analysis with a full state space.
1777: This "hash table width" should normally be set equal to,
1778: or preferably higher than,
1779: the logarithm of the expected number of unique system states generated
1780: by the analyzer.
1781: (If it is set too low, the number of hash collisions will increase
1782: and slow down the search.)
1783: The default
1784: .I N
1785: of 18 handles up to 262,144 system states, which should
1786: suffice for almost all applications of a full state space analysis.
1787: .IH "Bit State Space Analysis"
1788: .PP
1789: It can easily be calculated what the memory requirements of an analysis
1790: with a full state space are|reference(holzmann atttj).
1791: If, as in the example we have used, the protocol requires 64 bytes
1792: of memory to encode one system state, and we have a total of 2MB
1793: of memory available for the search, we can store up to 32,768 states.
1794: The analysis fails if there are more reachable states in the
1795: system state space.
1796: So far, \*s is the \f2only\f1 validation system that can avoid this trap.
1797: All other existing automated validation system (irrespective on
1798: which formalism they are based) simply run out of memory and
1799: abort their analysis without returning a useful answer to the user.
1800: .PP
1801: The coverage of a conventional analysis goes down rapidly when
1802: the memory limit is hit, i.e. if there are
1803: twice as many states in the full state space than we can store,
1804: the effective coverage of the search is only 50% and so on.
1805: \*S does substantially better in those cases by using the bit state
1806: space storage method|reference(holzmann atttj).
1807: The bit state space can be included by compiling the analyzer as follows:
1808: .P1 0
1809: $ cc -DBITSTATE -o run pan.c
1810: .P2
1811: The analyzer compiled in this way
1812: should of course find the same assertion violation again:
1813: .P1 0
1814: $ run
1815: assertion violated (i == ((last_i + 1))
1816: pan: aborted
1817: pan: wrote pan.trail
1818: search interrupted
1819: vector 64 byte, depth reached 56
1820: 61 states, stored
1821: 5 states, linked
1822: 1 states, matched
1823: hash factor: 67650.064516
1824: (size 2^22 states, stack frames: 0/5)
1825: $
1826: .P2
1827: In fact, for small to medium size problems there is very little
1828: difference between the full state space method and the bit state
1829: space method (with the exception that the latter is somewhat
1830: faster and uses substantially less memory).
1831: The big difference comes for larger problems.
1832: The last two lines in the output are useful in estimating
1833: the \f2coverage\f1 of a large run.
1834: The maximum number of states that the bit state space can
1835: accommodate is written on the last line (here @2 sup 22@ bytes or about 32 million
1836: bits = states).
1837: The line above it gives the \f2hash factor\f1: roughly
1838: equal to the maximum number of states divided by the actual
1839: number of states.
1840: A large hash factor (larger than 100) means, with high reliability,
1841: a coverage of 99% or 100%.
1842: As the hash factor approaches 1 the coverage approaches 0%.
1843: .PP
1844: Note carefully that the analyzer realizes a partial coverage \f2only\f1
1845: in cases where traditional validators are either unable to perform a
1846: search, or realize a far smaller coverage.
1847: In \f2no\f1 case will \*s produce an answer that is less reliable than
1848: that produced by other automated validation systems (quite on the contrary).
1849: .PP
1850: The object of a bit state validation is to achieve a hash factor
1851: larger than 100 by allocating the maximum amount of memory
1852: for the bit state space.
1853: For the best result obtainable: use the
1854: .CW -w\fIN
1855: option to size the state space to precisely the amount
1856: of real (not virtual) memory available on your machine.
1857: By default,
1858: .I N
1859: is 22, corresponding to a state space of 4MB.
1860: For example, if your machine has 128MB of real memory, you can use
1861: .CW -w27
1862: to analyze systems with up to a billion reachable states.
1863: .SP 2
1864: .NH
1865: \*P Reference Manual
1866: .PP
1867: This section describes the language \*P proper.
1868: As much as possible, the presentation follows the example
1869: from the
1870: .CW C
1871: reference manuals|reference(cbook).
1872: It does not cover possible restrictions or extensions of
1873: specific implementations.
1874: The current implementation of \*s, for instance,
1875: has an extra keyword
1876: .CW printf ,
1877: to access the corresponding
1878: .UX
1879: library function.
1880: .IH "Lexical Conventions"
1881: .PP
1882: There are five classes of tokens: identifiers, keywords, constants,
1883: operators and statement separators.
1884: Blanks, tabs, newlines, and comments serve only to separate tokens.
1885: If more than one interpretation is possible, a token is
1886: taken to be the longest string of characters that can
1887: constitute a token.
1888: .ix lexical conventions
1889: .ix tokens
1890: .IH Comments
1891: .PP
1892: Any string started with
1893: .CW /*
1894: and terminated with
1895: .CW */
1896: is a comment.
1897: Comments may not be nested.
1898: .ix comments
1899: .IH Identifiers
1900: .PP
1901: An identifier is a single letter, period, or underscore
1902: followed by zero or more letters, digits, periods, or underscores.
1903: .ix identifiers
1904: .IH Keywords
1905: .PP
1906: The following identifiers are reserved for use as keywords:
1907: .ix keywords
1908: .KS
1909: .ft CW
1910: .ps -1
1911: .vs -1
1912: .TS
1913: center;
1914: l l l.
1915: assert atomic bit
1916: bool break byte
1917: chan do fi
1918: goto if init
1919: int len mtype
1920: never printf od
1921: of proctype run
1922: short skip timeout
1923: .ps +1
1924: .vs +1
1925: .TE
1926: .KE
1927: .IH Constants
1928: .PP
1929: A constant is a sequence of digits representing a decimal integer.
1930: There are no floating point numbers in \*P.
1931: .ix constants
1932: Symbolic names for constants can be defined in two ways.
1933: The first method is to use a C-style macro definition
1934: .P1 0
1935: #define NAME value
1936: .P2
1937: The second method is to use the keyword
1938: .CW mtype
1939: (see ``declarations'' below).
1940: .IH Expressions
1941: .PP
1942: The following operators can be used to build expressions.
1943: .ix expressions
1944: .ix operators
1945: .KS
1946: .TS
1947: center;
1948: lFCW.
1949: + \- * \/ %
1950: > >= < <= == != !
1951: && ||
1952: & | ~ >> <<
1953: .TE
1954: .KE
1955: .PP
1956: Most operators are binary.
1957: The logical negation \f2!\f1 and the minus \f2\-\f1
1958: operator can be both unary and binary, depending on context.
1959: Expressions are used, for instance, in assignments of the type
1960: .CW "a = expression" ,
1961: with
1962: .CW a
1963: a variable.
1964: .ix assignment
1965: There is also one unary operator that applies to message channels:
1966: .P1 0
1967: len
1968: .P2
1969: It measures the number of messages an existing channel holds.
1970: There is one unary operator that is used for process instantiations:
1971: .P1 0
1972: run
1973: .P2
1974: And, finally, there are two binary operators
1975: .P1 0
1976: ! ?
1977: .P2
1978: which are used for sending and receiving messages (see below).
1979: .IH Declarations
1980: .PP
1981: .ix declarations
1982: Processes, channels, and variables must be declared before they can be used.
1983: Variables and channels can be declared either locally,
1984: within a process, or globally.
1985: A process can only be declared globally in a
1986: .CW proctype
1987: declaration.
1988: Local declarations may appear anywhere in a process body.
1989: .IH Variables
1990: .PP
1991: .ix variables
1992: .ix local variables
1993: .ix global variables
1994: .ix initializers
1995: A variable declaration is started by a keyword indicating the
1996: basic data type of the variable,
1997: .CW bit ,
1998: .CW bool ,
1999: .CW byte ,
2000: .CW short ,
2001: or
2002: .CW int ,
2003: followed
2004: by one or more identifiers, optionally followed by
2005: an initializer.
2006: .P1 0
2007: byte name1, name2 = 4, name3
2008: .P2
2009: By default all variables are initialized to zero.
2010: An initializer, if specified, must be a constant.
2011: The table below summarizes the width and attributes of each
2012: basic data type.
2013: .KS
2014: .ps -1
2015: .vs -2
2016: .TS
2017: center;
2018: l l l
2019: lFCW n r.
2020: =
2021: Name Size (bits) Usage
2022: _
2023: bit 1 unsigned
2024: bool 1 unsigned
2025: byte 8 unsigned
2026: short 16 signed
2027: int 32 signed
2028: _
2029: .TE
2030: .ps +1
2031: .vs +2
2032: .KE
2033: The names \f2bit\f1 and \f2bool\f1
2034: are synonyms for a single bit of
2035: information.
2036: A \f2byte\f1 is an unsigned quantity that can store a value between
2037: 0 and 255.
2038: \f2Short\f1s and \f2int\f1s are signed quantities that
2039: differ only in the range of values they can hold.
2040: .PP
2041: An array of variables is declared as follows:
2042: .P1 0
2043: int name1[N]
2044: .P2
2045: where
2046: .CW N
2047: is a constant.
2048: An array can have a just a single constant as an initializer.
2049: If specified it is used to initialize all elements of the array.
2050: .PP
2051: Symbolic names for constants, e.g. message types,
2052: can, optionally, be defined in a declaration
2053: of the type
2054: .P1 0
2055: mtype = { namelist }
2056: .P2
2057: where
2058: .CW namelist
2059: is a comma separated list of symbolic names.
2060: .IH "Message Channels"
2061: .PP
2062: A message channel can be declared, for instance, as follows:
2063: .ix channels
2064: .P1 0
2065: chan name[N] of { short, short }
2066: .P2
2067: where
2068: .CW N
2069: is a constant that specifies the maximum number of messages
2070: that can be stored in the channel.
2071: A list of one or more data types (or the channel type
2072: .CW chan )
2073: enclosed in curly braces defines the type of the messages that can
2074: be passed through the channel.
2075: All channels are initialized to be empty.
2076: .IH Processes
2077: .PP
2078: .ix process
2079: A process declaration starts with the keyword
2080: .CW proctype
2081: followed by a name, a list of formal parameters
2082: enclosed in round braces, and
2083: a sequence of statements and local
2084: variable declarations.
2085: The body of process declaration is enclosed in curly braces.
2086: .P1 0
2087: proctype name( /* parameter decls */ )
2088: {
2089: /* statements */
2090: }
2091: .P2
2092: .IH Statements
2093: .PP
2094: .ix statements
2095: .ix gotos
2096: .ix labels
2097: .ix skip
2098: There are twelve types of statements:
2099: .KS
2100: .TS
2101: center;
2102: a a a.
2103: .ft CW
2104: .ps -1
2105: .vs -1
2106: assertion assignment atomic
2107: break declaration expression
2108: goto receive selection
2109: repetition send timeout
2110: .ft
2111: .ps +1
2112: .vs +1
2113: .TE
2114: .KE
2115: Each statement may be preceded by a label: a name followed by a colon.
2116: A statement can only be passed if it is executable.
2117: To determine its executability the statement can be evaluated:
2118: if evaluation returns a zero value the statement is blocked.
2119: In all other cases the statement is executable and can be passed.
2120: The act of passing the statement after a successful evaluation is
2121: called the ``execution'' of the statement.
2122: There is one so-called \fIpseudo\fR-statements
2123: .CW skip ,
2124: a null statement equivalent to \(CW(1)\f1; it is always executable.
2125: It has no effect when executed, but may be needed
2126: to satisfy syntax requirements.
2127: The evaluation of an assertion statement
2128: .CW assert(condition)
2129: has no effect if the condition holds, but aborts the
2130: running process if evaluation of the condition returns a
2131: zero result (the boolean value ``false'').
2132: .PP
2133: .CW goto
2134: statements can be used to transfer control to any labeled statement
2135: within the same process or procedure.
2136: They also are always executable.
2137: Assignments have been discussed above, they are
2138: always executable.
2139: A declaration is also always executable.
2140: Expressions are only executable if they return a non-zero value.
2141: That is, the expression \(CW0\fR (zero) is never executable, and
2142: similarly \(CW1\fR always is executable.
2143: Below we consider the remaining statements: selection, repetition,
2144: send, receive, break, timeout, and atomic statements.
2145: .IH Selection
2146: .PP
2147: .ix if statement
2148: .ix case selection
2149: .ix nondeterminism
2150: A selection statement is started with the keyword
2151: .CW if ,
2152: followed by
2153: a list of one or more `options' and terminated with the keyword
2154: .CW fi .
2155: Every `option' is started with the flag \f(CW::\fR followed by any sequence
2156: of statements.
2157: One and only one option from a selection statement will
2158: be selected for execution.
2159: The first statement of an option determines
2160: whether the option can be selected or not.
2161: If more than one option is executable, one will be selected at random.
2162: Note that this randomness makes the language a nondeterministic one.
2163: .IH "Repetition and Break"
2164: .PP
2165: .ix do statement
2166: .ix repetition
2167: A repetition or
2168: .CW do
2169: statement is similar to a selection statement, but is executed
2170: repeatedly until either a
2171: .CW break
2172: statement is executed or a
2173: .CW goto
2174: jump will transfer control outside the cycle.
2175: The keywords of the repetition statement are
2176: .CW do
2177: and
2178: .CW od
2179: instead of the
2180: .CW if
2181: and
2182: .CW fi
2183: of selection.
2184: The
2185: .CW break
2186: statement will terminate the innermost repetition
2187: statement in which it is executed.
2188: The use of a \(CWbreak\fR statement outside a
2189: repetition statement is illegal.
2190: ......
2191: .IH "Atomic Sequences"
2192: .PP
2193: The keyword
2194: .CW atomic
2195: introduces an atomic sequence of statements, that is
2196: to be executed as one indivisible step.
2197: The syntax is as follows
2198: .P1 0
2199: atomic { sequence }
2200: .P2
2201: Logically the sequence of statements is now equivalent
2202: to one single statement.
2203: It is a run-time error if any statement that is part of an
2204: atomic sequence is found to be unexecutable.
2205: The safest is therefore to include only assignments and
2206: local conditions in atomic sequences, but no sends or receives.
2207: Labeling local computations as atomic can bring an important
2208: reduction of the complexity of a validation model.
2209: For the lazy, \*s has an option (\f(CW-q\f1) that tries to find
2210: the most obvious ``atomicable'' sequences in the code,
2211: but the user can often do better by hand.
2212: .IH Send
2213: .PP
2214: .ix i/o statements
2215: .ix send
2216: The syntax of a send statement is:
2217: .P1 0
2218: expr1!expr2
2219: .P2
2220: where
2221: .CW expr1
2222: returns the identity of a channel, e.g. obtained from a
2223: .CW chan
2224: operation, and
2225: .CW expr2
2226: returns a value to be appended to the channel.
2227: The send statement is not executable (blocks) if the addressed channel is full
2228: or does not exist.
2229: .ix value transfer
2230: If more than one value is to be passed from sender to receiver, the expressions
2231: are written in a comma separated list:
2232: .P1 0
2233: expr1!expr2,expr3,expr4
2234: .P2
2235: Equivalently, this may be written
2236: .P1 0
2237: expr1!expr2(expr3,expr4) .
2238: .P2
2239: .IH Receive
2240: .PP
2241: .ix i/o statements
2242: .ix receive
2243: .ix value transfer
2244: The syntax of the receive statement is:
2245: .P1 0
2246: expr1?name
2247: .P2
2248: where
2249: .CW expr1
2250: returns the name of a channel and
2251: .CW name
2252: is a variable or a constant.
2253: If a constant is specified the receive statement is only executable
2254: if the channel exists and
2255: the oldest message stored in the channel contains the same value.
2256: If a variable is specified, the receive statement is executable
2257: if the channel exists and contains any message at all.
2258: The variable in that case will receive the value of the message
2259: that is retrieved.
2260: If more than one value is sent per message, the receive statement
2261: also take a comma separated list of variables and constants
2262: .P1 0
2263: expr1?name1,name2,...
2264: .P2
2265: which again is syntactically equivalent to
2266: .P1 0
2267: expr1?name1(name2,...)
2268: .P2
2269: Each constant in this list puts an extra condition on the
2270: executability of the receive: it must be matched by the
2271: value of the corresponding message field of the
2272: message to be retrieved.
2273: The variable fields retrieve the values of the corresponding
2274: message fields on a receive.
2275: .PP
2276: Placing square brackets around the clause after the `?'
2277: in the receiver operation converts it into a condition,
2278: that is true only if the corresponding receive operation
2279: is executable.
2280: It can be used freely in any type of composite boolean condition,
2281: and it has no side-effects when evaluated.
2282: .PP
2283: A last type of operation allowed on channels is
2284: .P1 0
2285: len(expr)
2286: .P2
2287: where
2288: .CW expr
2289: returns the identity of an instantiated channel.
2290: The operation returns the number of messages in
2291: the channel specified, or zero if the channel does not exist.
2292: .IH Timeout
2293: .PP
2294: The timeout condition is a modeling feature that by definition becomes true
2295: only if no statement in any of the running processes is executable.
2296: It has no effect when executed.
2297: .IH "Macros and Include Files"
2298: .PP
2299: .ix macros
2300: .ix include files
2301: .ix preprocessor
2302: The source text of a specification is processed by the C|reference(cbook)
2303: preprocessor for macro-expansion and file inclusions.
2304: .NH
2305: Summary
2306: .PP
2307: In the first part of this memo
2308: we have introduced a notation for modeling concurrent
2309: systems, including but not limited to asynchronous
2310: data communication protocols, in a language named \*P.
2311: The language has several unusual features.
2312: All communication between processes takes
2313: place via either messages or shared variables.
2314: Both synchronous and asynchronous communication
2315: are modeled as two special cases of a general message
2316: passing mechanism.
2317: Every statement in \*P can potentially model delay: it is
2318: either executable or not, in most cases depending on the state
2319: of the environment of the running process.
2320: Process interaction and process coordination is thus at
2321: the very basis of the language.
2322: More about the design of \*P, of the validator \*s, and
2323: its application to protocol design, can be found in |reference(holzmann spinbook).
2324: .PP
2325: \*P is deliberately a validation modeling language, not a programming language.
2326: There are, for instance, no elaborate abstract data types,
2327: or more than a few basic types of variable.
2328: A validation model is an abstraction of a protocol implementation.
2329: The abstraction maintains the essentials of the process interactions,
2330: so that it can be studied in isolation.
2331: It suppresses implementation and programming detail.
2332: .PP
2333: The syntax of \*P expressions, declarations, and assignments
2334: is loosely based on the language
2335: .CW C |reference(cbook).
2336: The language was influenced significantly by the ``guarded command languages''
2337: of E.W. Dijkstra |reference(dijkstra guarded) and C.A.R. Hoare
2338: |reference(hoare csp).
2339: There are, however, important differences.
2340: Dijkstra's language had no primitives for process interaction.
2341: Hoare's language was based exclusively on synchronous
2342: communication.
2343: Also in Hoare's language, the type
2344: of statements that could appear in the guards of an option was
2345: restricted.
2346: The semantics of the selection and cycling statements
2347: in \*P is also rather different from other guarded
2348: command languages: the statements are not aborted when all guards
2349: are false but they block: thus providing the required synchronization.
2350: .PP
2351: With minimal effort \*s allows the user to generate sophisticated
2352: analyzers from \*P validation models.
2353: Both the \*s software itself, and the analyzers it can generate,
2354: are written in ANSII C and are portable across
2355: .UX
2356: systems.
2357: They can be scaled to fully exploit the physical limitations
2358: of the host computer, and deliver within those
2359: limits the best possible analyses that can be realized
2360: with the current state of the art in protocol analysis.
2361: .NH
2362: References
2363: .LP
2364: |reference_placement
2365: .af H1 A
2366: .nr H1 1
2367: .nr H2 0
2368: .SH
2369: Appendix: Building A Validation Suite
2370: .PP
2371: The first order of business in using \*s for
2372: a validation is the construction of a
2373: faithful model in \*P of the problem at hand.
2374: The language is deliberately kept small.
2375: The purpose of the modeling is to extract those
2376: aspects of the system that are relevant to the
2377: coordination problem being studied.
2378: All other details are suppressed.
2379: Formally: the model is a reduction of the
2380: system that needs to be equivalent to the full system
2381: only with respect to the properties that are being validated.
2382: Once a model has been constructed, it becomes
2383: the basis for the construction of a series of,
2384: what we may call, ``validation suites'' that
2385: are used to verify its properties.
2386: To build a validation suite we can prime the
2387: model with assertions.
2388: The assertions can formalize invariant relations
2389: about the values of variables or about allowable
2390: sequences of events in the model.
2391: .NH 2
2392: An Example
2393: .PP
2394: As a first example we take the following solution
2395: to the mutual exclusion problem, discussed earlier,
2396: published in 1966 by H. Hyman in the Communications of the ACM.
2397: It was listed, in pseudo Algol, as follows.
2398: .P1 0
2399: 1 \f3Boolean array\f2 b(0;1) \f3integer\f2 k, i,\f(CW
2400: 2 \f3comment\f2 process i, with i either 0 or 1;\f(CW
2401: 3 \f2C0: b(i) := \f3false\f2;\f(CW
2402: 4 \f2C1: \f3if\f2 k != i \f3then begin\f2\f(CW
2403: 5 \f2C2: \f3if\f2 not (b(1-i) \f3then go to\f2 C2;\f(CW
2404: 6 \f3else\f2 k := i; \f3go to\f2 C1 \f3end\f2;\f(CW
2405: 7 \f3else\f2 critical section;\f(CW
2406: 8 \f2b(i) := \f3true\f2;\f(CW
2407: 9 \f2remainder of program;\f(CW
2408: 10 \f3go to\f2 C0;\f(CW
2409: 11 \f3end\f(CW
2410: .P2
2411: The solution, as Dekker's earlier solution, is for two processes,
2412: numbered 0 and 1.
2413: Suppose we wanted to prove that Hyman's solution truly
2414: guaranteed mutually exclusive access to the critical section.
2415: Our first task is to build a model of the solution in \*P.
2416: While we're at it, we can pick some more useful names for
2417: the variables that are used.
2418: .P1 0
2419: 1 bool want[2]; /* Bool array b */
2420: 2 bool turn; /* integer k */
2421: 3
2422: .P3
2423: 4 proctype P(bool i)
2424: 5 {
2425: 6 want[i] = 1;
2426: .P3
2427: 7 do
2428: 8 :: (turn != i) ->
2429: 9 (!want[1-i]);
2430: 10 turn = i
2431: .P3
2432: 11 :: (turn == i) ->
2433: 12 break
2434: 13 od;
2435: .P3
2436: 14 skip; /* critical section */
2437: 15 want[i] = 0
2438: 16 }
2439: .P3
2440: 17
2441: .P3
2442: 18 init { run P(0); run P(1) }
2443: .P2
2444: We can generate, compile, and run a validator for this
2445: model, to see if there are any major problems, such as
2446: a global system deadlock.
2447: .P1 0
2448: $ spin -a hyman0
2449: $ cc pan.c
2450: $ a.out
2451: full statespace search for:
2452: assertion violations and invalid endstates
2453: vector 20 byte, depth reached 19, errors: 0
2454: 79 states, stored
2455: 0 states, linked
2456: 38 states, matched total: 117
2457: hash conflicts: 4 (resolved)
2458: (size 2^18 states, stack frames: 3/0)
2459:
2460: unreached code _init (proc 0):
2461: reached all 3 states
2462: unreached code P (proc 1):
2463: reached all 12 states
2464: .P2
2465: The model passes this first test.
2466: What we are really interested in, however, is if
2467: the algorithm guarantees mutual exclusion.
2468: There are several ways to proceed.
2469: The simplest is to just add enough information
2470: to the model that we can express the correctness
2471: requirement in a \*P assertion.
2472: .P1 0
2473: 1 bool want[2];
2474: 2 bool turn;
2475: 3 byte cnt;
2476: 4
2477: .P3
2478: 5 proctype P(bool i)
2479: 6 {
2480: .P3
2481: 7 want[i] = 1;
2482: .P3
2483: 8 do
2484: 9 :: (turn != i) ->
2485: 10 (!want[1-i]);
2486: 11 turn = i
2487: .P3
2488: 12 :: (turn == i) ->
2489: 13 break
2490: 14 od;
2491: 15 skip; /* critical section */
2492: .P3
2493: 16 cnt = cnt+1;
2494: 17 assert(cnt == 1);
2495: 18 cnt = cnt-1;
2496: 19 want[i] = 0
2497: 20 }
2498: .P3
2499: 21
2500: .P3
2501: 22 init { run P(0); run P(1) }
2502: .P2
2503: We have added a global variable
2504: .CW cnt
2505: that is incremented upon each access to the
2506: critical section, and decremented upon each exit
2507: from it.
2508: The maximum value that this variable should ever
2509: have is 1, and it can only have this value when
2510: a process is inside the critical section.
2511: .P1 0
2512: $ spin -a hyman1
2513: $ cc pan.c
2514: $ a.out
2515: assertion violated (cnt==1)
2516: pan: aborted (at depth 15)
2517: pan: wrote pan.trail
2518: full statespace search for:
2519: assertion violations and invalid endstates
2520: search was not completed
2521: vector 20 byte, depth reached 25, errors: 1
2522: 123 states, stored
2523: 0 states, linked
2524: 55 states, matched total: 178
2525: hash conflicts: 42 (resolved)
2526: (size 2^18 states, stack frames: 3/0)
2527: .P2
2528: The validator claims that the assertion can be violated.
2529: We can use the error trail to check it with \*s's \f(CW-t\f1 option:
2530: .P1 0
2531: $ spin -t -p hyman1
2532: proc 0 (_init) line 24 (state 2)
2533: proc 0 (_init) line 24 (state 3)
2534: .P3
2535: proc 2 (P) line 8 (state 7)
2536: proc 2 (P) line 9 (state 2)
2537: .P3
2538: proc 2 (P) line 10 (state 3)
2539: proc 2 (P) line 11 (state 4)
2540: .P3
2541: proc 1 (P) line 8 (state 7)
2542: proc 1 (P) line 12 (state 5)
2543: .P3
2544: proc 1 (P) line 15 (state 10)
2545: proc 2 (P) line 8 (state 7)
2546: .P3
2547: proc 2 (P) line 12 (state 5)
2548: proc 2 (P) line 15 (state 10)
2549: .P3
2550: proc 2 (P) line 16 (state 11)
2551: proc 2 (P) line 17 (state 12)
2552: .P3
2553: proc 2 (P) line 18 (state 13)
2554: proc 1 (P) line 16 (state 11)
2555: .P3
2556: proc 1 (P) line 17 (state 12)
2557: spin: "hyman1" line 17: assertion violated
2558: .P3
2559: step 17, #processes: 3
2560: want[0] = 1
2561: _p[0] = 12
2562: turn[0] = 1
2563: cnt[0] = 2
2564: .P3
2565: proc 2 (P) line 18 (state 13)
2566: proc 1 (P) line 17 (state 12)
2567: proc 0 (_init) line 24 (state 3)
2568: 3 processes created
2569: .P2
2570: Here is another way to catch the error.
2571: We again lace the model with the information that
2572: will allow us to count the number of processes
2573: in the critical section.
2574: .P1 0
2575: 1 bool want[2];
2576: 2 bool turn;
2577: 3 byte cnt;
2578: 4
2579: .P3
2580: 5 proctype P(bool i)
2581: 6 {
2582: 7 want[i] = 1;
2583: .P3
2584: 8 do
2585: 9 :: (turn != i) ->
2586: 10 (!want[1-i]);
2587: 11 turn = i
2588: .P3
2589: 12 :: (turn == i) ->
2590: 13 break
2591: 14 od;
2592: .P3
2593: 15 cnt = cnt+1;
2594: 16 skip; /* critical section */
2595: 17 cnt = cnt-1;
2596: 18 want[i] = 0
2597: 19 }
2598: .P3
2599: 20
2600: .P3
2601: 21 proctype monitor()
2602: 22 {
2603: 23 assert(cnt == 0 || cnt == 1)
2604: 24 }
2605: .P3
2606: 25
2607: .P3
2608: 26 init {
2609: 27 run P(0); run P(1); run monitor()
2610: 28 }
2611: .P2
2612: The invariant condition on the value of counter
2613: .CW cnt
2614: is now place in a separate process
2615: .CW monitor()
2616: (the name is immaterial).
2617: The extra process runs along with the two others.
2618: It will always terminate in one step, but it
2619: could execute that step at \f2any\f1 time.
2620: The systems modeled by \*P and validated by \*s
2621: are completely asynchronous.
2622: That means that the validation of \*s take into
2623: account \f2all\f1 possible relative timings of
2624: the three processes.
2625: In a full validation, the assertion therefore
2626: can be evaluated at any time during the lifetime
2627: of the other two processes.
2628: If the validator reports that it is not violated
2629: we can indeed conclude that there is no execution
2630: sequence at all (no way to select relative speeds for
2631: the three processes) in which the assertion can be
2632: violated.
2633: The setup with the monitor process is therefore an
2634: elegant way to check the validity of a system invariant.
2635: The validation produces:
2636: .P1 0
2637: $ spin -a hyman2
2638: $ cc pan.c
2639: $ a.out
2640: assertion violated ((cnt==0)||(cnt==1))
2641: pan: aborted (at depth 15)
2642: pan: wrote pan.trail
2643: full statespace search for:
2644: assertion violations and invalid endstates
2645: search was not completed
2646: vector 24 byte, depth reached 26, errors: 1
2647: 368 states, stored
2648: 0 states, linked
2649: 379 states, matched total: 747
2650: hash conflicts: 180 (resolved)
2651: (size 2^18 states, stack frames: 4/0)
2652: .P2
2653: Because of the extra interleaving of the two processes
2654: with a third monitor, the number of system states that
2655: had to be searched has increased, but the error is again
2656: correctly reported.
2657: .br
2658: .NE 8v
2659: .NH 2
2660: Another Example
2661: .PP
2662: Not always can a correctness requirement be cast in
2663: terms of a global system invariant.
2664: Here is an example that illustrates this.
2665: It is a simple alternating bit protocol, modeling
2666: the possibility of message loss, and distortion,
2667: and extended with negative acknowledgements.
2668: .P1 0
2669: 1 #define MAX 5
2670: 2
2671: 3 mtype = { mesg, ack, nak, err };
2672: 4
2673: .P3
2674: 5 proctype sender(chan in, out)
2675: 6 { byte o, s, r;
2676: 7
2677: 8 o=MAX-1;
2678: 9 do
2679: 10 :: o = (o+1)%MAX; /* next msg */
2680: 11 again: if
2681: 12 :: out!mesg(o,s) /* send */
2682: 13 :: out!err(0,0) /* distort */
2683: 14 :: skip /* or lose */
2684: 15 fi;
2685: .P3
2686: 16 if
2687: 17 :: timeout -> goto again
2688: 18 :: in?err(0,0) -> goto again
2689: 19 :: in?nak(r,0) -> goto again
2690: 20 :: in?ack(r,0) ->
2691: 21 if
2692: 22 :: (r == s) -> goto progress
2693: 23 :: (r != s) -> goto again
2694: 24 fi
2695: 25 fi;
2696: 26 progress: s = 1-s /* toggle seqno */
2697: 27 od
2698: 28 }
2699: 29
2700: .P3
2701: 30 proctype receiver(chan in, out)
2702: 31 { byte i; /* actual input */
2703: 32 byte s; /* actual seqno */
2704: 33 byte es; /* expected seqno */
2705: 34 byte ei; /* expected input */
2706: 35
2707: 36 do
2708: 37 :: in?mesg(i, s) ->
2709: 38 if
2710: 39 :: (s == es) ->
2711: 40 assert(i == ei);
2712: 41 progress: es = 1 - es;
2713: 42 ei = (ei + 1)%MAX;
2714: 43 if
2715: 44 /* send, */ :: out!ack(s,0)
2716: 45 /* distort */ :: out!err(0,0)
2717: 46 /* or lose */ :: skip
2718: 47 fi
2719: .P3
2720: 48 :: (s != es) ->
2721: .P3
2722: 49 if
2723: .P3
2724: 50 /* send, */ :: out!nak(s,0)
2725: 51 /* distort */ :: out!err
2726: 52 /* or lose */ :: skip
2727: .P3
2728: 53 fi
2729: .P3
2730: 54 fi
2731: 55 :: in?err(0,0) ->
2732: 56 out!nak(s,0)
2733: .P3
2734: 57 od
2735: 58 }
2736: 59
2737: .P3
2738: 60 init {
2739: .P3
2740: 61 chan s_r [1] of { byte,byte,byte };
2741: 62 chan r_s [1] of { byte,byte,byte };
2742: .P3
2743: 63 atomic {
2744: .P3
2745: 64 run sender(r_s, s_r);
2746: 65 run receiver(s_r, r_s)
2747: .P3
2748: 66 }
2749: .P3
2750: 67 }
2751: .P2
2752: To test the proposition that this protocol will
2753: correctly transfer data, the model has already
2754: been primed for the first validation runs.
2755: First, the sender is setup to transfer an infinite
2756: series of integers as messages, where the value
2757: of the integers are incremented modulo
2758: .CW MAX .
2759: The value of
2760: .CW MAX
2761: is not really too interesting, as long as it is
2762: larger than the range of the sequence numbers in
2763: the protocol: in this case 2.
2764: We want to verify that data that is sent can only be
2765: delivered to the receiver without any deletions or reorderings,
2766: despite the possibility of arbitrary message loss.
2767: The assertion on line 40 verifies precisely that.
2768: Note that if it were ever possible for the protocol to
2769: fail to meet the above requirement, the assertion can be violated.
2770: .PP
2771: A first validation run reassures us that this is not possible.
2772: .P1 0
2773: $ spin -a ABP0
2774: $ cc pan.c
2775: $ a.out
2776: full statespace search for:
2777: assertion violations and invalid endstates
2778: vector 40 byte, depth reached 131, errors: 0
2779: 346 states, stored
2780: 1 states, linked
2781: 125 states, matched total: 472
2782: hash conflicts: 17 (resolved)
2783: (size 2^18 states, stack frames: 0/25)
2784:
2785: unreached code _init (proc 0):
2786: reached all 4 states
2787: unreached code receiver (proc 1):
2788: line 58 (state 24)
2789: reached: 23 of 24 states
2790: unreached code sender (proc 2):
2791: line 28 (state 27)
2792: reached: 26 of 27 states
2793: .P2
2794: But, be careful.
2795: The result means that all data that is delivered, is
2796: delivered in the correct order without deletions etc.
2797: We did not check that the data \f2will\f1 necessarily be delivered.
2798: It may be possible for sender and receiver to cycle
2799: through a series of states, exchanges erroneous messages,
2800: without ever making effective progress.
2801: To check this, the state in the sender and in the receiver
2802: process that unmistakingly signify progress, were labeled
2803: as a ``progress states.''
2804: (In fact, either one by itself would suffice.)
2805: .PP
2806: We should now be able to demonstrate the absence of
2807: infinite execution cycles that do not pass through any
2808: of these progress states.
2809: We can use the same executable from the last run, but
2810: this time we perform a loop-check.
2811: .P1 0
2812: $ a.out -l
2813: pan: non-progress cycle (at depth 6)
2814: pan: wrote pan.trail
2815: full statespace search for:
2816: assertion violations and non-progress loops
2817: search was not completed
2818: vector 44 byte, depth reached 8, loops: 1
2819: 12 states, stored
2820: 1 states, linked
2821: 0 states, matched total: 13
2822: hash conflicts: 0 (resolved)
2823: (size 2^18 states, stack frames: 0/1)
2824: .P2
2825: There are non-progress cycles.
2826: The first one encountered is dumped into the error trail
2827: by the validator, and we can inspect it.
2828: The results are shown in the first half of Figure 2.
2829: The channel can distort or lose the message infinitely often;
2830: true, but not too exciting as an error scenario.
2831: To see how many non-progress cycles there are, we can use the \f(CW-c\f1 flag.
2832: If we set its numeric argument to zero, only
2833: a total count of all errors will be printed.
2834: .P1 0
2835: $ a.out -l -c0
2836: full statespace search for:
2837: assertion violations and non-progress loops
2838: vector 44 byte, depth reached 137, loops: 92
2839: 671 states, stored
2840: 2 states, linked
2841: 521 states, matched total: 1194
2842: hash conflicts: 39 (resolved)
2843: (size 2^18 states, stack frames: 0/26)
2844: .P2
2845: There are 92 cases to consider, and we could look at each
2846: one, using the \f(CW-c\f1 option (\f(CW-c1\f1, \f(CW-c2\f1, \f(CW-c3\f1, ...etc.)
2847: But, we can make the job a little easier by at least
2848: filtering out the errors caused by infinite message loss.
2849: We label all loss events (lines 13, 43, and 48) as
2850: progress states, using label names with the common 8-character
2851: prefix ``progress,'' and look at the cycles that remain.
2852: (Labels go behind the ``::'' flags.)
2853: .P1 0
2854: $ spin -a ABP1
2855: $ cc pan.c
2856: .P3
2857: $ a.out -l
2858: pan: non-progress cycle (at depth 133)
2859: pan: wrote pan.trail
2860: .P3
2861: full statespace search for:
2862: assertion violations and non-progress loops
2863: search was not completed
2864: .P3
2865: vector 44 byte, depth reached 136, loops: 1
2866: .P3
2867: 148 states, stored
2868: 2 states, linked
2869: 2 states, matched total: 152
2870: .P3
2871: hash conflicts: 0 (resolved)
2872: (size 2^18 states, stack frames: 0/26)
2873: .P2
2874: This time, the trace reveals an honest and a serious bug in the protocol.
2875: The second half of Figure 2 shows the trace-back.
2876: .1C
2877: .KF
2878: .nf
2879: .ps -2
2880: .vs -3p
2881: .ft CW
2882: .TS
2883: box expand;
2884: l
2885: l.
2886: $ spin -t -r -s ABP0
2887: <<<<<START OF CYCLE>>>>>
2888: proc 1 (sender) line 13, Send err,0,0 -> queue 2 (out)
2889: proc 2 (receiver) line 55, Recv err,0,0 <- queue 2 (in)
2890: proc 2 (receiver) line 56, Send nak,0,0 -> queue 1 (out)
2891: proc 1 (sender) line 19, Recv nak,0,0 <- queue 1 (in)
2892: spin: trail ends after 12 steps
2893: step 12, #processes: 3
2894: _p[0] = 6
2895: proc 2 (receiver) line 36 (state 21)
2896: proc 1 (sender) line 11 (state 6)
2897: proc 0 (_init) line 67 (state 4)
2898: 3 processes created
2899: $
2900: $ spin -t -r -s ABP1
2901: \&...
2902: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2903: proc 2 (receiver) line 47, Send err,0,0 -> queue 1 (out)
2904: proc 1 (sender) line 20, Recv err,1,0 <- queue 1 (in)
2905: proc 1 (sender) line 12, Send mesg,0,0 -> queue 2 (out)
2906: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2907: proc 2 (receiver) line 52, Send nak,0,0 -> queue 1 (out)
2908: proc 1 (sender) line 21, Recv nak,0,0 <- queue 1 (in)
2909: proc 1 (sender) line 12, Send mesg,0,0 -> queue 2 (out)
2910: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2911: proc 2 (receiver) line 52, Send nak,0,0 -> queue 1 (out)
2912: <<<<<START OF CYCLE>>>>>
2913: proc 1 (sender) line 21, Recv nak,0,0 <- queue 1 (in)
2914: proc 1 (sender) line 12, Send mesg,0,0 -> queue 2 (out)
2915: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2916: proc 2 (receiver) line 52, Send nak,0,0 -> queue 1 (out)
2917: spin: trail ends after 226 steps
2918: \&...
2919: .TE
2920: .fi
2921: .ps +2
2922: .vs +3p
2923: .SP .5
2924: .ce
2925: \fBFigure 2.\fR Error Trails - Extended Alternating Bit Protocol
2926: .SP .5
2927: .KE
2928: .2C
2929: .PP
2930: After a single positive acknowledgement is distorted
2931: and transformed into an
2932: .CW err
2933: message, sender and receiver get caught in an infinite
2934: cycle, where the sender will stubbornly repeat the last
2935: message for which it did not receive an acknowledgement,
2936: and the receiver, just as stubbornly, will reject that
2937: message with a negative acknowledgment.
2938: .NH 2
2939: Digging Deeper
2940: .PP
2941: This manual can only give an outline of the
2942: main features of \*s, and the more common
2943: ways in which it can be used for validations.
2944: There is a small number of \*s features that
2945: have not been discussed here, but that may be useful
2946: for tackling non-standard validation problems.
2947: \*S, for instance, can give \*P processes access
2948: to extra system information, such as the current
2949: values of normally invisible local variables,
2950: or the current execution states of remote processes.
2951: With this extra information it may be easier in
2952: some cases to build accurate assertions about
2953: required system behavior.
2954: .PP
2955: \*S also allows for a straightforward validation of ``tasks.''
2956: That is, if the user formalizes a task that is claimed to be
2957: performed by the system, \*s can quickly either prove or
2958: disprove that claim.
2959: The tasks can be used directly to verify any
2960: propositional temporal logic formula
2961: on the behavior of a system.
2962: .PP
2963: \*S also allows the user to formalize ``reductions'' of
2964: the system state space, which can be used
2965: to restrict a search it to a user defined subset.
2966: With this method it becomes trivial to verify quickly
2967: whether or not a given error pattern is within the range of
2968: behaviors of a system, even when a complete validation is
2969: considered to be infeasible.
2970: .PP
2971: For details about these alternative uses of \*P and
2972: the \*s software, refer to [5].
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.