Skip to Content

Spin: A Sound and Complete Verification Tool

Posted on 16 mins read

Spin is a system/protocol/algorithm verification tool. It is in a class known as model checkers, because it lets you create a model of your system and then it exhaustively checks the model for desired properties.

It is pretty easy to use, as it is written in C code and is easily compilable.

Compiling

The Spin code is pretty simple, and make should work as is, maybe with a little customization. The makefile in the Src/ directory has directions and suggestions in it for various platforms, including Windows and MacOS. You do need to have the yacc tool installed (or bison, with an alias). I have never used the Tcl/Tk GUI that is included (it is optional), but compiling Spin does not depend on this.

Spin Workflow Summary

The general workflow of using Spin is:

  1. Create/edit your Promela model in a text file with a “.prom” extension
  2. Simulate your model using “spin modelname.prom”
  3. Repeat steps 1-2 until you believe your model is ready for verification
  4. Generate a verifier using “spin -a modelname.prom”
  5. Compile the verifier using “gcc -o pan pan.c”
  6. Run the verifier using “./pan <options>” (you may or may not need options)
  7. If the verifier found errors, figure out the error using “spin -t -p modelname.prom”
  8. Repeat at step 1 until you have a correct, verified model

The most important option in step 6 is “-m#”, which increases the verifier search depth. This is almost always needed. The number in place of “#” should be big, like 10 million or so.

Note that if you edit/change your model, you must generate a new verifier, and if you generate a new verifier, you must compile the new verifier. Forgetting these steps and running an old verifier after you changed your model will result in much frustration!

The spin tool itself has lots of options, there are compile-time definitions to customize a verifier, and the compiled verifier has lots of options. If you want to become an expert in spin, you must seek other resources than my brief summary here!

Spin Models: The Promela Language

The first step in using Spin is creating a description, or model, of the system, protocol, or algorithm that you want to verify. Spin uses a language called Promela for this. It is important to remember, that even though Promela looks like a programming lanaguage, it is not. It is a modeling language.

The concise Promela reference is a good place to start, and there are other resources on the Spin website. For detailed information on each language feature and keyword the Promela Language Reference is the place to go.

Four things are important to understand about creating Promela models (i.e., writing Promela code):

  1. Promela is concurrent-process-oriented. The keyword proctype is used to declare template code for a new process, it is not used to write a function. There are no functions in Promela. The keyword run must be used to actually create a new process. Multiple processes of the same proctype can be created (using multiple run statements, or a loop).
  2. The keyword inline can be used to organize your code, but it does not create a function. Again, Promela does not have functions. The inline keyword creates a macro, which is an code segment that can be expanded in (or dropped into) the place where it is used. Using a macro looks a lot like calling a function, but it is not! Macros do not have their own local variables (but v6+ does), and macro arguments are very basic and are not function parameters but rather string substitutions.
  3. There is no input. Newer versions of Spin do allow some basic input for model simulation, but this only helps in model debugging, it plays no role in verification. For verification, you must write code to generate all possible inputs you need.
  4. Control structures are non-deterministic in simulation, and exhaustive in verification. The if control block and the do control loop use guarded commands to select between options. If no guarded commands are true, the process blocks until at least one becomes true. If more than one are true, then one is “randomly” chosen during simulation, but during verification all possible path choices are explored. The keyword guard else is only true if all other guards are false; it can be used both in if and do control blocks.

A Simple Example and Tool Use Process

Below is a simple Promela model:

int val;

proctype incrementBy(int amt)
{
   int localv;
   printf("Increment val by %d!\n",amt);
   localv = val+amt;
   val = localv;
}

init {
   val = 4;
   printf("val = %d\n", val);
   run incrementBy(2);
   run incrementBy(3);
   timeout ->
   printf("val = %d\n", val);
   assert (val == 9);
}

This model create two concurrent processes that attempt to each increment a shared variable by an amount. After they are finished (the timeout keyword waits for them), we assert that we expect the value of our variable to be 9, which it will be if all the increments happen properly.

We can simulate (think of as “run”) the model by invoking spin on it without any arguments:

jcook@jcook-dellxps:~/cs581/spin$ spin inc.prom 
      val = 4
          Increment val by 2!
              Increment val by 3!
      timeout
      val = 9
3 processes created

It worked! Note that each process has its own print indentation level, so that you can easily see what each process is doing. The first level is the init process.

So maybe now we believe that our system always leaves 9 in the variable. Well, now we need to verify that this is true. Verification is a three-step process:

  1. Generate a verifier using “spin -a”
  2. Compile the verifier using “gcc -o pan pan.c”
  3. Run the verifier using “./pan”

Let’s try this out:

