SPIN MODEL EXTRACTION
EXAMPLES AND EXERCISES

For the following exercises, we assume that you have a recent version of the Spin model extraction tool Modex installed on your system, version 2.4 or later, and a recent version of Spin, version 6.3.1 or later. Plus, to do anything useful with model extraction or Spin verification you'll need to have a standard C compiler, such as gcc, installed on your system.

We also assume that you have the verify script installed on your system, to simplify the verification process a little more, especially for the simpler examples.

0. Single-Threaded Code

As a first example, consider the following small C program.
  1 #include <stdio.h>
  2 			// file 1_bounds.c
  3 #define N       5
  4 #define M       4
  5 
  6 int
  7 main(void)
  8 {       int i, q[M], *p[N][M];
  9 
 10         for (i = 0; i < N; i++)
 11                 p[i][3] = &q[i];
 12 }
There is a bug in this program, but it is not too easy to spot. Even though there is just a single thread of execution, and Spin and Modex primarily target the verification of multi-threaded code, we can run the model-extractor on this small program to see if we can find the bug. Execute this command:
	$ verify 1_bounds.c
The various steps in the model extraction and verification process are printed on the output, and the error sequence found is listed as a sequence of C statements, leading step by step to the error, which in this case is an array bound overflow. Modex by default inserts checks for all pointer dereference operations and for array bound indexing operations, which means that we can verify this example even though we did not specify any explicit assertions for it.

To remove all files created by Modex and Spin, execute:

	$ verify clean
A second small example is the following inscrutible program.
  1 void	// file 2_pointers.c
  2 main(void)
  3 {       int x=12, y=34, z, w;
  4         int *p,*q,*i,*j,*k;
  5         int *****a;
  6 
  7         p = &z;
  8         q = &x;
  9         x = 56;
 10         *p = *q;
 11         i = p;
 12         p = &y;
 13         ****a = i;
 14         j = ****a;
 15         i = q;
 16 }
We may suspect trouble with the pointer dereference operations, but we can make sure with a quick verification run. It proceeds the same as before:
	$ verify 2_pointers.c
and when you're satisfied that you understand the error, you cleanup with:
	$ verify clean
There is also a step by step way to perform the verification. Sticking with the second example for now, you can try:
	$ modex -run 2_pointers.c
which will extract the Spin model, compile, and run it, and then stop.
Even more basic would be to execute:
	$ modex 2_pointers.c	# generate the model
	$ spin -run -O2 model	# compile and execute
	$ ./pan -r		# replay counter-example
You would only rarely need to use anything other than the main verify script though.

The Spin model that Modex generates is simply called model. If you're brave, you can try to look at that file and see if you can figure out how it is setup. For the 2_pointers.c program it looks as follows. We have slightly reformatted it here to make it easier to see the various parts.
  1 // Generated by MODEX Version 2.4 - 17 February 2014
  2 // Thu May  8 14:32:49 PDT 2014 from 2_pointers.c
  3 
  4 c_state "long res_main" "Global"
  5 
  6 bool lck_main_ret;
  7 bool lck_main;
  8 
  9 chan ret_main = [1] of { pid };
 10 chan exc_cll_main = [0] of { pid };
 11 chan req_cll_main = [1] of { pid };
 12 
 13 c_state "int  ***** a" "Local main"
 14 c_state "int  * p" "Local main"
 15 c_state "int  * q" "Local main"
 16 c_state "int  * i" "Local main"
 17 c_state "int  * j" "Local main"
 18 c_state "int  * k" "Local main"
 19 
 20 active proctype main( )
 21 {	int x = 12;
 22 	int y = 34;
 23 	int z;
 24 	int w;
 25 	pid lck_id;
 26 
 27    	c_code { Pmain->p=&(Pmain->z); };
 28    	c_code { Pmain->q=&(Pmain->x); };
 29    	c_code { Pmain->x=56; };
 30    	c_code [Pmain->q && Pmain->p] {		// note the precondition in square brackets
 31 		(*Pmain->p)=(*Pmain->q);
 32 	};
 33    	c_code { Pmain->i=Pmain->p; };
 34    	c_code { Pmain->p=&(Pmain->y); };
 35    	c_code [Pmain->a && (*Pmain->a) &&
 36 		(*((*Pmain->a))) &&
 37 		(*((*((*Pmain->a)))))] {
 38 			(*((*((*((*Pmain->a)))))))=Pmain->i;
 39 	};
 40    	c_code [Pmain->a && (*Pmain->a) &&
 41 		(*((*Pmain->a))) &&
 42 		(*((*((*Pmain->a)))))] {
 43 			Pmain->j=(*((*((*((*Pmain->a)))))));
 44 	};
 45    	c_code { Pmain->i=Pmain->q; };
 46 Return:
 47 	skip;
 48 }
