SPIN & Promela

Page Contents

Promela Notes

Symbolic Names & Variables

Almost equivalent of a C enum. Use the mtype declaration to introduce symbolic names for constant values.

mtype = {SYM_NAME 1, SYM_NAME_2, ... };
mtype my_variable = SUM_NAME_1 // Default would be zero

The symbol names have unique positive integer Ids.

The word mtype is short for "message type" and although usually defining values for types of messages between promela-processes can be used otherwise.

Promela Processes

The keyword proctype declares a promela-process. May be preceeded with the keyword active to start an instance of the promela-process automatically.

Note use of "promela-process" v.s. "process".

Example:

active [n] proctype some_name()
{
   printf("Do something\n")
}

The above starts n promela-processes of type some_name. The [n] can be ommitted, and is so it is like writing [1].

When more than 1 promela-process could continue to run, the choice of which gets to run is randomly made. This means no assumptions are made about scheduling.

Processes can be run manually from the init block, although this is less favourable as it creates another process (the init process), which could bloat a verification state space unecessarily.

proctype some_name(int a)
{
   printf("Do something %d\n", a)
}

init {
   run some_name(1);
   run some_name(2);
}

We can constrain a process using the provided keyword. A promela-process cannot take any step unless the provided class is true.

active [n] proctype some_name() provided (some-boolean-expression)
{
   printf("Do something\n");     // This line won't execute until `some-boolean-expression` is true
   printf("Do something else\n") // Neither will this line. 
                                 // Its like each line is guarded by `some-boolean-expression`
}

Scope

The only scopes are global and process-local. Thus variables cannot be scoped to, for example, an if statement. Variables cannot be used until they are declared - there is no JavaScript style hoisting.

In the global scope all promela-processes can see the variable. In the process-local scope only the process can see the variable.

Data Types

bit 0, 1
bool false, true
byte 0...255
chan 1...255
mtype 1...255
pid 0...255
short -215...215-1
int -231...231-1
unsigned0...2n-1

Data Structures

Thing C-style structures

typedef MyType {
   short myShort = 3;
   byte  myByte;
   unsigned myUnsigned : 5 /*< 5 bit unsigned integer */
};

proctype myProc(MyType t) {
   t.myShort = 3;
}

Flow Control & Execution

Execution

All conditional statements guard execution, and can block, whether or not they have any instructions to execute after the guard or not.

...
(x == y) ->
...

In the above snippet the promela-process executing the code will block at the line (x == y) -> until the condition is true. As there are no statements after the arrow, it will just block and when the condition becomes true continue onto the next line.

In promela every type of statement can act as a guard in any context, even when used standalone. But note, it should not have side effects! Only run(...) is allowed to have a side effect.

Things like prints or assignments are immediately executable.

Expressions which evaluate to false guaranteeably have no side effects.

Do Loop

A do loop looks like the following. It consists of a set of guard conditions. The guard conditions are evaluated on each iteration.

If a guard evaluates to true then it is said to be executable.

If no guard is executable the promela-process blocks until one is. Otherwise one branch out of the set of all executable branches is chosen at random.

do
:: boolean-guard-1 -> printf("Execute choice 1");  // What follows the guard is the
                      printf("do something 1")     // "execution sequence "
:: boolean-guard-2 -> printf("Execute choice 2");
                      printf("do something 2")     // Note last statement in sequence
                                                   // has no trailing semi-colon. The semi-
                                                   // colon is a seperator, not a terminator.
...
:: boolean-guard-n -> printf("Execute choice n");
                      printf("do something n")
od

Exit a loop using the break statement or the goto statement.

The arrow is just a nice syntactic sugar for the guard. It is equivalent to a semi-colon. We could write it like this:

do
:: boolean-guard-1; printf("Execute choice 1");
                    printf("do something 1")
:: boolean-guard-2; printf("Execute choice 2");
                    printf("do something 2")
...
od

To avoid blocking if no guard is true you can use the else keyword:

do
:: boolean-guard-1 -> printf("Execute choice 1")
:: else -> printf("Won't block and does busy waiting")
od

The keyword else will only evaluate to true if and only if all other guards are false. When else is selected it is therefore the only executable option.

Selection / If

Same execuation rules as for do loop:

if
:: boolean-guard-1; printf("Execute choice 1");
                    printf("do something 1")