jcook@jcook-dellxps:~/cs581/spin$ spin -a inc.prom 
jcook@jcook-dellxps:~/cs581/spin$ gcc -o pan pan.c
pan.c: In function ‘findtrail’:
pan.c:1540:24: warning: ‘sprintf’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
 1540 |   { sprintf(fnm, "%s.%s", MyFile, tprefix);
...and lots more print warnings, but just ignore them (or use -Wno-format)...

jcook@jcook-dellxps:~/cs581/spin$ ./pan
pan:1: assertion violated (val==9) (at depth 14)
pan: wrote inc.prom.trail

(Spin Version 6.5.2 -- 6 December 2019)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	acceptance   cycles 	- (not selected)
	invalid end states	+

State-vector 52 byte, depth reached 16, errors: 1
       24 states, stored
        0 states, matched
       24 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.002	equivalent memory usage for states (stored*(State-vector + overhead))
    0.292	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  128.730	total actual memory usage

The verifier says that our model is not always correct! This is seen in the first line that says the assertion was violated, and in the line that includes “errors: 1”.

Now we need to figure out how our model can produce the wrong value. To do this we use “spin -t”, or better yet “spin -t -p”. The “-t” option means “follow the trace”, and the trace is a path that the verifier created that leads to the found error, and the “-p” option says to print out each and every line of every process step in the trace. Here’s what that looks like:

jcook@jcook-dellxps:~/cs581/spin$ spin -t -p inc.prom
  1:	proc  0 (:init::1) inc.prom:14 (state 1)	[val = 4]
      val = 4
  2:	proc  0 (:init::1) inc.prom:15 (state 2)	[printf('val = %d\\n',val)]
Starting incrementBy with pid 1
  3:	proc  0 (:init::1) inc.prom:16 (state 3)	[(run incrementBy(2))]
          Increment val by 2!
  4:	proc  1 (incrementBy:1) inc.prom:8 (state 1)	[printf('Increment val by %d!\\n',amt)]
Starting incrementBy with pid 2
  5:	proc  0 (:init::1) inc.prom:17 (state 4)	[(run incrementBy(3))]
              Increment val by 3!
  6:	proc  2 (incrementBy:1) inc.prom:8 (state 1)	[printf('Increment val by %d!\\n',amt)]
  7:	proc  2 (incrementBy:1) inc.prom:9 (state 2)	[localv = (val+amt)]
  8:	proc  1 (incrementBy:1) inc.prom:9 (state 2)	[localv = (val+amt)]
  9:	proc  2 (incrementBy:1) inc.prom:10 (state 3)	[val = localv]
 10: proc 2 terminates
 11:	proc  1 (incrementBy:1) inc.prom:10 (state 3)	[val = localv]
 12: proc 1 terminates
 13:	proc  0 (:init::1) inc.prom:18 (state 5)	[(timeout)]
      val = 6
 14:	proc  0 (:init::1) inc.prom:19 (state 6)	[printf('val = %d\\n',val)]
spin: inc.prom:20, Error: assertion violated
spin: text of failed assertion: assert((val==9))
 15:	proc  0 (:init::1) inc.prom:20 (state 7)	[assert((val==9))]
spin: trail ends after 15 steps
#processes: 1
		val = 6
		sem = 1
 15:	proc  0 (:init::1) inc.prom:21 (state 8) <valid end state>
3 processes created

If you look carefully, steps 7-11 show that both processes copy the initial value of the shared value into their local variable, then increment it separately, and then write it back. This is the (concurrency) bug.

A Sequential Algorithm Example

Spin can be and is used to verify sequential algorithms, even though it is design to focus on concurrency. Below is a Promela model for finding the maxium value in an array. It uses inline macros for generating a “random” value, initializing the array, printing the array, finding the maximum value, and then checking the maximum value. The check includes an assert statement, and this is what is verified to be true, for all possible executions, when we run the verifier.

#define SIZE  5
#define VMAX  5
#define VMIN -5

int vals[SIZE];
int max;

inline genValue(i)
{
   int v=0;
   do
    :: (v < VMAX) -> v++;
    :: (v > VMIN) -> v--;
    :: true -> break;
   od
   vals[i] = v;
}

inline initArray()
{
   int i=0;
   do
    :: (i < SIZE) -> 
       genValue(i);
       i++;
    :: else -> break;
   od
}

inline printArray()
{
   int i=0;
   do
    :: (i < SIZE) -> 
       printf("vals[%d] = %d\n",i,vals[i]);
       i++;
    :: else -> break;
   od
}

inline findMax()
{
   int i=0;
   max = 0;
   do
    :: (i < SIZE) -> 
       if
        :: (vals[i] > max) -> max = vals[i];
        :: else -> skip;
       fi
       i++;
    :: else -> break;
   od
}

inline verifyMax()
{
   int i=0;
   do
    :: (i < SIZE) -> 
       assert(vals[i] <= max);
       i++;
    :: else -> break;
   od
}

init
{
   initArray();
   printArray();
   findMax();
   verifyMax();
   printf("max is %d\n",max);
}

Below are the commands and output for simulating and then verifying this model:

jcook@burro:~/ws/work/cs581/spin/max$ spin findmax.prom 
      vals[0] = 0
      vals[1] = -4
      vals[2] = 0
      vals[3] = -2
      vals[4] = 1
      max is 1
1 process created
jcook@burro:~/ws/work/cs581/spin/max$ spin -a findmax.prom 
jcook@burro:~/ws/work/cs581/spin/max$ gcc -Wno-format -o pan pan.c
jcook@burro:~/ws/work/cs581/spin/max$ ./pan
Depth=     107 States=    1e+06 Transitions= 1.02e+06 Memory=   204.608	t=     0.49 R=   2e+06
... multiple Depth lines elided...
Depth=     107 States=    9e+06 Transitions= 9.15e+06 Memory=   812.128	t=     4.81 R=   2e+06

(Spin Version 6.5.2 -- 6 December 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	acceptance   cycles 	- (not selected)
	invalid end states	+

State-vector 56 byte, depth reached 107, errors: 0
  9804061 states, stored
   161050 states, matched
  9965111 transitions (= stored+matched)
        0 atomic steps
hash conflicts:    199958 (resolved)

Stats on memory usage (in Megabytes):
  785.390	equivalent memory usage for states (stored*(State-vector + overhead))
  744.916	actual memory usage for states (compression: 94.85%)
         	state-vector as stored = 52 byte + 28 byte overhead
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  873.163	total actual memory usage


unreached in init
	(0 of 59 states)

pan: elapsed time 5.29 seconds
pan: rate 1853319.7 states/second

The line that includes “errors: 0” is the important line – it says that our model is correct! However, our check of the algorithm is incomplete – it only checks that max is as big or bigger than all values in the array, it does not check that max is actually a value in the array! We can add this to our check, which is now this:

inline verifyMax()
{
   int i=0;
   bool exists=false;
   do
    :: (i < SIZE) -> 
       assert(vals[i] <= max);
       if
        :: (vals[i] == max) -> exists = true;
        :: else -> skip;
       fi
       i++;
    :: else -> break;
   od
   assert exists;
}

Now when we verify our algorithm, it fails! The elided output is:

jcook@burro:~/ws/work/cs581/spin/max$ spin -a findmax.prom 
jcook@burro:~/ws/work/cs581/spin/max$ gcc -Wno-format -o pan pan.c
jcook@burro:~/ws/work/cs581/spin/max$ ./pan
...
State-vector 56 byte, depth reached 113, errors: 1
...

Our next step is to “follow the trail” in simulation to see how this can happen. The output (without the -p detail) is:

jcook@burro:~/ws/work/cs581/spin/max$ spin -t findmax.prom 
      vals[0] = -5
      vals[1] = -5
      vals[2] = -5
      vals[3] = -5
      vals[4] = -5
spin: findmax.prom:71, Error: assertion violated
spin: text of failed assertion: assert(exists)
spin: trail ends after 110 steps
#processes: 1
		vals[0] = -5
		vals[1] = -5
		vals[2] = -5
		vals[3] = -5
		vals[4] = -5
		max = 0
110:	proc  0 (:init::1) findmax.prom:80 (state 66)
1 process created

Clearly, we set max to be zero at the beginning, but the values in the array can all be negative. This is a bug, we should set max to be the smallest possible value, or even just set it to the first value in the array, so that it will always be a value that is in the array. With this change (setting it to the first value), when we do now have a correct model:

jcook@burro:~/ws/work/cs581/spin/max$ spin -a findmax.prom 
jcook@burro:~/ws/work/cs581/spin/max$ gcc -Wno-format -o pan pan.c
jcook@burro:~/ws/work/cs581/spin/max$ ./pan
...
State-vector 56 byte, depth reached 113, errors: 0
...

Controlling Verification Time

At its heart, spin verification is pretty simple: just search all possible execution paths and execution states of the model. Internally, it is highly engineered to represent states and perform the search as efficiently as possible, but it still needs to search all possible model states. So, if you have two 32-bit integers in your model that can take on any value that fits into 32 bits, spin must search all 2^64 different value combinations in order to verify your model. That’s like a million trillion values or so! We must avoid that much model search space!

The two “control knobs” that you need on most models are:

  1. A strict limit on the range of values you generate for the model data; and
  2. A limit on the size of the data for your model.

You can see these two control knobs in the model above in the “#define” statements for SIZE, VMAX, and VMIN. SIZE is for part two above, this limits the size of the array we will search over, and VMAX and VMIN capture the value limits that we are using. Even though the array is made up of ints, the “random” values we generate are limited to be in between VMIN and VMAX, and so our model search space is limited only to that small range of values.

The trick for both of these control knobs is that you want to keep them small enough so that your verification finishes in a reasonable amount of time and space (memory), but large enough that you believe they cover the necessary behavior that you are wanting to verify. For example, verifying a binary search over an array of just two elements probably is not going to exercise all of the possible conditions in your algorithm; an array of five elements might.

LTL: Linear Temporal Logic Properties

Assertions in your Promela model are good for verifying the state of the model at a particular point, but they don’t work for universal properties that need to hold over the whole timeline of the model’s behavior. These kinds of properties are most commonly needed for infinitely running systems, such as protocols (we can always keep sending and receiving messages) or concurrent processes (the threads in a web server can always respond to a new request).

For properties like this, Spin uses Linear Temporal Logic formulae, or LTL.

LTL formulae are logic formulae that are quantified over time rather than over sets, like “normal” set-theory existential and universal quantification is. Also, in LTL time is simply the logical ordering of events (or states), not anything related to real time.

The two basic LTL operators are called always and eventually. Think of these as temporal universal and existential quantification, respectively. The always operator is represented by a square (and is often called “box”), or in ASCII by two square brackets, []. The eventually operator is represented by a diamond, or in ASCII by two angle brackets, <>.

For example, the LTL formula “[](x<100)” is read as “always x is less than 100”. If Spin were to verify this formula for a model that had a global variable x, it would mean that at every step of execution of the model, the variable x never is 100 or greater. To use assertions to check that same property, you would have to put the assertion “assert (x<100)” in between every line of code! This is the power of LTL.

Although there are many uses for LTL formulae to represent system properties, the two most common are safety and liveness__ properties.

A safety property is a property that, if true for your system, means that your system is safe. The way to think about it is “something bad can never happen”. The “something bad” is some sort of logical formula that you do not want to ever be true in your system.

In LTL, the way to write a safety property is: "[](!(something bad))". We read this as “always not something bad”. For the example above with variable x, the “something bad” is if x reaches 100 or greater. So we would rewrite the formula as “[](!(x>=100))”. Obviously it means the same thing, since “always something good” is essentially the negation of “always not something bad”. We just usually think of safety properties as avoiding the bad, rather than specifying the good.

A liveness property captures the idea that the system will always be able to function – i.e., it stays alive, with respect to a particular property. Another way to phrase this is “something good can always happen”.

It is tempting to write a liveness property as “<>(something good)”. An easy read of this is “eventually something good”. However, this does not work. This would allow the good thing to happen once, but then never happen again. A liveness property must be specified as: "[]<>(something good)". We read this as “always eventually something good”. This means that no matter where the system currently is or how many times it has already done the good behavior, it can always still do it again in the future. In other words, it is always alive, always possible in the future; the system never “hangs”.

LTL Example: Railroad Lights

Below is a small Promela model that tries to capture lights on a railroad track, where only one direction should be green at a time:

/*
* Implementation of RailRoad red/green light
*/

#define green  1
#define red    0

#define East 0
#define West 1
byte light[2];

proctype RRLight(byte me; byte other; byte dir) 
{
   do
   :: (light[me] == green) -> 
      light[me] = red; 
      printf("%c turned red\n",dir);
   :: (light[me] == green) -> 
      printf("%c stayed green\n",dir);
   :: (light[me] == red) -> 
      printf("%c stayed red\n",dir);
   :: (light[me] == red && light[other] != green) -> 
      light[me] = green; 
      printf("%c turned green\n",dir);
   od;
}

init
{
   light[East] = red;
   light[West] = green;
   atomic {
      run RRLight(East,West,'E');
      run RRLight(West,East,'W');
   };
}

ltl safetyGreen {[]!(light[East]==green && light[West]==green)}
ltl liveGoGreen {[]<>(light[East]==green)}

When we simulate it, it shows the lights switching back and forth from red to green and vice versa. The last two lines show LTL properties that are written in the model file but are properties to check. The first is a safety properties that says both lights are never green at the same time, and the second is a liveness property that says the east-bound light can always return back to be green; since both lights use the same proctype, if we prove liveness for one, it will be true of the other.

Unfortunately, there is no attempt at synchronization in this model, and so both the safety and liveness properties will fail to be verified. Both lights can be green at the same time, and one light can starve and never turn green again at some point.

Other Resources

None for now.