A few things are worth pointing out. First, all local variables from the function main are extracted and inserted into the verifier's state-vector with c_state declarations. You would normally never use that type of Promela statement yourself, but it is there to make it possible to introduce arbitrary C data objects into the model checker. Data objects with a type that can be represented in Promela are declared normally (e.g., the variables x, y, z, and w).

Next, each C statement is wrapped in a c_code fragment, which basically is a Promela statement that contains an arbitrary piece of C code. (It gives us a way to completely redefine the language.) Every c_code fragment can have a guard in square brackets, that acts as an assertion for the fragment that follows. We could, for instance, write a standard Spin statement assert(3<41) also as:

	c_code [ 3<41 ] { ; }
with the same effect. On line 30 you a guard statement that checks that the pointers p and q are not NULL, before they are dereferenced in the c_code fragment that follows.

You also see that all references to the local variables in function main are prefixed with Pmain->. This is because these variables, in the extracted model are now located in the state-vector. On replay, the verify script will filter most of these decorations out again, so that it is easier to interpret error trails.

Note that the text of an extracted model is normally not something you would ever want to look at (other than if you are trying to debug the model extraction process itself).

There is one other caution about Spin models that contain c_code fragments. Because c_code statements contain uninterpreted C code, the Spin simulator cannot execute them. (It does not have a parser for C builtin, only for Promela). So to replay an error trace of a model with embedded C code you must always use the compiled verification code. The main verify script will do this automatically. Yyou can also reproduce an error trail found earlier as follows:
	$ verify replay

1. Multiple POSIX Threads

Now let's look at a simple C program with two POSIX threads.
  1 #include <pthread.h>	// file 3_threads.c
  2 #include <assert.h>
  3 
  4 int shared = 0;
  5 int *ptr;
  6 
  7 void *
  8 thread1(void *arg)
  9 {       int tmp;
 10 
 11         ptr = &shared;
 12         tmp = shared;
 13         tmp++;
 14         shared = tmp;
 15         return 0;
 16 }
 17 
 18 void *
 19 thread2(void *arg)
 20 {       int tmp;
 21 
 22         if (ptr)
 23         {       tmp = shared;
 24                 tmp++;
 25                 shared = tmp;
 26         }
 27         return 0;
 28 }
 29 
 30 int
 31 main(void)
 32 {       pthread_t t[2];
 33 
 34         pthread_create(&t[0], 0, thread1, 0);
 35         pthread_create(&t[1], 0, thread2, 0);
 36 
 37         pthread_join(t[0], 0);
 38         pthread_join(t[1], 0);
 39 
 40         assert(shared == 2);
 41 
 42         return 0;
 43 }
Verification proceeds as before:
	$ verify 3_threads.c
and quickly shows us if the assertion on line 40 can be violated. (No surprises there.)

A similar C program, but now with a total of three threads, is as follows.

  1 #include <pthread.h>	// file: 4_mutex.c
  2 #include <assert.h>
  3 
  4 pthread_t x, y, z;
  5 int cnt;
  6 
  7 void
  8 lock(pthread_t Pid)
  9 {
 10 busywait:
 11         x = Pid;
 12         if (y != 0 && !pthread_equal(Pid, y))
 13                 goto busywait;
 14 
 15         z = Pid;
 16         if (!pthread_equal(x, Pid))
 17                 goto busywait;
 18 
 19         y = Pid;
 20         if (!pthread_equal(z, Pid))
 21                 goto busywait;
 22 }
 23 
 24 void
 25 unlock()
 26 {
 27         x = 0;
 28         y = 0;
 29         z = 0;
 30 }
 31 
 32 void *
 33 thread(void *arg)
 34 {
 35         lock(pthread_self());
 36         cnt++;
 37         assert(cnt == 1);
 38         cnt--;
 39         unlock();
 40 }
 41 
 42 int
 43 main(void)
 44 {       pthread_t t[2];
 45 
 46         pthread_create(&t[0], 0, thread, 0);
 47         pthread_create(&t[1], 0, thread, 0);
 48 
 49         pthread_join(t[0], 0);
 50         pthread_join(t[1], 0);
 51 
 52         return 0;
 53 }