:: boolean-guard-2; printf("Execute choice 2");
                    printf("do something 2")
...
fi

Atomic Sequences

All statements in an atomic sequence are executed without interruption by another promela-process. It is a type of compund statement.

An atomic sequence can have a guard (the first statement), in which case the guard determines whether the sequence runs, and when it does run, it does so atomically.

Write a sequence as follows:

atomic { boolean-guard-condition -> statment1; statement2; ... }

Sequences can included flow control and be non-deterministic (control structures with multiple true guards can randomly choose a path).

Warning: If any statement in the sequence, other than the guard blocks, the atomicity is broken at the point of blocking and re-gained when unblocking occurs.

Deterministic Steps

Like atomic sequences except no non-determinism (control structures will deterministically choose a path when multiple guards are true), no jumps, and may not contain blocking statements other than the guard. It is a type of compund statement.

Macros / Inline Functions

An inline "function" behaves, in many ways, like a C pre-processor macro does. The word "function" is in quotes because it is not a function! It is just some nice syntactic sugar that defines a macro.

inline macro_name(param1, ...) {
// Do some stuff
}

To see the result of preprocessing pass the -I option to SPIN.

Not that because this is a pre-processor substition the statements in the inline body are not atomic unless you explicitly mark them so.

Special Variables

_pid

Read-only, local variable. Evaluates to numeric ID of currently running promela-process.

Variables holding numeric IDs should be of type pid. E.g.:

pid myvar = _pid;

timeout

Read-only boolean variable. Is true when no other statement in the entire system is executable. False otherwise.

Don't Care Dummy Write Variable

The underscore (_).

Message Passing

Promela channels are used to pass messages between asynchronous promela-processes. Every channel has its own unique ID.

Declaring Channels

Declare channels using the chan keyword:

mtype = { some, set, of, symbolic_constants };
...
chan CHAN_NAME = [n] of { mtype, ... } 

Where n is zero or a positive integer declaring how many items the channel can hold until it blocks. Thus if n == 0, the channel will immediately block a sender until a receiver reads the value being sent (creates a rendez-vous). If n == 1 the sender can send 1 value to an empty channel without blocking. If the channel already has a message in it the sender would block, and so on...

The type of message is either a symbolic constant, in which case, for example we could declare:

chan CHAN_NAME = [1] of {mtype}

Or the message can be an aggregate (think structure in C):

chan CHAN_NAME = [1] of {mtype, int, bit, user-defined, ...}

Sending / Receiving From Channels

To send a message into a channel:

CHAN_NAME!expr1[, expr2, ...]
CHAN_NAME!expr1(expr2[, ...]) // equivalent to the above

The default is that the send is executable only if there is space in the channel otherwise it will block.

To receive a message of particular type from a channel:

CHAN_NAME?var1[, var2, ...]
CHAN_NAME?var1(var2[, ...]) // equivalent to the above

The default is that the receive is executable only if there is a message in the channel otherwise it will block.

The above will receive messages into the listed variables. If you specify constants instead, the statement is only executable if the constants match the message to be read.

If we want to use a variable as-if it were a constant to constrain what can be received surround the variable with eval(varname).

Constrain Channel Usage (Make Verification Quicker)

Use xr, meaning exclusive read, and xs for exculsive send as shown:

chan b = [1] of { ... }
chan c = [1] of { ... }
active proctype proc1() {
   xs b; /* assert proc1 only sends to b */
   xr c; /* assert proc2 only receives from c */
}

Helps reduce amount of work verification algorithm has to do by providing some hints about the channel usage in the model. They are assertions that will be checked during a validation.

Other Channel Operations

Length: Use len(chanName) to get the number of messages in a channel.

Emptiness: Use empty/nempty(chanName) to see if channel is empty/not-empty.

Full: Use full/nfull(chanName) to see if channel is full/not-full.

Would progress: To find out if a send/receive would be executable you cannot use chan!expr or chan?const_or_var as these expressions both have side effects.

Instead use chan![expr] or chan?[const_or_var]. These only examine the precondition for the execution of the statement, but don't actually execute it.

Read but don't dequeue: chanName?<var_or_const>

Linear Temporal Logic

Automata

Finite State Automaton is defined by a tuple (S, s_0, L, T, F) where:

