![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to spin.ms_o 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_o 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 a few
1124: special types of statements, such as
1125: \f(CWassert\f1, \f(CWblock\f1,
1126: and \f(CWhang\f1, that we discuss next.
1127: .NH 3
1128: End-State Labels
1129: .PP
1130: When \*P is used as a validation language the user must
1131: be able to make very specific assertions about the behavior
1132: that is being modeled.
1133: In particular, if a \*P is checked for the presence of
1134: deadlocks, the validator must be able to distinguish a normal \f2end state\f1
1135: from an abnormal one.
1136: .PP
1137: A normal end state could be a state in which every \*P process
1138: that was instantiated has properly reached the end of the
1139: defining program body, and all message channels are empty.
1140: But, not all \*P process are, of course, meant to reach the
1141: end of their program body.
1142: Some may very well linger in an \f(CWIDLE\f1
1143: state, or they may sit patiently in a loop
1144: ready to spring into action when new input arrives.
1145: .PP
1146: To make it clear to the validator that these alternate end states
1147: are legal, and do not constitute a deadlock, a \*P model can use
1148: end state labels.
1149: For instance, if by adding a label to the process type
1150: \f(CWdijkstra()\f1, from section 1.9:
1151: .P1
1152: proctype dijkstra()
1153: { byte count = 1;
1154:
1155: end: do
1156: :: (count == 1) \->
1157: sema!p; count = 0
1158: :: (count == 0) \->
1159: sema?v; count = 1
1160: od
1161: }
1162: .P2
1163: we indicate that it is not an error if, at the end of an
1164: execution sequence, a process of type \f(CWdijkstra()\f1
1165: has not reached its closing curly brace, but waits in the loop.
1166: Of course, such a state could still be part of a deadlock state, but
1167: if so, it is not caused by this particular process.
1168: (It will still be reported if any one of the other processes
1169: in not in a valid end-state).
1170: .PP
1171: There may be more than one end state label per validation model.
1172: If so, all labels that occur within the same process body must
1173: be unique.
1174: The rule is that every label name that \f2starts\f1 with the three
1175: character sequence \f(CW"end"\f1
1176: is an endstate label.
1177: So it is perfectly valid to use variations such as
1178: \f(CWenddne\f1, \f(CWend0\f1, \f(CWend_appel\f1, etc.
1179: .NH 3
1180: Progress-State Labels
1181: .PP
1182: In the same spirit as the end state labels, the user can also
1183: define \f2progress state\f1 labels.
1184: In this case, a progress state labels will mark a state that
1185: \f2must\f1 be executed for the protocol to make progress.
1186: Any infinite cycle in the protocol execution that does not
1187: pass through at least one of these progress states, is a
1188: potential starvation loop.
1189: In the
1190: .CW dijkstra
1191: example, for instance, we can label the
1192: successful passing of a semaphore test as ``progress'' and
1193: ask a validator to make sure that there is no cycle in the
1194: protocol execution where at least one process succeeds in
1195: passing the semaphore guard.
1196: If more than one state carries a progress label,
1197: variations with a common prefix are again valid:
1198: \f(CWprogress0\f1, \f(CWprogress_foo\f1, etc.
1199: .KF
1200: .P1
1201: proctype dijkstra()
1202: { byte count = 1;
1203:
1204: end: do
1205: :: (count == 1) ->
1206: progress: sema!p; count = 0
1207: :: (count == 0) ->
1208: sema?v; count = 1
1209: od
1210: }
1211: .P2
1212: .KE
1213: .PP
1214: .CW "spin -a"
1215: generates analyzers that support (after compilation) a
1216: .CW -l
1217: option, which makes the analyzer use a fast search for non-progress loops,
1218: instead of the default search for deadlocks.
1219: The
1220: .CW -l
1221: search completely avoids the expense of a
1222: full construction of all strongly
1223: connected components in the reachability graph
1224: (the conventional method for doing loop analysis).
1225: The expense is therefore never more than about
1226: twice the time and memory requirements of
1227: a default search for deadlocks.
1228: .IH "Message Type Definitions"
1229: .PP
1230: We have seen how variables are declared and how constants
1231: can be defined using C-style macros.
1232: As a mild form of syntactic sugar, \*P also allows for
1233: message type definitions that look as follows:
1234: .P1 0
1235: mtype = {
1236: ack, nak, err,
1237: next, accept
1238: }
1239: .P2
1240: This is a preferred way of specifying the message types since
1241: it abstracts from the specific values to be used, and it makes
1242: the names of the constants available to an implementation,
1243: which can improve error reporting.
1244: .IH "Pseudo Statements"
1245: .PP
1246: We have now discussed all the basic types of statements defined in \*P:
1247: assignments, conditions, send and receive,
1248: .CW assert ,
1249: .CW timeout ,
1250: .CW goto ,
1251: .CW break
1252: and
1253: .CW skip .
1254: Note that
1255: .CW chan ,
1256: .CW len
1257: and
1258: .CW run
1259: are not really statements but unary operators that can be used in
1260: conditions and assignments.
1261: .PP
1262: The
1263: .CW skip
1264: statement was mentioned in passing as a statement that can be
1265: a useful filler to satisfy syntax requirements, but that really
1266: has no effect.
1267: It is formally not part of the language but a \f2pseudo-statement\f1,
1268: merely a synonym of another statement with the same effect: a
1269: simple condition of a constant value
1270: .CW (1) .
1271: In the same spirit two other pseudo-statements are predefined.
1272: They are called
1273: .CW block
1274: and
1275: .CW halt .
1276: The first is a stop statement that is never executable: the
1277: opposite of
1278: .CW skip .
1279: It is modeled as another condition
1280: .CW (0) .
1281: The
1282: .CW halt
1283: statement aborts the execution of the system of processes
1284: whenever it is executed.
1285: It is equivalent to an assertion that will always fail:
1286: .CW assert(0) .
1287: .IH Example
1288: .PP
1289: Here is a simple example of a (flawed) protocol, modeled in \*P.
1290: .P1 0
1291: mtype = {
1292: ack, nak, err, next, accept
1293: }
1294:
1295: .P3
1296: proctype transfer(chan in,out,chin,chout)
1297: { byte o, i;
1298:
1299: in?next(o);
1300: .P3
1301: do
1302: :: chin?nak(i) ->
1303: out!accept(i);
1304: chout!ack(o)
1305: .P3
1306: :: chin?ack(i) ->
1307: out!accept(i);
1308: in?next(o);
1309: chout!ack(o)
1310: .P3
1311: :: chin?err(i) ->
1312: chout!nak(o)
1313: od
1314: }
1315:
1316: .P3
1317: init
1318: { chan AtoB[1] of { byte, byte };
1319: chan BtoA[1] of { byte, byte };
1320: .P3
1321: chan Ain [2] of { byte };
1322: chan Bin [2] of { byte };
1323: .P3
1324: chan Aout[2] of { byte };
1325: chan Bout[2] of { byte };
1326: .P3
1327: atomic {
1328: run transfer(Ain,Aout, AtoB,BtoA);
1329: run transfer(Bin,Bout, BtoA,AtoB)
1330: };
1331: .P3
1332: AtoB!err(0)
1333: }
1334: .P2
1335: The channels
1336: .CW Ain
1337: and
1338: .CW Bin
1339: are to be filled with
1340: token messages of type
1341: .CW next
1342: and arbitrary values (e.g.
1343: ASCII character values) by unspecified background processes:
1344: the users of the transfer service.
1345: Similarly, these user processes
1346: can read received data from the channels
1347: .CW Aout
1348: and
1349: .CW Bout .
1350: The channels and processes are initialized in a single
1351: atomic statement, and started with the dummy
1352: .CW err
1353: message.
1354: .NH
1355: Introduction to Spin
1356: .PP
1357: Given a model system specified in \*P, \*s
1358: can either perform random simulations of the system's execution
1359: or it can generate a C program that performs a fast exhaustive
1360: validation of the system state space.
1361: The validator can check, for instance, if user specified system
1362: invariants may be violated during a protocol's execution.
1363: .PP
1364: If \*s is invoked without any options it performs a random simulation.
1365: With option
1366: .CW -n\fIN
1367: the seed for the simulation is set explicitly to the integer value
1368: .I N .
1369: .PP
1370: The options
1371: .CW pglrs
1372: controls the amount of information output from the simulation run.
1373: Every line of output normally contains a reference to the source
1374: line in the specification that caused it.
1375: .IP \f(CW-p\f1
1376: Shows the state changes of the \*P
1377: processes at every time step.
1378: .IP \f(CW-g\f1
1379: Shows the current value of global variables at every time step.
1380: .IP \f(CW-l\f1
1381: Shows the current value of local variables, after the
1382: process that owns them has changed state.
1383: It is best used in combination with option
1384: .CW -p .
1385: .IP \f(CW-r\f1
1386: Shows all message receive events.
1387: It shows the process performing the receive, its name and number,
1388: the source line number, the message parameter number (there is
1389: one line for each parameter), the message type and the message
1390: channel number and name.
1391: .IP \f(CW-s\f1
1392: Shows all message send events.
1393: .LP
1394: \*S understands four other options:
1395: .IP \f(CW-a\f1
1396: Generates a protocol specific analyzer.
1397: The output is written into a set of C files, named
1398: .CW pan.[cbhmt] ,
1399: that can be compiled to produce the analyzer
1400: (which is then executed to perform the analysis).
1401: To guarantee an exhaustive exploration of the state space, the
1402: program can be compiled simply as
1403: .RS
1404: .IP
1405: .P1
1406: $ cc -o run pan.c
1407: .P2
1408: .RE
1409: .IP
1410: For larger systems this may, however, exhaust the available memory
1411: on the machine used.
1412: Large to very large systems can still be analyzed by using a
1413: memory efficient bit state space method by
1414: .RS
1415: .IP
1416: .P1
1417: $ cc -DBITSTATE -o run pan.c
1418: .P2
1419: .RE
1420: .IP
1421: An indication of the coverage of such a search can be derived from the
1422: .I "hash factor"
1423: (see below).
1424: The generated executable analyzer, named
1425: .CW run
1426: above, has its own set of options that can be seen by typing
1427: .CW "run -?"
1428: (see also below in ``The Analyzer'').
1429: .IP \f(CW-m\f1
1430: can be used to change the default semantics of send actions.
1431: Normally, a send operation is only executable if the target channel
1432: is non-full.
1433: This imposes an implicit synchronization that can not always
1434: be justified.
1435: Option \f(CW-m\f1 causes send actions to be always executable.
1436: Messages sent to a channel that is full are then dropped.
1437: If this option is combined with \f(CW-a\f1 the semantics of send
1438: in the analyzers generated is similarly altered, and the validations
1439: will take the effects of this type of message loss into consideration.
1440: .IP \f(CW-q\f1
1441: causes \*s to peruse the model for obviously atomicable
1442: sequences, and to label them appropriately, in an effort to
1443: reduce the complexity of large validation runs.
1444: Typically, the user can do better by hand (by being more
1445: daring than \*s can be in this case).
1446: .IP \f(CW-t\f1
1447: is a trail-hunting option.
1448: If the analyzer finds a violation of an assertion, a deadlock or
1449: an unspecified reception, it writes an error trail into a file
1450: named
1451: .CW pan.trail .
1452: The trail can be inspected in detail by invoking \*s with the
1453: .CW -t
1454: option.
1455: In combination with the options
1456: .CW pglrs
1457: different views of the error sequence are then easily obtained.
1458: .PP
1459: For brevity, other features of \*s are not discussed here.
1460: For details see|reference(holzmann spinbook), for a hint of
1461: what else is available, see ``Digging Deeper'' at the end of this manual.
1462: .IH "The Simulator"
1463: .PP
1464: Consider the following example protocol, that we will store in a
1465: file named
1466: .CW lynch .
1467: .P1 0
1468: 1 #define MIN 9
1469: 2 #define MAX 12
1470: 3 #define FILL 99
1471: 4
1472: 5 mtype = { ack, nak, err }
1473: 6
1474: .P3
1475: 7 proctype transfer(chan chin, chout)
1476: 8 { byte o, i, last_i=MIN;
1477: 9
1478: 10 o = MIN+1;
1479: .P3
1480: 11 do
1481: 12 :: chin?nak(i) ->
1482: 13 assert(i == last_i+1);
1483: 14 chout!ack(o)
1484: .P3
1485: 15 :: chin?ack(i) ->
1486: 16 if
1487: 17 :: (o < MAX) -> o = o+1
1488: 18 :: (o >= MAX) -> o = FILL
1489: 19 fi;
1490: 20 chout!ack(o)
1491: .P3
1492: 21 :: chin?err(i) ->
1493: 22 chout!nak(o)
1494: 23 od
1495: 24 }
1496: 25
1497: .P3
1498: 26 proctype channel(chan in, out)
1499: 27 { byte md, mt;
1500: 28 do
1501: 29 :: in?mt,md ->
1502: 30 if
1503: 31 :: out!mt,md
1504: 32 :: out!err,0
1505: 33 fi
1506: 34 od
1507: 35 }
1508: 36
1509: .P3
1510: 37 init
1511: 38 { chan AtoB[1] of { byte, byte };
1512: 39 chan BtoC[1] of { byte, byte };
1513: 40 chan CtoA[1] of { byte, byte };
1514: 41 atomic {
1515: 42 run transfer(AtoB, BtoC);
1516: 43 run channel(BtoC, CtoA);
1517: 44 run transfer(CtoA, AtoB)
1518: 45 };
1519: 46 AtoB!err,0; /* start */
1520: 47 hang
1521: 48 }
1522: .P2
1523: The protocol uses three message types: \f2ack\f1, \f2nak\f1, and
1524: a special type \f2err\f1 that is used to model message distortions
1525: on the communication channel between the two transfer processes.
1526: The behavior of the channel is modeled explicitly with a channel
1527: process.
1528: There is also an
1529: .CW assert
1530: statement that claims a (faulty) invariant
1531: relation between two local variables in the transfer processes.
1532: .PP
1533: Running \*s without options gives us a random simulation that
1534: will only provide output when execution terminates, or if
1535: a \f2printf\f1 statement is encountered.
1536: In this case:
1537: .P1 0
1538: $ spin lynch
1539: spin: "lynch" line 13: assertion violated
1540: #processes: 4
1541: proc 3 (transfer) line 11 (state 15)
1542: proc 2 (channel) line 28 (state 6)
1543: proc 1 (transfer) line 13 (state 3)
1544: proc 0 (:init:) line 48 (state 6)
1545: 4 processes created
1546: $
1547: .P2
1548: There are no \f2printf\f1's in the specification, but execution
1549: halts on an assertion violation.
1550: Curious to find out more, we can repeat the run with more verbose
1551: output, e.g. printing all receive events.
1552: The result of that run is shown in Figure 1.
1553: Most output will be self-explanatory.
1554: .PP
1555: The above simulation run ends in the same assertion violation.
1556: Since the simulation resolves nondeterministic choices in a
1557: random manner, this need not always be the case.
1558: To force a reproducible run, the option
1559: .CW -n\fIN
1560: can be used.
1561: For instance:
1562: .P1 0
1563: $ spin -r -n100 lynch
1564: .P2
1565: will seed the random number generator with the integer value 100
1566: and is guaranteed to produce the same output each time it is executed.
1567: .PP
1568: The other options can add still more output to the simulation run,
1569: but the amount of text can quickly become overwhelming.
1570: An easy solution is to filter the output through \f2grep\f1.
1571: For instance, if we are only interested in the behavior of the
1572: channel process in the above example, we say:
1573: .P1 0
1574: $ spin -n100 -r lynch | grep "proc 2"
1575: .P2
1576: The results are shown in Figure 1.
1577: .1C
1578: .KF
1579: .nf
1580: .ps -2
1581: .vs -3p
1582: .ft CW
1583: .TS
1584: box expand;
1585: l
1586: l.
1587: $ spin -r lynch
1588: proc 1 (transfer) line 21, Recv err,0 <- queue 1 (chin)
1589: proc 2 (channel) line 29, Recv nak,10 <- queue 2 (in)
1590: proc 3 (transfer) line 12, Recv nak,10 <- queue 3 (chin)
1591: proc 1 (transfer) line 15, Recv ack,10 <- queue 1 (chin)
1592: \&...
1593: proc 1 (transfer) line 15, Recv ack,12 <- queue 1 (chin)
1594: proc 2 (channel) line 29, Recv ack,99 <- queue 2 (in)
1595: proc 3 (transfer) line 15, Recv ack,99 <- queue 3 (chin)
1596: proc 1 (transfer) line 15, Recv ack,99 <- queue 1 (chin)
1597: proc 2 (channel) line 29, Recv ack,99 <- queue 2 (in)
1598: proc 3 (transfer) line 21, Recv err,0 <- queue 3 (chin)
1599: proc 1 (transfer) line 12, Recv nak,99 <- queue 1 (chin)
1600: spin: "lynch" line 13: assertion violated
1601: #processes: 4
1602: proc 3 (transfer) line 11 (state 15)
1603: proc 2 (channel) line 28 (state 6)
1604: proc 1 (transfer) line 13 (state 3)
1605: proc 0 (:init:) line 48 (state 6)
1606: 4 processes created
1607: $ spin -n100 -r lynch | grep "proc 2"
1608: proc 2 (channel) line 29, Recv nak,10 <- queue 2 (in)
1609: proc 2 (channel) line 29, Recv ack,11 <- queue 2 (in)
1610: proc 2 (channel) line 29, Recv ack,12 <- queue 2 (in)
1611: proc 2 (channel) line 28 (state 6)
1612: .TE
1613: .fi
1614: .ps +2
1615: .vs +3p
1616: .SP .5
1617: .ce
1618: \fBFigure 1.\fR Simulation Run Output
1619: .SP .5
1620: .KE
1621: .2C
1622: ......
1623: .IH "The Analyzer"
1624: .PP
1625: The simulation runs can be useful in quick debugging of
1626: new designs, but by simulation alone we can not prove
1627: that the system is really error free.
1628: A validation of even very large models can be performed with the
1629: .CW -a
1630: and
1631: .CW -t
1632: options of \*s.
1633: .PP
1634: An exhaustive state space searching program for a protocol
1635: model is generated as follows, producing five files, named \f2pan.[bchmt]\f1.
1636: .P1 0
1637: $ spin -a lynch
1638: .P3
1639: $ wc pan.[bchmt]
1640: .P3
1641: 92 326 2041 pan.b
1642: .P3
1643: 854 2502 17524 pan.c
1644: .P3
1645: 147 576 3475 pan.h
1646: .P3
1647: 307 1230 7493 pan.m
1648: .P3
1649: 177 548 3997 pan.t
1650: .P3
1651: 1577 5182 34530 total
1652: .P2
1653: The details are none too interesting: \f2pan.c\f1 contains
1654: most of the C code for the analysis of the protocol.
1655: File \f2pan.t\f1 contains a transition matrix that encodes
1656: the protocol control flow; \f2pan.b\f1 and \f2pan.m\f1 contain
1657: C code for forward and backward transitions and
1658: \f2pan.h\f1 is a general header file.
1659: The program can be compiled in two different ways: with a full
1660: state space or with a bit state space.
1661: .IH "Exhaustive Search"
1662: .PP
1663: The best method, that works up to system state spaces of
1664: roughly 100,000 states, is to use the
1665: default compilation of the program:
1666: .P1 0
1667: $ cc -o run pan.c
1668: .P2
1669: The executable program \f2run\f1 can now be executed to perform
1670: the validation.
1671: The validation is truly exhaustive: it tests all possible
1672: event sequences in all possible orders.
1673: It should, of course, find the same assertion violation.
1674: .P1 0
1675: $ run
1676: assertion violated (i == last_i + 1))
1677: pan: aborted
1678: pan: wrote pan.trail
1679: search interrupted
1680: vector 64 byte, depth reached 56
1681: 61 states, stored
1682: 5 states, linked
1683: 1 states, matched
1684: hash conflicts: 0 (resolved)
1685: (size 2^18 states, stack frames: 0/5)
1686: .P2
1687: The first line of the output announces the assertion violation
1688: and attempts to give a first indication of the invariant that
1689: was violated.
1690: The violation was found after 61 states had been generated.
1691: Hash "conflicts" gives the number
1692: of hash collisions that happened during access to the state space.
1693: As indicated,
1694: all collisions are resolved in full search mode, since all states are
1695: placed in a linked list.
1696: The most relevant piece of output in this case, however, is on the
1697: third line which tells us that a trail file was created that can
1698: be used in combination with the simulator to recreate the error
1699: sequence.
1700: We can now say, for instance
1701: .P1 0
1702: $ spin -t -r lynch | grep "proc 2"
1703: .P2
1704: to determine the cause of the error.
1705: Note carefully that the validator is guaranteed to find the
1706: assertion violation if it is feasible.
1707: If an exhaustive search does not report such a violation, it is
1708: certain that \f2no\f1 execution execution sequence exists that can
1709: violate the assertion.
1710: .IH Options
1711: .PP
1712: The executable analyzer that is generated comes with a modest
1713: number of options that can be checked as follows
1714: .P1 0
1715: $ run -?
1716: -cN stop at Nth error (default=1)
1717: -l find non-progress loops
1718: -mN max depth N (default=10k)
1719: -wN hash table of 2^N entries (default=18)
1720: .P2
1721: Using a zero as an argument to the first option
1722: forces the state space search to continue,
1723: even if errors are found.
1724: An overview of unexecutable (unreachable) code is given with every
1725: complete run: either the default run if it did not find any
1726: errors, or the run with option
1727: .CW -c0 .
1728: In this case the output is:
1729: .P1 0
1730: $ run -c0
1731: assertion violated (i == (last_i + 1))
1732: assertion violated (i == (last_i + 1))
1733: assertion violated (i == (last_i + 1))
1734: assertion violated (i == (last_i + 1))
1735: assertion violated (i == (last_i + 1))
1736: .P3
1737: vector 64 byte, depth reached 60, errors: 5
1738: 165 states, stored
1739: 5 states, linked
1740: 26 states, matched
1741: hash conflicts: 1 (resolved)
1742: (size 2^18 states, stack frames: 0/6)
1743:
1744: unreached code :init: (proc 0):
1745: reached all 9 states
1746: unreached code channel (proc 1):
1747: line 35 (state 9),
1748: reached: 8 of 9 states
1749: unreached code transfer (proc 2):
1750: line 24 (state 18),
1751: reached: 17 of 18 states
1752: .P2
1753: There were five assertion violations, and some 165 unique
1754: system states were generated.
1755: Each state description (the \f2vector size\f1) took up 64 bytes
1756: of memory; the longest non-cyclic execution sequence was 60.
1757: There is one unreachable state both in the channel process and in
1758: the transfer process.
1759: In both cases the unreachable state is the control flow point
1760: just after the do-loop in each process.
1761: Note that both loops are indeed meant to be non-terminating.
1762: .PP
1763: The \f(CW-l\f1 option will cause the analyzer to search for
1764: non-progress loops rather than deadlocks or assertion violations.
1765: The option is explained in the section on ``More Advanced Usage.''
1766: .PP
1767: The executable analyzer has two other options.
1768: By default the search depth is restricted to a rather
1769: arbitrary 10,000 steps.
1770: If the depth limit is reached, the search is truncated, making
1771: the validation less than exhaustive.
1772: To make certain that the search is exhaustive, make sure that the
1773: "depth reached" notice is within the maximum search depth, and
1774: if not, repeat the analysis with an explicit
1775: .CW -m
1776: argument.
1777: .PP
1778: The
1779: .CW -m
1780: option can of course also be used to truncate
1781: the search explicitly, in an effort to find the shortest possible
1782: execution sequence that violates a given assertion.
1783: Such a truncated search, however, is not guaranteed to find every
1784: possible violation, even within the search depth.
1785: .PP
1786: The last option
1787: .CW -w\fIN
1788: can only affect the run time, not
1789: the scope, of an analysis with a full state space.
1790: This "hash table width" should normally be set equal to,
1791: or preferably higher than,
1792: the logarithm of the expected number of unique system states generated
1793: by the analyzer.
1794: (If it is set too low, the number of hash collisions will increase
1795: and slow down the search.)
1796: The default
1797: .I N
1798: of 18 handles up to 262,144 system states, which should
1799: suffice for almost all applications of a full state space analysis.
1800: .IH "Bit State Space Analysis"
1801: .PP
1802: It can easily be calculated what the memory requirements of an analysis
1803: with a full state space are|reference(holzmann atttj).
1804: If, as in the example we have used, the protocol requires 64 bytes
1805: of memory to encode one system state, and we have a total of 2MB
1806: of memory available for the search, we can store up to 32,768 states.
1807: The analysis fails if there are more reachable states in the
1808: system state space.
1809: So far, \*s is the \f2only\f1 validation system that can avoid this trap.
1810: All other existing automated validation system (irrespective on
1811: which formalism they are based) simply run out of memory and
1812: abort their analysis without returning a useful answer to the user.
1813: .PP
1814: The coverage of a conventional analysis goes down rapidly when
1815: the memory limit is hit, i.e. if there are
1816: twice as many states in the full state space than we can store,
1817: the effective coverage of the search is only 50% and so on.
1818: \*S does substantially better in those cases by using the bit state
1819: space storage method|reference(holzmann atttj).
1820: The bit state space can be included by compiling the analyzer as follows:
1821: .P1 0
1822: $ cc -DBITSTATE -o run pan.c
1823: .P2
1824: The analyzer compiled in this way
1825: should of course find the same assertion violation again:
1826: .P1 0
1827: $ run
1828: assertion violated (i == ((last_i + 1))
1829: pan: aborted
1830: pan: wrote pan.trail
1831: search interrupted
1832: vector 64 byte, depth reached 56
1833: 61 states, stored
1834: 5 states, linked
1835: 1 states, matched
1836: hash factor: 67650.064516
1837: (size 2^22 states, stack frames: 0/5)
1838: $
1839: .P2
1840: In fact, for small to medium size problems there is very little
1841: difference between the full state space method and the bit state
1842: space method (with the exception that the latter is somewhat
1843: faster and uses substantially less memory).
1844: The big difference comes for larger problems.
1845: The last two lines in the output are useful in estimating
1846: the \f2coverage\f1 of a large run.
1847: The maximum number of states that the bit state space can
1848: accommodate is written on the last line (here @2 sup 22@ bytes or about 32 million
1849: bits = states).
1850: The line above it gives the \f2hash factor\f1: roughly
1851: equal to the maximum number of states divided by the actual
1852: number of states.
1853: A large hash factor (larger than 100) means, with high reliability,
1854: a coverage of 99% or 100%.
1855: As the hash factor approaches 1 the coverage approaches 0%.
1856: .PP
1857: Note carefully that the analyzer realizes a partial coverage \f2only\f1
1858: in cases where traditional validators are either unable to perform a
1859: search, or realize a far smaller coverage.
1860: In \f2no\f1 case will \*s produce an answer that is less reliable than
1861: that produced by other automated validation systems (quite on the contrary).
1862: .PP
1863: The object of a bit state validation is to achieve a hash factor
1864: larger than 100 by allocating the maximum amount of memory
1865: for the bit state space.
1866: For the best result obtainable: use the
1867: .CW -w\fIN
1868: option to size the state space to precisely the amount
1869: of real (not virtual) memory available on your machine.
1870: By default,
1871: .I N
1872: is 22, corresponding to a state space of 4MB.
1873: For example, if your machine has 128MB of real memory, you can use
1874: .CW -w27
1875: to analyze systems with up to a billion reachable states.
1876: .SP 2
1877: .NH
1878: \*P Reference Manual
1879: .PP
1880: This section describes the language \*P proper.
1881: As much as possible, the presentation follows the example
1882: from the
1883: .CW C
1884: reference manuals|reference(cbook).
1885: It does not cover possible restrictions or extensions of
1886: specific implementations.
1887: The current implementation of \*s, for instance,
1888: has an extra keyword
1889: .CW printf ,
1890: to access the corresponding
1891: .UX
1892: library function.
1893: .IH "Lexical Conventions"
1894: .PP
1895: There are five classes of tokens: identifiers, keywords, constants,
1896: operators and statement separators.
1897: Blanks, tabs, newlines, and comments serve only to separate tokens.
1898: If more than one interpretation is possible, a token is
1899: taken to be the longest string of characters that can
1900: constitute a token.
1901: .ix lexical conventions
1902: .ix tokens
1903: .IH Comments
1904: .PP
1905: Any string started with
1906: .CW /*
1907: and terminated with
1908: .CW */
1909: is a comment.
1910: Comments may not be nested.
1911: .ix comments
1912: .IH Identifiers
1913: .PP
1914: An identifier is a single letter, period, or underscore
1915: followed by zero or more letters, digits, periods, or underscores.
1916: .ix identifiers
1917: .IH Keywords
1918: .PP
1919: The following identifiers are reserved for use as keywords:
1920: .ix keywords
1921: .KS
1922: .ft CW
1923: .ps -1
1924: .vs -1
1925: .TS
1926: center;
1927: l l l.
1928: assert bit block
1929: bool break byte
1930: chan do fi
1931: goto halt if
1932: init int len
1933: mtype od of
1934: proctype run short
1935: skip timeout
1936: .ps +1
1937: .vs +1
1938: .TE
1939: .KE
1940: .IH Constants
1941: .PP
1942: A constant is a sequence of digits representing a decimal integer.
1943: There are no floating point numbers in \*P.
1944: .ix constants
1945: Symbolic names for constants can be defined in two ways.
1946: The first method is to use a C-style macro definition
1947: .P1 0
1948: #define NAME value
1949: .P2
1950: The second method is to use the keyword
1951: .CW mtype
1952: (see ``declarations'' below).
1953: .IH Expressions
1954: .PP
1955: The following operators can be used to build expressions.
1956: .ix expressions
1957: .ix operators
1958: .KS
1959: .TS
1960: center;
1961: lFCW.
1962: + \- * \/ %
1963: > >= < <= == != !
1964: && ||
1965: & | ~ >> <<
1966: .TE
1967: .KE
1968: .PP
1969: Most operators are binary.
1970: The logical negation \f2!\f1 and the minus \f2\-\f1
1971: operator can be both unary and binary, depending on context.
1972: Expressions are used, for instance, in assignments of the type
1973: .CW "a = expression" ,
1974: with
1975: .CW a
1976: a variable.
1977: .ix assignment
1978: There is also one unary operator that applies to message channels:
1979: .P1 0
1980: len
1981: .P2
1982: It measures the number of messages an existing channel holds.
1983: There is one unary operator that is used for process instantiations:
1984: .P1 0
1985: run
1986: .P2
1987: And, finally, there are two binary operators
1988: .P1 0
1989: ! ?
1990: .P2
1991: which are used for sending and receiving messages (see below).
1992: .IH Declarations
1993: .PP
1994: .ix declarations
1995: Processes, channels, and variables must be declared before they can be used.
1996: Variables and channels can be declared either locally,
1997: within a process, or globally.
1998: A process can only be declared globally in a
1999: .CW proctype
2000: declaration.
2001: Local declarations may appear anywhere in a process body.
2002: .IH Variables
2003: .PP
2004: .ix variables
2005: .ix local variables
2006: .ix global variables
2007: .ix initializers
2008: A variable declaration is started by a keyword indicating the
2009: basic data type of the variable,
2010: .CW bit ,
2011: .CW bool ,
2012: .CW byte ,
2013: .CW short ,
2014: or
2015: .CW int ,
2016: followed
2017: by one or more identifiers, optionally followed by
2018: an initializer.
2019: .P1 0
2020: byte name1, name2 = 4, name3
2021: .P2
2022: By default all variables are initialized to zero.
2023: An initializer, if specified, must be a constant.
2024: The table below summarizes the width and attributes of each
2025: basic data type.
2026: .KS
2027: .ps -1
2028: .vs -2
2029: .TS
2030: center;
2031: l l l
2032: lFCW n r.
2033: =
2034: Name Size (bits) Usage
2035: _
2036: bit 1 unsigned
2037: bool 1 unsigned
2038: byte 8 unsigned
2039: short 16 signed
2040: int 32 signed
2041: _
2042: .TE
2043: .ps +1
2044: .vs +2
2045: .KE
2046: The names \f2bit\f1 and \f2bool\f1
2047: are synonyms for a single bit of
2048: information.
2049: A \f2byte\f1 is an unsigned quantity that can store a value between
2050: 0 and 255.
2051: \f2Short\f1s and \f2int\f1s are signed quantities that
2052: differ only in the range of values they can hold.
2053: .PP
2054: An array of variables is declared as follows:
2055: .P1 0
2056: int name1[N]
2057: .P2
2058: where
2059: .CW N
2060: is a constant.
2061: An array can have a just a single constant as an initializer.
2062: If specified it is used to initialize all elements of the array.
2063: .PP
2064: Symbolic names for constants, e.g. message types,
2065: can, optionally, be defined in a declaration
2066: of the type
2067: .P1 0
2068: mtype = { namelist }
2069: .P2
2070: where
2071: .CW namelist
2072: is a comma separated list of symbolic names.
2073: .IH "Message Channels"
2074: .PP
2075: A message channel can be declared, for instance, as follows:
2076: .ix channels
2077: .P1 0
2078: chan name[N] of { short, short }
2079: .P2
2080: where
2081: .CW N
2082: is a constant that specifies the maximum number of messages
2083: that can be stored in the channel.
2084: A list of one or more data types (or the channel type
2085: .CW chan )
2086: enclosed in curly braces defines the type of the messages that can
2087: be passed through the channel.
2088: All channels are initialized to be empty.
2089: .IH Processes
2090: .PP
2091: .ix process
2092: A process declaration starts with the keyword
2093: .CW proctype
2094: followed by a name, a list of formal parameters
2095: enclosed in round braces, and
2096: a sequence of statements and local
2097: variable declarations.
2098: The body of process declaration is enclosed in curly braces.
2099: .P1 0
2100: proctype name( /* parameter decls */ )
2101: {
2102: /* statements */
2103: }
2104: .P2
2105: .IH Statements
2106: .PP
2107: .ix statements
2108: .ix gotos
2109: .ix labels
2110: .ix skip
2111: There are twelve types of statements:
2112: .KS
2113: .TS
2114: center;
2115: a a a.
2116: .ft CW
2117: .ps -1
2118: .vs -1
2119: assertion assignment atomic
2120: break declaration expression
2121: goto receive selection
2122: repetition send timeout
2123: .ft
2124: .ps +1
2125: .vs +1
2126: .TE
2127: .KE
2128: Each statement may be preceded by a label: a name followed by a colon.
2129: A statement can only be passed if it is executable.
2130: To determine its executability the statement can be evaluated:
2131: if evaluation returns a zero value the statement is blocked.
2132: In all other cases the statement is executable and can be passed.
2133: The act of passing the statement after a successful evaluation is
2134: called the ``execution'' of the statement.
2135: There are also three so-called \fIpseudo\fR-statements, which are
2136: really syntactic equivalents of specific variants of some of the
2137: above statements
2138: They are
2139: .P1
2140: skip block halt
2141: .P2
2142: equivalent to two conditions and an assert statement, respectively:
2143: .P1
2144: 1 0 assert(0).
2145: .P2
2146: .CW skip ,
2147: therefore, is a null statement; it is always executable.
2148: It has no effect when executed, but may be needed
2149: to satisfy syntax requirements.
2150: .CW block ,
2151: is never executable.
2152: The evaluation of an assertion statement
2153: .CW assert(condition)
2154: has no effect if the condition holds, but aborts the
2155: running process if evaluation of the condition returns a
2156: zero result (the boolean value ``false'').
2157: .CW halt ,
2158: therefore, effectively stops the execution of the system.
2159: .PP
2160: .CW goto
2161: statements can be used to transfer control to any labeled statement
2162: within the same process or procedure.
2163: They also are always executable.
2164: Assignments have been discussed above, they are
2165: always executable.
2166: A declaration is also always executable.
2167: Expressions are only executable if they return a non-zero value.
2168: That is, the expression \(CW0\fR (zero) is never executable, and
2169: similarly \(CW1\fR always is executable.
2170: Below we consider the remaining statements: selection, repetition,
2171: send, receive, break, timeout, and atomic statements.
2172: .IH Selection
2173: .PP
2174: .ix if statement
2175: .ix case selection
2176: .ix nondeterminism
2177: A selection statement is started with the keyword
2178: .CW if ,
2179: followed by
2180: a list of one or more `options' and terminated with the keyword
2181: .CW fi .
2182: Every `option' is started with the flag \f(CW::\fR followed by any sequence
2183: of statements.
2184: One and only one option from a selection statement will
2185: be selected for execution.
2186: The first statement of an option determines
2187: whether the option can be selected or not.
2188: If more than one option is executable, one will be selected at random.
2189: Note that this randomness makes the language a nondeterministic one.
2190: .IH "Repetition and Break"
2191: .PP
2192: .ix do statement
2193: .ix repetition
2194: A repetition or
2195: .CW do
2196: statement is similar to a selection statement, but is executed
2197: repeatedly until either a
2198: .CW break
2199: statement is executed or a
2200: .CW goto
2201: jump will transfer control outside the cycle.
2202: The keywords of the repetition statement are
2203: .CW do
2204: and
2205: .CW od
2206: instead of the
2207: .CW if
2208: and
2209: .CW fi
2210: of selection.
2211: The
2212: .CW break
2213: statement will terminate the innermost repetition
2214: statement in which it is executed.
2215: The use of a \(CWbreak\fR statement outside a
2216: repetition statement is illegal.
2217: ......
2218: .IH "Atomic Sequences"
2219: .PP
2220: The keyword
2221: .CW atomic
2222: introduces an atomic sequence of statements, that is
2223: to be executed as one indivisible step.
2224: The syntax is as follows
2225: .P1 0
2226: atomic { sequence }
2227: .P2
2228: Logically the sequence of statements is now equivalent
2229: to one single statement.
2230: It is a run-time error if any statement that is part of an
2231: atomic sequence is found to be unexecutable.
2232: The safest is therefore to include only assignments and
2233: local conditions in atomic sequences, but no sends or receives.
2234: Labeling local computations as atomic can bring an important
2235: reduction of the complexity of a validation model.
2236: For the lazy, \*s has an option (\f(CW-q\f1) that tries to find
2237: the most obvious ``atomicable'' sequences in the code,
2238: but the user can often do better by hand.
2239: .IH Send
2240: .PP
2241: .ix i/o statements
2242: .ix send
2243: The syntax of a send statement is:
2244: .P1 0
2245: expr1!expr2
2246: .P2
2247: where
2248: .CW expr1
2249: returns the identity of a channel, e.g. obtained from a
2250: .CW chan
2251: operation, and
2252: .CW expr2
2253: returns a value to be appended to the channel.
2254: The send statement is not executable (blocks) if the addressed channel is full
2255: or does not exist.
2256: .ix value transfer
2257: If more than one value is to be passed from sender to receiver, the expressions
2258: are written in a comma separated list:
2259: .P1 0
2260: expr1!expr2,expr3,expr4
2261: .P2
2262: Equivalently, this may be written
2263: .P1 0
2264: expr1!expr2(expr3,expr4) .
2265: .P2
2266: .IH Receive
2267: .PP
2268: .ix i/o statements
2269: .ix receive
2270: .ix value transfer
2271: The syntax of the receive statement is:
2272: .P1 0
2273: expr1?name
2274: .P2
2275: where
2276: .CW expr1
2277: returns the name of a channel and
2278: .CW name
2279: is a variable or a constant.
2280: If a constant is specified the receive statement is only executable
2281: if the channel exists and
2282: the oldest message stored in the channel contains the same value.
2283: If a variable is specified, the receive statement is executable
2284: if the channel exists and contains any message at all.
2285: The variable in that case will receive the value of the message
2286: that is retrieved.
2287: If more than one value is sent per message, the receive statement
2288: also take a comma separated list of variables and constants
2289: .P1 0
2290: expr1?name1,name2,...
2291: .P2
2292: which again is syntactically equivalent to
2293: .P1 0
2294: expr1?name1(name2,...)
2295: .P2
2296: Each constant in this list puts an extra condition on the
2297: executability of the receive: it must be matched by the
2298: value of the corresponding message field of the
2299: message to be retrieved.
2300: The variable fields retrieve the values of the corresponding
2301: message fields on a receive.
2302: .PP
2303: Placing square brackets around the clause after the `?'
2304: in the receiver operation converts it into a condition,
2305: that is true only if the corresponding receive operation
2306: is executable.
2307: It can be used freely in any type of composite boolean condition,
2308: and it has no side-effects when evaluated.
2309: .PP
2310: A last type of operation allowed on channels is
2311: .P1 0
2312: len(expr)
2313: .P2
2314: where
2315: .CW expr
2316: returns the identity of an instantiated channel.
2317: The operation returns the number of messages in
2318: the channel specified, or zero if the channel does not exist.
2319: .IH Timeout
2320: .PP
2321: The timeout condition is a modeling feature that by definition becomes true
2322: only if no statement in any of the running processes is executable.
2323: It has no effect when executed.
2324: .IH "Macros and Include Files"
2325: .PP
2326: .ix macros
2327: .ix include files
2328: .ix preprocessor
2329: The source text of a specification is processed by the C|reference(cbook)
2330: preprocessor for macro-expansion and file inclusions.
2331: .NH
2332: Summary
2333: .PP
2334: In the first part of this memo
2335: we have introduced a notation for modeling concurrent
2336: systems, including but not limited to asynchronous
2337: data communication protocols, in a language named \*P.
2338: The language has several unusual features.
2339: All communication between processes takes
2340: place via either messages or shared variables.
2341: Both synchronous and asynchronous communication
2342: are modeled as two special cases of a general message
2343: passing mechanism.
2344: Every statement in \*P can potentially model delay: it is
2345: either executable or not, in most cases depending on the state
2346: of the environment of the running process.
2347: Process interaction and process coordination is thus at
2348: the very basis of the language.
2349: More about the design of \*P, of the validator \*s, and
2350: its application to protocol design, can be found in |reference(holzmann spinbook).
2351: .PP
2352: \*P is deliberately a validation modeling language, not a programming language.
2353: There are, for instance, no elaborate abstract data types,
2354: or more than a few basic types of variable.
2355: A validation model is an abstraction of a protocol implementation.
2356: The abstraction maintains the essentials of the process interactions,
2357: so that it can be studied in isolation.
2358: It suppresses implementation and programming detail.
2359: .PP
2360: The syntax of \*P expressions, declarations, and assignments
2361: is loosely based on the language
2362: .CW C |reference(cbook).
2363: The language was influenced significantly by the ``guarded command languages''
2364: of E.W. Dijkstra |reference(dijkstra guarded) and C.A.R. Hoare
2365: |reference(hoare csp).
2366: There are, however, important differences.
2367: Dijkstra's language had no primitives for process interaction.
2368: Hoare's language was based exclusively on synchronous
2369: communication.
2370: Also in Hoare's language, the type
2371: of statements that could appear in the guards of an option was
2372: restricted.
2373: The semantics of the selection and cycling statements
2374: in \*P is also rather different from other guarded
2375: command languages: the statements are not aborted when all guards
2376: are false but they block: thus providing the required synchronization.
2377: .PP
2378: With minimal effort \*s allows the user to generate sophisticated
2379: analyzers from \*P validation models.
2380: Both the \*s software itself, and the analyzers it can generate,
2381: are written in ANSII C and are portable across
2382: .UX
2383: systems.
2384: They can be scaled to fully exploit the physical limitations
2385: of the host computer, and deliver within those
2386: limits the best possible analyses that can be realized
2387: with the current state of the art in protocol analysis.
2388: .NH
2389: References
2390: .LP
2391: |reference_placement
2392: .af H1 A
2393: .nr H1 1
2394: .nr H2 0
2395: .SH
2396: Appendix: Building A Validation Suite
2397: .PP
2398: The first order of business in using \*s for
2399: a validation is the construction of a
2400: faithful model in \*P of the problem at hand.
2401: The language is deliberately kept small.
2402: The purpose of the modeling is to extract those
2403: aspects of the system that are relevant to the
2404: coordination problem being studied.
2405: All other details are suppressed.
2406: Formally: the model is a reduction of the
2407: system that needs to be equivalent to the full system
2408: only with respect to the properties that are being validated.
2409: Once a model has been constructed, it becomes
2410: the basis for the construction of a series of,
2411: what we may call, ``validation suites'' that
2412: are used to verify its properties.
2413: To build a validation suite we can prime the
2414: model with assertions.
2415: The assertions can formalize invariant relations
2416: about the values of variables or about allowable
2417: sequences of events in the model.
2418: .NH 2
2419: An Example
2420: .PP
2421: As a first example we take the following solution
2422: to the mutual exclusion problem, discussed earlier,
2423: published in 1966 by H. Hyman in the Communications of the ACM.
2424: It was listed, in pseudo Algol, as follows.
2425: .P1 0
2426: 1 \f3Boolean array\f2 b(0;1) \f3integer\f2 k, i,\f(CW
2427: 2 \f3comment\f2 process i, with i either 0 or 1;\f(CW
2428: 3 \f2C0: b(i) := \f3false\f2;\f(CW
2429: 4 \f2C1: \f3if\f2 k != i \f3then begin\f2\f(CW
2430: 5 \f2C2: \f3if\f2 not (b(1-i) \f3then go to\f2 C2;\f(CW
2431: 6 \f3else\f2 k := i; \f3go to\f2 C1 \f3end\f2;\f(CW
2432: 7 \f3else\f2 critical section;\f(CW
2433: 8 \f2b(i) := \f3true\f2;\f(CW
2434: 9 \f2remainder of program;\f(CW
2435: 10 \f3go to\f2 C0;\f(CW
2436: 11 \f3end\f(CW
2437: .P2
2438: The solution, as Dekker's earlier solution, is for two processes,
2439: numbered 0 and 1.
2440: Suppose we wanted to prove that Hyman's solution truly
2441: guaranteed mutually exclusive access to the critical section.
2442: Our first task is to build a model of the solution in \*P.
2443: While we're at it, we can pick some more useful names for
2444: the variables that are used.
2445: .P1 0
2446: 1 bool want[2]; /* Bool array b */
2447: 2 bool turn; /* integer k */
2448: 3
2449: .P3
2450: 4 proctype P(bool i)
2451: 5 {
2452: 6 want[i] = 1;
2453: .P3
2454: 7 do
2455: 8 :: (turn != i) ->
2456: 9 (!want[1-i]);
2457: 10 turn = i
2458: .P3
2459: 11 :: (turn == i) ->
2460: 12 break
2461: 13 od;
2462: .P3
2463: 14 skip; /* critical section */
2464: 15 want[i] = 0
2465: 16 }
2466: .P3
2467: 17
2468: .P3
2469: 18 init { run P(0); run P(1) }
2470: .P2
2471: We can generate, compile, and run a validator for this
2472: model, to see if there are any major problems, such as
2473: a global system deadlock.
2474: .P1 0
2475: $ spin -a hyman0
2476: $ cc pan.c
2477: $ a.out
2478: full statespace search for:
2479: assertion violations and invalid endstates
2480: vector 20 byte, depth reached 19, errors: 0
2481: 79 states, stored
2482: 0 states, linked
2483: 38 states, matched total: 117
2484: hash conflicts: 4 (resolved)
2485: (size 2^18 states, stack frames: 3/0)
2486:
2487: unreached code _init (proc 0):
2488: reached all 3 states
2489: unreached code P (proc 1):
2490: reached all 12 states
2491: .P2
2492: The model passes this first test.
2493: What we are really interested in, however, is if
2494: the algorithm guarantees mutual exclusion.
2495: There are several ways to proceed.
2496: The simplest is to just add enough information
2497: to the model that we can express the correctness
2498: requirement in a \*P assertion.
2499: .P1 0
2500: 1 bool want[2];
2501: 2 bool turn;
2502: 3 byte cnt;
2503: 4
2504: .P3
2505: 5 proctype P(bool i)
2506: 6 {
2507: .P3
2508: 7 want[i] = 1;
2509: .P3
2510: 8 do
2511: 9 :: (turn != i) ->
2512: 10 (!want[1-i]);
2513: 11 turn = i
2514: .P3
2515: 12 :: (turn == i) ->
2516: 13 break
2517: 14 od;
2518: 15 skip; /* critical section */
2519: .P3
2520: 16 cnt = cnt+1;
2521: 17 assert(cnt == 1);
2522: 18 cnt = cnt-1;
2523: 19 want[i] = 0
2524: 20 }
2525: .P3
2526: 21
2527: .P3
2528: 22 init { run P(0); run P(1) }
2529: .P2
2530: We have added a global variable
2531: .CW cnt
2532: that is incremented upon each access to the
2533: critical section, and decremented upon each exit
2534: from it.
2535: The maximum value that this variable should ever
2536: have is 1, and it can only have this value when
2537: a process is inside the critical section.
2538: .P1 0
2539: $ spin -a hyman1
2540: $ cc pan.c
2541: $ a.out
2542: assertion violated (cnt==1)
2543: pan: aborted (at depth 15)
2544: pan: wrote pan.trail
2545: full statespace search for:
2546: assertion violations and invalid endstates
2547: search was not completed
2548: vector 20 byte, depth reached 25, errors: 1
2549: 123 states, stored
2550: 0 states, linked
2551: 55 states, matched total: 178
2552: hash conflicts: 42 (resolved)
2553: (size 2^18 states, stack frames: 3/0)
2554: .P2
2555: The validator claims that the assertion can be violated.
2556: We can use the error trail to check it with \*s's \f(CW-t\f1 option:
2557: .P1 0
2558: $ spin -t -p hyman1
2559: proc 0 (_init) line 24 (state 2)
2560: proc 0 (_init) line 24 (state 3)
2561: .P3
2562: proc 2 (P) line 8 (state 7)
2563: proc 2 (P) line 9 (state 2)
2564: .P3
2565: proc 2 (P) line 10 (state 3)
2566: proc 2 (P) line 11 (state 4)
2567: .P3
2568: proc 1 (P) line 8 (state 7)
2569: proc 1 (P) line 12 (state 5)
2570: .P3
2571: proc 1 (P) line 15 (state 10)
2572: proc 2 (P) line 8 (state 7)
2573: .P3
2574: proc 2 (P) line 12 (state 5)
2575: proc 2 (P) line 15 (state 10)
2576: .P3
2577: proc 2 (P) line 16 (state 11)
2578: proc 2 (P) line 17 (state 12)
2579: .P3
2580: proc 2 (P) line 18 (state 13)
2581: proc 1 (P) line 16 (state 11)
2582: .P3
2583: proc 1 (P) line 17 (state 12)
2584: spin: "hyman1" line 17: assertion violated
2585: .P3
2586: step 17, #processes: 3
2587: want[0] = 1
2588: _p[0] = 12
2589: turn[0] = 1
2590: cnt[0] = 2
2591: .P3
2592: proc 2 (P) line 18 (state 13)
2593: proc 1 (P) line 17 (state 12)
2594: proc 0 (_init) line 24 (state 3)
2595: 3 processes created
2596: .P2
2597: Here is another way to catch the error.
2598: We again lace the model with the information that
2599: will allow us to count the number of processes
2600: in the critical section.
2601: .P1 0
2602: 1 bool want[2];
2603: 2 bool turn;
2604: 3 byte cnt;
2605: 4
2606: .P3
2607: 5 proctype P(bool i)
2608: 6 {
2609: 7 want[i] = 1;
2610: .P3
2611: 8 do
2612: 9 :: (turn != i) ->
2613: 10 (!want[1-i]);
2614: 11 turn = i
2615: .P3
2616: 12 :: (turn == i) ->
2617: 13 break
2618: 14 od;
2619: .P3
2620: 15 cnt = cnt+1;
2621: 16 skip; /* critical section */
2622: 17 cnt = cnt-1;
2623: 18 want[i] = 0
2624: 19 }
2625: .P3
2626: 20
2627: .P3
2628: 21 proctype monitor()
2629: 22 {
2630: 23 assert(cnt == 0 || cnt == 1)
2631: 24 }
2632: .P3
2633: 25
2634: .P3
2635: 26 init {
2636: 27 run P(0); run P(1); run monitor()
2637: 28 }
2638: .P2
2639: The invariant condition on the value of counter
2640: .CW cnt
2641: is now place in a separate process
2642: .CW monitor()
2643: (the name is immaterial).
2644: The extra process runs along with the two others.
2645: It will always terminate in one step, but it
2646: could execute that step at \f2any\f1 time.
2647: The systems modeled by \*P and validated by \*s
2648: are completely asynchronous.
2649: That means that the validation of \*s take into
2650: account \f2all\f1 possible relative timings of
2651: the three processes.
2652: In a full validation, the assertion therefore
2653: can be evaluated at any time during the lifetime
2654: of the other two processes.
2655: If the validator reports that it is not violated
2656: we can indeed conclude that there is no execution
2657: sequence at all (no way to select relative speeds for
2658: the three processes) in which the assertion can be
2659: violated.
2660: The setup with the monitor process is therefore an
2661: elegant way to check the validity of a system invariant.
2662: The validation produces:
2663: .P1 0
2664: $ spin -a hyman2
2665: $ cc pan.c
2666: $ a.out
2667: assertion violated ((cnt==0)||(cnt==1))
2668: pan: aborted (at depth 15)
2669: pan: wrote pan.trail
2670: full statespace search for:
2671: assertion violations and invalid endstates
2672: search was not completed
2673: vector 24 byte, depth reached 26, errors: 1
2674: 368 states, stored
2675: 0 states, linked
2676: 379 states, matched total: 747
2677: hash conflicts: 180 (resolved)
2678: (size 2^18 states, stack frames: 4/0)
2679: .P2
2680: Because of the extra interleaving of the two processes
2681: with a third monitor, the number of system states that
2682: had to be searched has increased, but the error is again
2683: correctly reported.
2684: .br
2685: .NE 8v
2686: .NH 2
2687: Another Example
2688: .PP
2689: Not always can a correctness requirement be cast in
2690: terms of a global system invariant.
2691: Here is an example that illustrates this.
2692: It is a simple alternating bit protocol, modeling
2693: the possibility of message loss, and distortion,
2694: and extended with negative acknowledgements.
2695: .P1 0
2696: 1 #define MAX 5
2697: 2
2698: 3 mtype = { mesg, ack, nak, err };
2699: 4
2700: .P3
2701: 5 proctype sender(chan in, out)
2702: 6 { byte o, s, r;
2703: 7
2704: 8 o=MAX-1;
2705: 9 do
2706: 10 :: o = (o+1)%MAX; /* next msg */
2707: 11 again: if
2708: 12 :: out!mesg(o,s) /* send */
2709: 13 :: out!err /* distort */
2710: 14 :: skip /* or lose */
2711: 15 fi;
2712: .P3
2713: 16 if
2714: 17 :: timeout -> goto again
2715: 18 :: in?err -> goto again
2716: 19 :: in?nak(r) -> goto again
2717: 20 :: in?ack(r) ->
2718: 21 if
2719: 22 :: (r == s) -> goto progress
2720: 23 :: (r != s) -> goto again
2721: 24 fi
2722: 25 fi;
2723: 26 progress: s = 1-s /* toggle seqno */
2724: 27 od
2725: 28 }
2726: 29
2727: .P3
2728: 30 proctype receiver(chan in, out)
2729: 31 { byte i; /* actual input */
2730: 32 byte s; /* actual seqno */
2731: 33 byte es; /* expected seqno */
2732: 34 byte ei; /* expected input */
2733: 35
2734: 36 do
2735: 37 :: in?mesg(i, s) ->
2736: 38 if
2737: 39 :: (s == es) ->
2738: 40 assert(i == ei);
2739: 41 progress: es = 1 - es;
2740: 42 ei = (ei + 1)%MAX;
2741: 43 if
2742: 44 /* send, */ :: out!ack(s)
2743: 45 /* distort */ :: out!err
2744: 46 /* or lose */ :: skip
2745: 47 fi
2746: .P3
2747: 48 :: (s != es) ->
2748: .P3
2749: 49 if
2750: .P3
2751: 50 /* send, */ :: out!nak(s)
2752: 51 /* distort */ :: out!err
2753: 52 /* or lose */ :: skip
2754: .P3
2755: 53 fi
2756: .P3
2757: 54 fi
2758: 55 :: in?err ->
2759: 56 out!nak(s)
2760: .P3
2761: 57 od
2762: 58 }
2763: 59
2764: .P3
2765: 60 init {
2766: .P3
2767: 61 chan s_r [1] of { byte,byte,byte };
2768: 62 chan r_s [1] of { byte,byte,byte };
2769: .P3
2770: 63 atomic {
2771: .P3
2772: 64 run sender(r_s, s_r);
2773: 65 run receiver(s_r, r_s)
2774: .P3
2775: 66 }
2776: .P3
2777: 67 }
2778: .P2
2779: To test the proposition that this protocol will
2780: correctly transfer data, the model has already
2781: been primed for the first validation runs.
2782: First, the sender is setup to transfer an infinite
2783: series of integers as messages, where the value
2784: of the integers are incremented modulo
2785: .CW MAX .
2786: The value of
2787: .CW MAX
2788: is not really too interesting, as long as it is
2789: larger than the range of the sequence numbers in
2790: the protocol: in this case 2.
2791: We want to verify that data that is sent can only be
2792: delivered to the receiver without any deletions or reorderings,
2793: despite the possibility of arbitrary message loss.
2794: The assertion on line 40 verifies precisely that.
2795: Note that if it were ever possible for the protocol to
2796: fail to meet the above requirement, the assertion can be violated.
2797: .PP
2798: A first validation run reassures us that this is not possible.
2799: .P1 0
2800: $ spin -a ABP0
2801: $ cc pan.c
2802: $ a.out
2803: full statespace search for:
2804: assertion violations and invalid endstates
2805: vector 40 byte, depth reached 131, errors: 0
2806: 346 states, stored
2807: 1 states, linked
2808: 125 states, matched total: 472
2809: hash conflicts: 17 (resolved)
2810: (size 2^18 states, stack frames: 0/25)
2811:
2812: unreached code _init (proc 0):
2813: reached all 4 states
2814: unreached code receiver (proc 1):
2815: line 58 (state 24)
2816: reached: 23 of 24 states
2817: unreached code sender (proc 2):
2818: line 28 (state 27)
2819: reached: 26 of 27 states
2820: .P2
2821: But, be careful.
2822: The result means that all data that is delivered, is
2823: delivered in the correct order without deletions etc.
2824: We did not check that the data \f2will\f1 necessarily be delivered.
2825: It may be possible for sender and receiver to cycle
2826: through a series of states, exchanges erroneous messages,
2827: without ever making effective progress.
2828: To check this, the state in the sender and in the receiver
2829: process that unmistakingly signify progress, were labeled
2830: as a ``progress states.''
2831: (In fact, either one by itself would suffice.)
2832: .PP
2833: We should now be able to demonstrate the absence of
2834: infinite execution cycles that do not pass through any
2835: of these progress states.
2836: We can use the same executable from the last run, but
2837: this time we perform a loop-check.
2838: .P1 0
2839: $ a.out -l
2840: pan: non-progress cycle (at depth 6)
2841: pan: wrote pan.trail
2842: full statespace search for:
2843: assertion violations and non-progress loops
2844: search was not completed
2845: vector 44 byte, depth reached 8, loops: 1
2846: 12 states, stored
2847: 1 states, linked
2848: 0 states, matched total: 13
2849: hash conflicts: 0 (resolved)
2850: (size 2^18 states, stack frames: 0/1)
2851: .P2
2852: There are non-progress cycles.
2853: The first one encountered is dumped into the error trail
2854: by the validator, and we can inspect it.
2855: The results are shown in the first half of Figure 2.
2856: The channel can distort or lose the message infinitely often;
2857: true, but not too exciting as an error scenario.
2858: To see how many non-progress cycles there are, we can use the \f(CW-c\f1 flag.
2859: If we set its numeric argument to zero, only
2860: a total count of all errors will be printed.
2861: .P1 0
2862: $ a.out -l -c0
2863: full statespace search for:
2864: assertion violations and non-progress loops
2865: vector 44 byte, depth reached 137, loops: 92
2866: 671 states, stored
2867: 2 states, linked
2868: 521 states, matched total: 1194
2869: hash conflicts: 39 (resolved)
2870: (size 2^18 states, stack frames: 0/26)
2871: .P2
2872: There are 92 cases to consider, and we could look at each
2873: one, using the \f(CW-c\f1 option (\f(CW-c1\f1, \f(CW-c2\f1, \f(CW-c3\f1, ...etc.)
2874: But, we can make the job a little easier by at least
2875: filtering out the errors caused by infinite message loss.
2876: We label all loss events (lines 13, 43, and 48) as
2877: progress states, using label names with the common 8-character
2878: prefix ``progress,'' and look at the cycles that remain.
2879: (Labels go behind the ``::'' flags.)
2880: .P1 0
2881: $ spin -a ABP1
2882: $ cc pan.c
2883: .P3
2884: $ a.out -l
2885: pan: non-progress cycle (at depth 133)
2886: pan: wrote pan.trail
2887: .P3
2888: full statespace search for:
2889: assertion violations and non-progress loops
2890: search was not completed
2891: .P3
2892: vector 44 byte, depth reached 136, loops: 1
2893: .P3
2894: 148 states, stored
2895: 2 states, linked
2896: 2 states, matched total: 152
2897: .P3
2898: hash conflicts: 0 (resolved)
2899: (size 2^18 states, stack frames: 0/26)
2900: .P2
2901: This time, the trace reveals an honest and a serious bug in the protocol.
2902: The second half of Figure 2 shows the trace-back.
2903: .1C
2904: .KF
2905: .nf
2906: .ps -2
2907: .vs -3p
2908: .ft CW
2909: .TS
2910: box expand;
2911: l
2912: l.
2913: $ spin -t -r -s ABP0
2914: <<<<<START OF CYCLE>>>>>
2915: proc 1 (sender) line 13, Send err,0,0 -> queue 2 (out)
2916: proc 2 (receiver) line 55, Recv err,0,0 <- queue 2 (in)
2917: proc 2 (receiver) line 56, Send nak,0,0 -> queue 1 (out)
2918: proc 1 (sender) line 19, Recv nak,0,0 <- queue 1 (in)
2919: spin: trail ends after 12 steps
2920: step 12, #processes: 3
2921: _p[0] = 6
2922: proc 2 (receiver) line 36 (state 21)
2923: proc 1 (sender) line 11 (state 6)
2924: proc 0 (_init) line 67 (state 4)
2925: 3 processes created
2926: $
2927: $ spin -t -r -s ABP1
2928: \&...
2929: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2930: proc 2 (receiver) line 47, Send err,0,0 -> queue 1 (out)
2931: proc 1 (sender) line 20, Recv err,1,0 <- queue 1 (in)
2932: proc 1 (sender) line 12, Send mesg,0,0 -> queue 2 (out)
2933: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2934: proc 2 (receiver) line 52, Send nak,0,0 -> queue 1 (out)
2935: proc 1 (sender) line 21, Recv nak,0,0 <- queue 1 (in)
2936: proc 1 (sender) line 12, Send mesg,0,0 -> queue 2 (out)
2937: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2938: proc 2 (receiver) line 52, Send nak,0,0 -> queue 1 (out)
2939: <<<<<START OF CYCLE>>>>>
2940: proc 1 (sender) line 21, Recv nak,0,0 <- queue 1 (in)
2941: proc 1 (sender) line 12, Send mesg,0,0 -> queue 2 (out)
2942: proc 2 (receiver) line 39, Recv mesg,0,0 <- queue 2 (in)
2943: proc 2 (receiver) line 52, Send nak,0,0 -> queue 1 (out)
2944: spin: trail ends after 226 steps
2945: \&...
2946: .TE
2947: .fi
2948: .ps +2
2949: .vs +3p
2950: .SP .5
2951: .ce
2952: \fBFigure 2.\fR Error Trails - Extended Alternating Bit Protocol
2953: .SP .5
2954: .KE
2955: .2C
2956: .PP
2957: After a single positive acknowledgement is distorted
2958: and transformed into an
2959: .CW err
2960: message, sender and receiver get caught in an infinite
2961: cycle, where the sender will stubbornly repeat the last
2962: message for which it did not receive an acknowledgement,
2963: and the receiver, just as stubbornly, will reject that
2964: message with a negative acknowledgment.
2965: .NH 2
2966: Digging Deeper
2967: .PP
2968: This manual can only give an outline of the
2969: main features of \*s, and the more common
2970: ways in which it can be used for validations.
2971: There is a small number of \*s features that
2972: have not been discussed here, but that may be useful
2973: for tackling non-standard validation problems.
2974: \*S, for instance, can give \*P processes access
2975: to extra system information, such as the current
2976: values of normally invisible local variables,
2977: or the current execution states of remote processes.
2978: With this extra information it may be easier in
2979: some cases to build accurate assertions about
2980: required system behavior.
2981: .PP
2982: \*S also allows for a straightforward validation of ``tasks.''
2983: That is, if the user formalizes a task that is claimed to be
2984: performed by the system, \*s can quickly either prove or
2985: disprove that claim.
2986: The tasks can be used directly to verify any
2987: propositional temporal logic formula
2988: on the behavior of a system.
2989: .PP
2990: \*S also allows the user to formalize ``reductions'' of
2991: the system state space, which can be used
2992: to restrict a search it to a user defined subset.
2993: With this method it becomes trivial to verify quickly
2994: whether or not a given error pattern is within the range of
2995: behaviors of a system, even when a complete validation is
2996: considered to be infeasible.
2997: .PP
2998: For details about these alternative uses of \*P and
2999: 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.