We can try a verification as before, but this time we have to be careful because the program fails to conform with the relatively simple assumptions that Modex makes about a C program in this category. Note that on lines 46 and 47 two instantiations of the same function named thread are created. Modex will by default assume that no more than one instantiation will be created per function. To make sure things work correctly, we therefore have to tell Modex to support two instantiations of functions, instead of one. The verify script doesn't help us there, so we have to take over and execute the steps one by one, for instance as follows:
	$ modex -xe2 -run 4_mutex.c
	$ verify replay

2. Defining Abstractions

Consider the following C program, which is taken from the TACAS 2013 competition of software verification tools, in the concurrency category. We have restored the code to something closer to what a programmer would write and reformatted for readability. (The competition version of the file was called 04_incdec_cas_true.c.)
  1 #include <pthread.h>	// file: 5_incdec.c
  2 #include <limits.h>
  3 
  4 #define uint    unsigned int
  5 
  6 volatile uint value = 0;
  7 volatile uint inc_flag = 0;
  8 volatile uint dec_flag = 0;
  9 
 10 uint
 11 inc(void)
 12 {       uint inc_v, inc_vn, inc_casret;
 13 
 14         do {
 15                 inc_v = value;
 16                 if (inc_v == UINT_MAX)
 17                 {       return 0;       // fail, return min
 18                 }
 19                 inc_vn = inc_v + 1;
 20                 cas(&value, inc_v, inc_vn, &inc_casret, &inc_flag);
 21         } while (inc_casret==0);
 22 
 23         assert(dec_flag || value > inc_v);
 24 
 25         return inc_vn;
 26 }
 27 
 28 uint
 29 dec(void)
 30 {       uint dec_v, dec_vn, dec_casret;
 31 
 32         do {
 33                 dec_v = value;
 34                 if (dec_v == 0)
 35                 {       return UINT_MAX; // fail, return max
 36                 }
 37                 dec_vn = dec_v - 1;
 38                 cas(&value, dec_v, dec_vn, &dec_casret, &dec_flag);
 39         }
 40         while (dec_casret==0);
 41 
 42         assert(inc_flag || value < dec_v);
 43 
 44         return dec_vn;
 45 }
 46 
 47 void *
 48 thread(void *arg)
 49 {       int r;
 50 
 51         r = rand();
 52 
 53         if (r)
 54         {       inc();
 55         } else
 56         {       dec();
 57         }
 58 
 59         return 0;
 60 }
 61 
 62 int
 63 main(void)
 64 {       pthread_t t;
 65 
 66         while(1) {
 67                 pthread_create(&t, 0, thread, 0);
 68         }
 69         exit(0);
 70 }
There are a number of things to watch for in this example. First, the main function starts up an infinite number of threads on line 67, without waiting for any of them to complete with a pthread_join call. For the purposes of verification it will suffice to check the program with just two threads of execution (we are interested in the possibility of race conditions). We can do that with a simple entry in a Modex guidance file that we will introduce shortly.

Second, the thread routine, for whatever reason, contains a call to a random number generator on line 51. The result of that call is stored in a signed integer variable. Depending on the size of an integer (32 or 64 bits) this could mean a very large number of cases that would need to be covered in the verification. The code that follows, though, only distinguishes between zero and non-zero values. This means that this is a perfect example for the use of abstraction. In this case it is simple to define a logically sound and complete abstraction rule that maps the values returned by the random number generator to just two distinct values: zero and one. We can define that rule in the Modex guidance file.

The third issue we need to resolve is that the program makes use of a compare-and-swap machine instruction cas, which is guaranteed to be executed indivisibly, i.e., free from thread interleaving. For our verification we could rely on that same instruction, if available, but we can also explicitly define the semantics of the instruction as an atomicically executed C function. The place to do that is again in the Modex guidance file.

The Modex guidance file is by convention given the same name as the C file being verified, but with extension .prx instead of .c, so that Modex will use it automatically whenever we try to verify that code. In this case that guidance file can look as follows.

  1 %X -xe2	// file: 5_incdec.prx
  2 %C
  3 void
  4 cas(volatile uint *v,
  5     volatile uint  e,
  6     volatile uint  u,
  7     volatile uint *r,
  8     volatile uint *flag)
  9 {
 10         if (*v == e)
 11         {       *flag = 1, *v = u, *r = 1;
 12         } else
 13         {       *r = 0;
 14         }
 15 }
 16 %L
 17 r=rand()        if :: r = 0 :: r = 1 fi