S is a finite set of states
s_0 is the initiatial state such that s_0 \in S
L is a finite set of labels
T is a set of transitions, T \subseteq (S \times L \times S) , and
F is a set of final states

For example, look at the following automaton:

Picture of a finite automaton

For this automaton we have:

S = \{ s_0, s_1, s_2, s_3 \}
s_0 is the initiatial state such that s_0 \in S
L = \{ a, b, c \}
T \subseteq (S \times L \times S) = \left\{ \{s_0, a, s_1\}, \{s_0, b, s_2\}, \{s_1, c, s_2\}, \{s_2, d, s_1\}, \{s_2, e, s_3\} \right\} , and
F = \{ s_3 \}

Why is this interesting? It is interesting because we can represent concurrent activity as a set of states. Imagine the following promela program:

mtype = { A, B }
mytype state = A

active proctype proc1()
{
    do
    :: state = A
    od
}


active proctype proc2()
{
    do
    :: state = B
    od
}

We can represent the state of the program as follows:

An this is just for a super simple program! If there was more than one variable then the state would consist of a tuple of all the variables. In this way SPIN can take a Promela program and convert it into a finite automaton (FA) and use this to search all the possible states for us (not infinitely although the above tree grows infinitely, the state space is finite - S = \{A, B\} ).

The above automotons are all deterministic (and when finite known as DFA). From each state there is only one path to the next state.

A non-deterministic automaton (if finite known by the abreviation NFA) is one where from at least one state there is more that one path out of that state. But, there are algorithms to convert NFAs to equivalent DFAs.

Runs

A run of a FA is a an ordered sequence of transitions - possibly infinite. For example R = \{ (s_0, l_0, s_1), (s_1, l_1, s_2), \ldots \} : \forall i,j,k, (i,j,k \ge 0) \implies (s_i, l_j, s_k) \in T) .

An accepting run is one where the final state is in the set of end states (implicity all the end states are seen as accepting).

Runs defined in this way are all terminating. But what about infinite loops through states? These may or may not be a good thing. These runs must be infinite and are referred to as \omega -runs. The set of transitions that occur infinitely often in the run are denoted \sigma^\omega and other states \sigma^+ .

An accepting \omega -run is one where \exists s_f: s_f \in F \land s_f \in \sigma^\omega - the Buchi acceptance definition. I.e., an accepting \omega -run is a loop when at least one state is visited infinitely often.

This rule is extended to finite runs using the stutter extension rule which adds an end state that can be repeated infinitely often.

SPIN Notes

Types Of Claims

SPIN is concerned about what is and isn't possible, not what is good or bad, or probable and improbable.

To allow SPIN to tell you about what is and isn't possible you need to make claims about your model. You can make,

  1. Claims about reachable/unreachable states, and
  2. Claims about feasible/infeasible executions (i.e., paths forming state transitions). E.g., every time state P is visited, subsequently state Q should eventually be visited.

SPIN automatically checks for deadlocks (unintended end states).

A system invariant should be true for every reachable state in the system. A process invariant is true only for every state reachable in a process.

Basic Assertions

Basic assertions use the assert(expr) statement. The expr should always evaluate to true (or non-zero int). If it does not SPIN considers this an error and fails the model.

End States

Only default valid end state is when every promela-process has terminated. Verification checks no invalid end states can be reached, which is a saftey issue.

To mark alternative states as valid end states use end-state labels. Labels must be unique to their proctype. Every label that starts with the prefix end marks a valid end state.

To make sure all promela-processes are in a valid end state at the end of verification and additionally that all message queues are empty use the -q with the compiler verifier.

Progress (Liveness) States

Used to specify livenesss properties.

Similar syntax to end states but use labels with the prefix progress to mark statements that accomplishes something - allows infinite cycles to be seen as "good" rather than an error condition that signals that a process is stuck making no progress.

See the SPIN command line usage on how to search for no-progress cycles. Enabling NP searching disables the search for invalid end states (safety).

Faireness

Every process that can execute a statement will eventually do so. I.e., no starvation. There are two types of faireness: weak and strong faireness.

[Weak fairness] states that if a process reaches a point where it has an executable statement, and the executability of that statement never changes, it will eventually proceed by executing the statment...

...[Strong faireness] states that if the process reaches a point where it has a statement that becomes executable intinitely often, it will eventually proceeed by executing the statement.

