Return to spin.ms_o CVS log

Up to [Research Unix] / researchv10dc / vol2 / spin

Annotation of researchv10dc/vol2/spin/spin.ms_o, revision 1.1

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.