The first line defines that we want to extract all functions as instrumented Spin processes, supporting a minimum of two simultaneous calls to each function. The main function is by default extracted as a standard process that cannot be called by other funtions, following standard C convention. Next, on lines 3 to 15, in a segment marked with Modex command %C is the definition of the semantics for the atomic compare-and-swap routine. Finally, on line 17, following the Modex %L (for Lookup table) command is the abstraction rule for the statement that invoked the random number generator. We can now perform the verification as before:
	$ verify 5_incdec.c

3. Using Conversions

Consider the following C program.
  1 #include <stdio.h>	// file: 6_suspend.c
  2 #include <thread.h>
  3 
  4 int count;
  5 mutex_t count_lock;
  6 
  7 void *
  8 counter(void *arg)
  9 {       int i;
 10 
 11         while (1) {
 12                 printf("."); fflush(stdout);
 13 
 14                 mutex_lock(&count_lock);
 15                 count++;
 16 
 17                 for (i=0;i<50000;i++);
 18 
 19                 mutex_unlock(&count_lock);
 20 
 21                 for (i=0;i<50000;i++);
 22         }
 23 
 24         return((void *)0);
 25 }
 26 
 27 main()
 28 {       char str[80];
 29         thread_t ctid;
 30 
 31         /* create the thread counter subroutine */
 32         thr_create(NULL, 0, counter, 0, THR_NEW_LWP|THR_DETACHED, &ctid);
 33 
 34         while(1) {
 35                 gets(str);
 36                 thr_suspend(ctid);
 37 
 38                 mutex_lock(&count_lock);
 39                 printf("\n\nCOUNT = %d\n\n", count);
 40                 mutex_unlock(&count_lock);
 41 
 42                 thr_continue(ctid);
 43         }
 44 
 45         return(0);
 46 }
There are quite a number of interesting features of this example that we have to address to be able to perform an efficient verification of this code. First, the code uses primitives for thread creation, suspension, and continuation, and for locking and unlocking, that are not part of the POSIX library. We still want to be able to handle them, and for that we will need to make use of the Modex conversion tables. Next, the code has statements that merely affect runtime and not the basic functionality (e.g., the deaul looks on lines 17 and 21). We can hide these from the model with additional conversion rules. Next, the code uses an outdated call to an io routine gets, and clearly we do not want the model checker to have to execute those calls (and we as a user having to provide the inputs). Again, we can suppress this with a simple rule in the conversion table.

We can define everything we need in a small file with the extension .prx as follows.

  1 %X -a main
  2 %X -n counter
  3 %L
  4 gets(str)                       hide
  5 thr_create(...                  hide
  6 printf(...                      hide
  7 (i<50000)                       false
  8 
  9 thr_suspend(ctid)               Suspended = 1
 10 thr_continue(ctid)              Suspended = 0
 11 
 12 mutex_lock(&(count_lock))       atomic { count_lock == 0 -> count_lock = 1 }
 13 mutex_unlock(&(count_lock))     count_lock = 0
 14 
 15 %P
 16    bool Suspended;
 17 
 18    #include "_modex_main.pml"
 19 
 20    active proctype counter() provided (!Suspended) {
 21         #include "_modex_counter.pml"
 22    }
 23 %G
 24 maxdepth: 100
 25 shortest: 1
 26 %%
If the file has the same basename as our C program, Modex will know to use it to guide the model extraction process directly.

The conversion rules we mentioned are given after the %L tag on line 3. First, on line 4 we tell Modex to hide the calls to gets, and on line 5 to do the same with calls to thr_create. We will create the counter thread in a different way that will allow us to suspend and continue it with a Spin provided clause. We get rid of the for delay-loops on like 7 by shortcutting the loop-condition. Lines 9 and 10 define the thread suspension condition, which is picked up in the proctype definition for the counter thread on line 20. The body of the counter process is extracted on line 2, and the main process is extracted on line 1.

The final segment of the .prx file (lines 24-25) show some additional features that are available to guide the verification process. Here we restrict the maximum search depth for the verifier to 100 steps and we ask the model checker to look for the shortest counter-example. To perform the verification process all we have to do is to give the familiar command:

	$ verify 6_suspend.c
and Modex will apply the rules defined in the 6_suspend.prx file. The counter-example shows a deadlock scenario, where the counter-process holds the mutual exclusion lock, but is suspended, and the main process tries to obtain that lock, but can't.

A full review of different ways to define model extraction .prx files is beyond the scope of this overview, but it can be found online here: Modex Manual.


Spin HomePage
Modex HomePage
(Page Updated: 10 May 2014)