-- The SPIN Model Checker, Primer and Reference Manual, G. J. Holzmann.

See the SPIN command line usage on how enforce weak fairness. This adds a computational burden to the verification so it will be slower. Strong fairness no supported as too computationally expensive.

Accept States

Mostly used with a never claim. Used to find execution paths that do pass through at least one accept state(s) but not infinitely often - use label prefix accept.

Never Claims

Claims that apply to every state in the entire system and all times, i.e. at every execution step of the system.

Ignored in simulation mode. Only used in verification mode. Help capture liveness requirments.

Example of checking system invariant p, taken from "The SPIN Model Checker, Primer and Reference Manual" by G. J. Holzmann.

never {
   do
   :: !p -> break /* } Replace both lines with assert(p) */
   :: else        /* } for equivalent behaviour          */
   od
}

If the invariant is ever broken, i.e. !p, the never claim exits, which signals to SPIN that a violation has occured. Expressions in the claim must be side effect free!

Note the use of else. As the claim is to be checked at each statement execution the loop must not block, although it is permissible for never claims to block.

A more comples example from "The SPIN Model Checker" book (annotation mine):

/* CHECK that every state in which p is true eventually leads to a state
 * in which q is true, and in the interim, p remains true.
 *
 * SPIN checks for VIOLATIONS of this property only (i.e., does not check
 * satisfaction).*/
never {
S0:    do
       :: p && !q -> break   /* p is true AND q is false -> expect q to become true */
       :: true               /* Always executable, which is how we get the...       */
       od                    /* ..."eventually leads to a true " because even...   */
                             /* ...when (p &&!q) is true, this branch could...      */
                             /* ...execute instead. Also allows for p to go false   */
                             /* ... and then true again before we hit our condition.*/
S1:
accept:                      /* Remaining in this loop is a valid end state         */
/* The loop blocks when p and q true in this accept state and the claim STOPS...    */
/* ...tracking system execution - we don't have to create another infinite accept...*/
/* ...state */
       do
       :: !q                 /* p is any AND q is false **forever**. Must mark as...*/
                             /* ... valid end state, otherwise q never becoming...  */
                             /* ... true would be an error!                         */
       :: !(p || q) -> break /* p is false AND q is false -> true p did not reach...*/
                             /* ...a true q!                                        */
       od
/* The loop will exit (and cause a claim violation) if !p && !q */
}

Trace Assertions

Used for message channels. All referenced channels must be global and all choices must be deterministic.

An example from the SPIN book:

trace {
   do
   :: q1!a; q2:b /* Says all ops on queue q1 must be send a, receive b, repeat */
   od
}

A trace assertion can only use simple queue operations. Values matched must be constants or mtype or the special variable _, which means "don't care ".

Use notrace blocks to achieve the exact opposite.

SPIN Command Line

Limit Simulation Steps

The following limits the simulation exection to n steps:

spin -u<n> file.pml

For example, to limit it to 50 steps we would write:

spin -u50 file.pml

Columnated Output

To just get the prinf output, one column per process:

spin -c file.pml

Generate Verification model

spin -a filename.pml
cc -o pan pan.c
./pan

If there are any errors a trail file will be output named filename.pml.trail.

Find Shortest Execution Trace

If a tail fails in <n> steps, to find the shortest possible path to failure less than or equal to n steps:

spin -t file.pml
cc -DREACH -o pan pan.c
./pan -i -m<n>

Alternatively compile to use breadth first search:

cc -DBFS -o pan pan.c
./pan

Guided Simulation (Use A Trail File)

To replay a trail file in a simulation:

spin -p -t file.pml

Stricter End States - Message Queues Must Be Empty

By defailt when verification ends all promela-processes must be in a valid end state but the message queues do not have to be empty. To make this stricter and require that message queues also be empty use the -q with the compiled verifier.

Search For No Progress Cycles

spin -a file.pml     # Compile the verifier
cc -DNP -o pan pan.c # Enable search for no-progress cycles.
./pan -l [-f]        # Search for NP cycles.
#        ^^^^
#        Enforce weak fairness (strong fairness too computationally expensive)

Docker Image

Bit of a Linux tool so to run on Windows using Docker the following will create a little image which can run SPIN...

FROM ubuntu

RUN apt update -y && \
    apt install -y vim build-essential spin