File: 1_Exercises.html

package info (click to toggle)
spin 6.4.5%2Bdfsg-3
links: PTS, VCS
area: main
in suites: stretch
size: 2,636 kB
ctags: 2,878
sloc: ansic: 40,035; yacc: 996; makefile: 37; sh: 5
file content (1049 lines) | stat: -rw-r--r-- 38,596 bytes
<html>
<head>
<title>SPIN VERIFICATION EXAMPLES AND EXERCISES</title>
<style type="text/css">
	body {
		font-family: Arial, Helvetica, sens-serif ;
	}
	.boxed {
		margin-left:   24px ;
		margin-right:  24px ;
		margin-top:    12px ;
		margin-bottom: 12px ;
		padding-top:   12px ;
		padding-left:  12px ;
		padding-right: 12px ;
		border: 1px solid blue ;
	}
</style>
</head>
<p>
<table width=100%><tr><td width=10%> </td><td>
<h1><tt>SPIN VERIFICATION EXAMPLES AND EXERCISES</tt></h1>
Included below are some verification exercises
that can help you get acquainted with the <i>Spin</i> model checker.
All examples used here are available as <i>Promela</i> files in
the </i>Examples</i> directory of the <i>Spin</i> distribution.

<h2><tt><font color=blue>0.</font> Installing Spin</tt></h2>
We will assume you are using the most recent version of Spin, which
at the time of writing is Version 6.4.0.
If Spin is not yet installed on your machine, do this
(assuming a linux-like machine):
<pre>
	$ cd
	$ wget http://spinroot.com/spin/Src/spin640.tar.gz
	$ tar -xzvf spin640.tar.gz
	$ cd Spin/Src6.4.0
	$ make
	$ cp spin /usr/local/bin	# on a Mac: cp spin /usr/bin
	$ cd ../Examples/Exercises
	$ spin -V	# make sure it's there
	Spin Version 6.4.0 -- 19 September 2014
</pre>

<h2><tt><font color=blue>1.</font> Evaluating Search Complexity</tt></h2>

This first set of exercises is meant to give an indication of
the nature of the state space explosion phenomenon,
and how <i>Spin</i> deals with it.
It consists of small problems that can be solved with <i>Spin</i>.
At each step, it is best to first try to determine what
should happen, write down your prediction, and only then
perform the experiment with Spin, and explain the result.
(Especially if it differs from what you thought would happen.)
Answer each of the questions marked <b><font color=blue>a)</font></b> ...
<b><font color=blue>k)</font></b>, spending as much as you need to
understand what really happens.
<p>
<b><font color=blue>a)</font></b> How many reachable states do you predict will the
following small <i>Promela</i> model generate?
<pre>
	init {	// file: ex_1a.pml
		byte i	// initialized to 0 by default
		do	// loop forever
		:: i++	// a C-ism for i = i + 1
		od
	}
</pre>
Try a simulation run of 514 steps:
<pre>
	$ spin -u514 -p -l ex_1a.pml	# print out local vars at every step
</pre>
Notice what happens with the value of byte variable <tt>i</tt>
on the 255-th increment (in step 511).
	<div class="boxed">
	Note:
	The first argument <tt>-u514</tt>, limits the similation to 514 steps.
	The second argument <tt>-p</tt> tells Spin to print some information
	about every step that it executes, and the third argument <tt>-l</tt>
	tells Spin to print also the value of all local variables whenever
	they change.
	<br>You can see all options that Spin supports by executing:
	<pre>	$ spin --</pre>
	i.e., using two dashes as the argument.<p>
	</div>
<br>
<b><font color=blue>b)</font></b>
Would the simulation terminate if you didn't limit the number of steps?
<br>
<b><font color=blue>c)</font></b>
The model allows for an infinite number of increments of variable i.
Is this still a finite state model?
<p>
	<div class="boxed">
	Note:
	Spin converts the program-like model into a state machine.
	You can see this in the simulation sequence, where every increment
	ends up taking two steps, instead of one. The second step is the
	jump back to the start of the loop. When we do verification, where
	performance is important, Spin optimizes the statemachines
	a bit more, and it gets rid of that second step again.
	You can see the optimized state machine that Spin generates by executing:
	<pre>	$ spin -search -dump ex_1a.pml</pre>
	</div>

<b><font color=blue>d)</font></b>
Estimate the number of reachable states for this model.
Is it finite?
Will a verification run terminate?
Try it as follows.
<pre>
	$ spin -search ex_1a.pml	# equivalently: spin -run ex_1a.pml
</pre>
Explain the output and the number of states that is reported.
	<div class="boxed">
	The <tt>-search</tt> argument is a shorthand in
	Spin version 6.4 for a series of steps to perform a formal
	verification, that you <i>can</i> also execute one by one
	(but would only do in exceptional cases):
	<pre>
	$ spin -a ex_1a.pml # generate a C verifier for the model in pan.c
	$ cc -o pan pan.c   # compile it
	$ ./pan             # execute it</pre>
	Spin's <tt>-search</tt> argument separates arguments processed
	by Spin in interpreting the model itself (these would go <i>before</i> the
	<tt>-search</tt> argument) and arguments that are used to compile and run the
	verifier (these would go <i>after</i> the <tt>-search</tt> argument).
	In our example we needed no additional arguments of either type.<p>
	</div>
<p>
<b><font color=blue>e)</font></b>
What would happen if you had declared the variable to be
of type <tt>short </tt> instead of <tt>byte </tt>? 
What if you use a <tt>bit </tt>? 
Try these with a verification run and explain the results.  
	<div class="boxed">
	Note: A <tt>bit</tt> or <tt>boolean</tt> variable can
	only store two different values. As you noted above, a
	byte variable can store 256 possible values, and is unsigned.
	The datatype <tt>short</tt> is defined the same way as it
	is in the C programming language: it is a signed quantity of
	16 bits. See the definition of the data ranges for all Promela
	types in the manual pages for Promela:
	<a href="http://spinroot.com/spin/Man/datatypes.html">here</a>.
	Note that the ranges can be machine dependent, as they are in C.<p>
	</div>
<p>
<b><font color=blue>f)</font></b>
Predict how many reachable states there
are for the following system, and write them down as a reachability tree.
<pre>
	#ifndef N
	 #define N	2
	#endif
	init {	// file: ex_1f.pml
		chan dummy = [N] of { byte } // a message channel of N slots
		do
		:: dummy!85    // send value  85 to the channel
		:: dummy!170   // send value 170 to the channel
		od
	}
</pre>
	<div class="boxed">
	Note: All Spin models are preprocessed with the standard
	C preprocessor. This means that we can use include files and
	macro definitions. In this case, the macro N is defined to
	have the value 2, unless you define a different value on
	the command line when you invoke Spin. For instance, you can
	define N to be 4 by executing:
	<pre>	$ spin -DN=4 -m -search ex_1f.pml</pre>
	</div>
You can check your prediction as follows.
We're only interested in the size of the state space,
not in problems that may be caused by blocking on a full channel,
so we use the  <tt>-m</tt>
option to define that the sender of a message never blocks.
(Messages sent to a full channel are then lost.)
<pre>
	$ spin -m -search ex_1f.pml	# use -m to ignore buffer overflow
</pre>
Explain the result.
	<div class="boxed">
	Note: If you were brave enough to omit the <tt>-m</tt> argument,
	you've noticed that there are far fewer states. Spin will in this
	case report all <i>invalid end-state</i> errors it finds. That term
	is a nice euphemism for <i>deadlock</i>: a state from which no
	further progress is possible, but where the process(es) in the
	model have not all terminated.<p>
	An invalid endstate does not always correspond to an actual
	deadlock. If it does not, we can label the state where a process
	is okay to stop with an <tt>end-state</tt> label. We can place
	one at the first <tt>do</tt> keyword in the model, for instance,
	and then you'd be free to omit the <tt>-m</tt> flag, since the
	verifier now knows that it is okay to block the init process at
	that point in the code. You should get the same number of
	reachable states as before:
	<pre>
	init {
		chan dummy = [N] of { byte } // a message channel of N slots
	end:	do
		:: dummy!85    // send value  85 to the channel
		:: dummy!170   // send value 170 to the channel
		od
	}</pre>
	</div>
<p>
<b><font color=blue>g)</font></b>
What happens if you set N to 3, 4, 5, etc. ?
Express the number of states as a function of N.
Use your formula to calculate how many states there
will be if you set N to 14 ?
Check your prediction as follows.
<pre>	$ spin -DN=14 -m -search ex_1f.pml</pre>
Set N to 20 and repeat the run.
<pre>	$ spin -DN=20 -m -search ex_1f.pml</pre>
<p>
Consider the following metrics on this verification run:
<pre>
	T: the elapsed time for the run that is reported at the end
	S: the number of states <i>stored</i>
	G: the number of <i>total</i> number of states stored <i>and matched</i>
	V: the State-vector size (the amount of memory needed to store one state)
</pre>
	<div class="boxed">
	Note:<br>
	T measures only the time needed
	to perform the verification. It excludes the time needed for
	the generation and compilation of the verification code itself.
	(At higher settings for compiler optimization, and for more
	complexi models, this can introduce a notable time delay as well.)
	<p>
	G counts not just new states visited in the search, but also states
	that were re-visited (<i>matched</i>), so it reflects more accurately
	how much work was done by the verifier.
	<p>
	S/T (or G/T) gives you a measure for the efficiency of the verification
	process, or the <i>rate</i> at which reachable states are processed.
	Generally this rate will depend on a number of factors, including
	the size S, and, of course, the speed of your machine.
	For Spin this rate is typically in the range 10<sup>5</sup> to
	10<sup>6</sup> states per second.
	We look at a few other factors that can influence performance below.
	<p>
	S*V gives you the amount of memory that would be needed to store
	the full state space without compression.
	The statespace is not the only place where memory is used
	during the search (e.g., the stack also consumes memory) but it
	is typically the largest factor.<p>
	</div>
<p>

<b><font color=blue>h)</font></b>
The efficiency of a reachability analysis also depends critically
on the state space storage algorithm that is used.
By default, Spin uses a standard hash-table with linked lists to store
states. To study the effect of the hash-table size on performance,
repeat the last verification run with a very small hash table,
for instance as follows:
<pre>
	$ spin -DN=20 -m -search -w12 ex_1f.pml
</pre>
	<div class="boxed">
	Note: runtime parameter <tt>-w12</tt> goes <i>after</i>
	the <tt>-search</tt> option, and the other parameters for parsing
	the model itself go <i>before</i> it.<p>
	</div>
Explain the results.
	<div class="boxed">
	Hint: compare the number of hash conflicts
	that is reported for each run.<br>
	Try different settings for the <tt>-w</tt> argument. Notice that the number
	of states stored does not change, but the number of hash-conflicts, and the
	runtime needed, does.<p>
	</div>
<p>

<b><font color=blue>i)</font></b>
How much memory would you need to do a verification run
for our last example with N=24 ?
	<div class="boxed">
	Note: both the number of reachable states and
	the number of bytes per state goes up with N.
	Estimate that you would need about 42 bytes per state for N=24.<p>
	</div>
Now assume that you only have 16 Megabyte of memory available
to store the statespace.
You likely have much more, but we're going for the dramatic effect here.
<br>
16 MB is 2<sup>24</sup> bytes, so we could store no more than
16,777,216 / 42 = 399,457, or about 399,000 reachable states in
this much memory.
Other parts of the verification consume some memory as well,
so this is an upper-bound only.
To find out the real number, try it as follows.
In this command we limit the search to 16 MB plus a 1 MB margin,
and we use a small hashtable size (<tt>-w15</tt>:
<pre>
	$ spin -DN=24 -m -search -DMEMLIM=17 -w15 ex_1f.pml
</pre>
	<div class="boxed">
	We use a small setting for the hash-table <tt>-w15</tt>,
	to avoid that the hash-table itself would dominate the
	memory requirements. The default size of the hash-table
	would exceed the memory limit we are imposing here.
	<br>
	All arguments that <i>follow</i> a <tt>-search</tt>
	argument are passed by Spin to either the compiler
	or the runtime verifier. In this case we used both types of
	pass-thru options. All arguments that <i>preceed</i> the <tt>-search</tt>
	argument are processed by Spin itself as before.<p>
	</div>
<br>
If the real statespace size is2<sup>(N+1)</sup>-1 states (33,554,431),
what fraction of that statespace did you cover in your verification run?
Is it more than 1%?

<p>
<b><font color=blue>j)</font></b>
Let's see if we can improve over that last result,
without increasing the amount of memory.
<br>
Perform a bitstate search with Spin, as follows.
<pre>
	$ spin -DN=24 -m -search -DMEMLIM=17 -bitstate ex_1f.pml
</pre>
The default argument for <tt>-w</tt> gives us precisely the right
size of the hash-array of 16 MB here. (The default is <tt>-w27</tt>).
Compare the number of states stored with that of the earlier run.
It should have increased to about 64% of the actual number that
you calculated before: a significant increase.
	<div class="boxed">
	Note: a few things are worth pointing out here. First, the
	coverage of the bitstate run is significantly greater than
	that of the exhaustive run, but both used precisely the same
	amount of memory. This improves the accuracy of a verification,
	and improves our chances of finding errors, but it will generally
	deny us the certainty of a proof if <i>no</i> errors are found.
	<br>
	We can improve our chances of finding errors even more if we
	repeat the run with different hash-functions. By changing
	hash-functions we can achieve that hash-conflicts (which now
	remain unresolved and lead to truncation of the search) appear
	in different places, meaning that a different sampling of the
	state space will result. Spin has 100 different hash-functions
	builtin. You can change the default of <tt>-h1</tt> to for
	instance <tt>-h71</tt> to get a different sampling of the statespace.
	<br>
	One other things you can vary, to influence the sampling, is
	the number of bits that is set per state (i.e., the number of
	independent hash-functions that is used per state).
	You do so by specifying a <tt>-k</tt> argument. The default is
	<tt>-k3</tt>, which sets three bit-positions per state by using
	three independent hash-functions, but you can specify any other
	value greater than zero.<p>
	</div>

<p>
<b><font color=blue>k)</font></b>
The default setting for the <tt>-w</tt> argument in a bitstate search
is <tt>-w27</tt>. This defines a bitstate hash-array size of 2<sup>27</sup>
bits, which at 8 bits per byte equals 2<sup>24</sup> bytes, or 16 MB.
In a bitstate search the <tt>-w</tt> argument does determine the
maximum number of states that can be recorded in the bitstate hash-array.
<br>
Repeat the run without the memory bound, and enable
some compiler optimization while you're at it, as follows:
<pre>
	$ spin -DN=24 -m -search -O2 -bitstate -w29 ex_1f.pml
</pre>
and perform some additional runs with different sizes of the
bitstate array (different from the default of <tt>-w27</tt>).
Notice how the coverage achieved is changing for smaller and
larger hash-array sizes.
	<div class="boxed">
	You should be able to get pretty close to exhaustive coverage of the
	statespace with a <tt>-w30</tt> or <tt>-w31</tt> argument, using
	no more than about 128 MB or 256 MB (a small fraction of what an
	exhaustive search would consume).
	Note also if the rate at which states are explored is changing much.
	<br>
	For added credit, check also how the performance changes if you
	compile with or without different levels of compiler optimization,
	e.g., <tt>-O</tt>, <tt>-O2</tt>, or <tt>-O3</tt>.<p>
	</div>

<h2><tt><font color=blue>2.</font> Verifying a Protocol</tt></h2>
<p>
The figure below shows a protocol specification given
by <a href="#R2">Bartlett et al.</a>
This figure appears as Figure 3c
in the paper referenced, which introduced
what became known as the <i>alternating-bit protocol</i>.
It was originally designed to make it possible to transmit
information reliably over noisy telephone lines with low-speed
(e.g., 300 baud) modems.
<p>
<center>
<img src="1_fig1.gif">
</center>
<p>

A <i>Promela</i> version of this protocol is shown below.
<p>
State S1 is the initial state in process A and
state S2 is the initial state in process B.
<pre>
  1 mtype = { a0, a1, b0, b1, err } // file ex_2.pml
  2 
  3 chan a2b = [0] of { mtype }	// a rendezvous channel for messages from A to B
  4 chan b2a = [0] of { mtype }	// a second channel for the reverse direction
  5 
  6 active proctype A()
  7 {
  8 S1:	a2b!a1
  9 S2:	if
 10 	:: b2a?b1  -> goto S1
 11 	:: b2a?b0  -> goto S3
 12 	:: b2a?err -> goto S5
 13 	fi
 14 S3:	a2b!a1  -> goto S2
 15 S4:	b2a?err -> goto S5
 16 S5:	a2b!a0  -> goto S4
 17 }
 18 
 19 active proctype B()
 20 {
 21 	goto S2
 22 S1:	b2a!b1
 23 S2:	if
 24 	:: a2b?a0  -> goto S3
 25 	:: a2b?a1  -> goto S1
 26 	:: a2b?err -> goto S5
 27 	fi
 28 S3:	b2a!b0 -> goto S2
 29 S4:	a2b?_  -> goto S1
 30 S5:	a2b!b0 -> goto S4
 31 }
</pre>
<b><font color=blue>a)</font></b>
Use a spin verification to see if there are any unreachable states.
Explain the result.
<p>
<b><font color=blue>b)</font></b>
How would you modify the model to make all states reachable?
	<div class="boxed">
	Consider modeling unreliable channel behavior, by including
	message loss and/or message corruption as possible behaviors.
	You can do so by introducing an additional channel process, that
	shuttles messages from sender to receiver, or you can do so
	by adding an option at the sender to either send message
	correctly, or as an <tt>err</tt> message, to simulate corruption.
	<br>Like this:
	<pre>
	S1:	if
		:: b2a!b1	// correct transmission
		:: b2a!err	// model message corruption
		fi</pre>
	</div>
<b><font color=blue>c)</font></b>
How could you extend the model to be able to prove the following property:
	<ul>
	<i>"Every message fetched by A is received error-free
	at least once and accepted at most once by B."</i>
	</ul>
This problem is a little <i>harder</i>.
Skip it if you're not already familiar with writing Promela specifications.

	<div class="boxed">
	Hint: you can add fields to the messages with data values.
	To do so you have to change the channel declarations.
	For instance, as follows:
	<pre>
	chan a2b = [0] of { mtype, byte }
	chan b2a = [0] of { mtype, byte }</pre>
	where the send and receive operations now have two field of
	matching types. For instance:
	<pre>	a2b!a1(78)</pre>
	You can find more hints about proving this type of property in
	the last problem in this set, below.<p>
	</div>


<h2><tt><font color=blue>3.</font> Verifying a Mutual Exclusion Algorithm</tt></h2>
<p>
If two or more concurrent processes execute the
same code and access the same data, there is
a potential problem that they may overwrite
each others results and corrupt the data.
The <i>mutual exclusion problem</i> is the problem of
restricting access to a critical section in the
code to a single process at a time, assuming <i>only</i>
the indivisibility of read and write instructions.
The problem was first described by <a href="#R4">Edsger Dijkstra</a>.
	<div class="boxed">
	In practical applications, the mutual exclusion problem
	is normally solved by using locks or semaphores.
	(The concept of a <i>semaphore</i> was also first proposed
	by Dijkstra.) Locks and semaphores in turn are typically
	implemented with special indivisible machine instructions
	for <i>test and set</i> or <i>compare and swap</i> operations.
	<br>
	It is especially important to note that
	mutual exclusion algorithms that do not use any special
	machine instructions no longer work correctly on modern CPU
	architectures with out-of-order execution. On these machines
	(i.e., the machine your using now, no matter which brand it is)
	the problem can not be solved under the constraints that
	Dijkstra defined in 1965. Nonetheless, for mysterious reasons,
	mutual exclusion algorithms still remain popular as
	examples of the application of logic model checking.<p>
	</div>
<p>
<b><font color=blue>a)</font></b>
Dijkstra published a first solution to the problem (that worked on
the CPUs from that time) in his 1965 paper.
A year later a different author published an
"improved" solution" in the same journal
(<i>Comm. of the ACM</i>, Vol. 9, No. 1, p. 45).
It is reproduced here as it was published (in pseudo Algol).
<pre>
  1 Boolean array b(0;1) integer k, i, j,
  2 comment process i, with i either 0 or 1 and j = 1-i;
  3 C0:	b(i) := false;
  4 C1:	if k != i then begin
  5 C2:	if not (b(j) then go to C2;
  6 	else k := i; go to C1 end;
  7 	else critical section;
  8 	b(i) := true;
  9 	remainder of program;
 10 	go to C0;
 11 	end
</pre>
Model this algorithm as a Spin model, and prove or disprove the
correctness of the algorithm.
You do not need to, and should not, consider out of order executions.
	<div class="boxed">
	If you get stuck, take a look at a sample solution in file
	ex_3a.pml -- and analyze it as follows:
	<pre>	$ spin -search ex_3a.pml
	$ spin -p -replay ex_3a.pml</pre>
	In this sample solution an LTL property is used to verify
	the algorithm. You can also verify this simple safety
	property with a plain assertion. For hints on how to do
	that, see the suggestion box at problem 3b below.
	For more suggestions for replaying counter-examples,
	or finding shorter alternative sequences, look for
	the suggestion box under problem 3c below.<p>
	</div>
<p>
<b><font color=blue>b)</font></b>
The mutual exclusion problem was popular as an intellectual challenge
for a very long time.
For an overview solution attempts up to
roughly 1984, see <a href="#R5">Raynal</a> or <a href="#R6">Lamport</a>.
An elegant solution was published by <a href="#R7">Peterson</a>.
In <i>Promela</i> the solution can be modeled as follows.
The predefined Promela variable <tt>_pid</tt> contains the id of
the running process: which in this case is either 0 or 1.
<pre>
  1 bool flag[2]	// file: ex_3b.pml
  2 bool turn
  3 
  4 active [2] proctype user()
  5 {
  6 	flag[_pid] = true
  7 	turn = _pid
  8 	(flag[1-_pid] == false || turn == 1-_pid)
  9 
 10 crit: skip	// critical section
 11 
 12 	flag[_pid] = false
 13 }
</pre>
Verify Peterson's algorithm with Spin.

	<div class="boxed">
	A simple way to do the check is to count the number
	of processes that can reach the label <tt>crit</tt>.
	You can add a global variable <tt>cnt</tt>, and increment
	it before reaching the label, and decrement it afterwards.
	Now it is easy to perform the critical check, simply
	with an assertion. For instance:
	<pre>
	 9       cnt++
	10 crit: assert(cnt == 1)
	11       cnt--
	</pre>
	Additional questions: what data type should <tt>cnt</tt>
	have? Could it be a <tt>bit</tt>? Could it be an <tt>int</tt>?
	Should it?
	Could the variable <tt>cnt</tt> be declared locally instead
	of globally? Explain your answer.<p>
	</div>

<p>
<b><font color=blue>c)</font></b>
Far too many publications contained what later turned out to be
faulty solutions to the mutual exclusion problem. In the sixties
and seventies there were no model checkers to quickly find out
whether or not a solution was sound.
As an example, the next version of the algorithm was recommended
by a computer manufacturer to a customer in the late eighties.
<pre>
  1 byte cnt                                    // file ex_3c.pml
  2 byte x, y, z
  3 
  4 active [2] proctype user()
  5 {	byte me = _pid+1			// 1 or 2
  6 
  7 L1:	x = me
  8 	if
  9 	:: (y != 0 && y != me) -> goto L1	// try again
 10 	:: (y == 0 || y == me)
 11 	fi
 12 	z = me
 13 	if
 14 	:: (x != me)  -> goto L1		// try again
 15 	:: (x == me)
 16 	fi
 17 	y = me
 18 	if
 19 	:: (z != me) -> goto L1			// try again
 20 	:: (z == me)
 21 	fi					// success
 22 	cnt++
 23 	assert(cnt == 1)			// critical section
 24 	cnt--
 25 	goto L1					// Dijkstra wouldn't like this either
 26 }
</pre>
First try to find a scenario that leads to the assertion
violation by studying the algorithm.
Next generate the counter-example with <i>Spin</i>.
	<div class="boxed">
	Assuming that you easily generated a counter-example
	(<tt>spin -search ex_3c.pml</tt> will do it), the next question
	you'll have is how to inspect it. You'll need the Spin flag <tt>-replay</tt>
	for this. The <tt>-replay</tt> argument tells spin to look for a
	counter-example trail that is store in a file with the same
	name as the Promela model, but with file extension <tt>.trail</tt>.
	You can try, for instance:
	<pre>	$ spin -replay ex_3c.pml</pre>
	which will show you a final value for the
	global variable <tt>cnt</tt> of 2, but it doesn't show the steps
	leading to the assertion violation. To do so you will have to
	add some more options, telling Spin what to print at each step.
	For instance:<pre>	$ spin -p -replay ex_3c.pml</pre> is far more
	informative.
	<br>
	You'll also notice that the trail is longer than it would need
	to be. To get a shorter trail, you can try running the verification
	with an iterative shortening option <tt>-i</tt>. For instance
	<pre>
	$ spin -search -i ex_3c.pml		# add runtime parameter -i
	$ spin -p -replay ex_3c.pml</pre>	# -p goes before -replay
	This is still not the shortest possible trail. To get that,
	you can recompile Spin to force it to search for the shortest
	possible counter-example. For instance by using a breadth-first,
	instead of the default depth-first search, as follows:
	<pre>
	$ spin -search -bfs ex_3c.pml		# use breadth-first search
	$ spin -p -replay ex_3c.pml</pre>
	You can also get the shortest counter-example with the default
	depth-first search, but now you have to tell the verifier to
	remember the length of execution sequences (which uses more
	memory) and use the iterative shortening method:
	<pre>
	$ spin -search -i ex_3c.pml	# modified depth-first with shortening
	$ spin -p -replay ex_3c.pml</pre>
	</div>

<h2><tt><font color=blue>4.</font> Verifying Petri Nets</tt></h2>
<p>
It is often easier to build a small Spin model and
ask the model checker to verify it than it is to write
or to check a thorough manual proof of correctness.
Petri Nets are relatively easy to model as <i>Promela</i> verification models.
For this exercise, consider the Petri Net model shown below, which
first appeared as Figure 1 in <a href="#R8">Berthelot et al</a>.
<p>
<center>
<img src="1_fig2.gif">
</center>
<p>

A Spin model for this Petri net can be written as follows.
<pre>
  1 #define Place	byte	// assume at most 255 tokens per place
  2                             // file ex_4.pml
  3 Place p1=1, p2, p3          // place p1 has an initial token
  4 Place p4=1, p5, p6          // place p4 has an initial token
  5 
  6 #define inp1(x)	x>0 -> x--
  7 #define inp2(x,y)	x>0 && y>0 -> x--; y--
  8 #define out1(x)	x++
  9 #define out2(x,y)	x++; y++
 10 
 11 init
 12 {
 13   do
 14   :: inp1(p1)    -> out1(p2)	// t1
 15   :: inp2(p2,p4) -> out1(p3)	// t2
 16   :: inp1(p3)    -> out2(p1,p4)	// t3
 17   :: inp1(p4)    -> out1(p5)	// t4
 18   :: inp2(p1,p5) -> out1(p6)	// t5
 19   :: inp1(p6)    -> out2(p4,p1)	// t6
 20   od
 21 }
</pre>
<p>
The net was proven to be deadlock free in the paper referenced,
with a manual reduction and proof technique.
Verify the result with <i>Spin</i>.
Explain the result in detail.

<h2><tt><font color=blue>5.</font> Veryfying a Process Scheduling Algorithm</tt></h2>
<p>
The model below for implementing sleep and wakeup routines
in a distributed operating systems kernel is based on
<a href="#R10">Ruane's</a> description.
The model contains an error that can be detected as a
fair non-progress cycle (use runtime options </i>-l</i> and </i>-f</i>).
Check if the proposed fix by Ruane, indicated in the model, suffices
to remove the problem.
<pre>
  1 mtype = { Wakeme, Running }		// file ex_5.pml
  2 
  3 bit	lk,	sleep_q
  4 bit	r_lock,	r_want
  5 mtype	State =	Running
  6 
  7 active proctype client()
  8 {
  9 sleep:					// sleep routine
 10 	atomic { (lk == 0) -> lk = 1 }	// spinlock(&lk)
 11 	do				// while r->lock
 12 	:: (r_lock == 1) ->		// r->lock == 1
 13 		r_want = 1
 14 		State = Wakeme
 15 		lk = 0			// freelock(&lk)
 16 		(State == Running)	// wait for wakeup
 17 	:: else ->			// r->lock == 0
 18 		break
 19 	od;
 20 progress:
 21 	assert(r_lock == 0)		// should still be true
 22 	r_lock = 1			// consumed resource
 23 	lk = 0				// freelock(&lk)
 24 	goto sleep
 25 }
 26 
 27 active proctype server()		// interrupt routine
 28 {
 29 wakeup:					// wakeup routine
 30 	r_lock = 0			// r->lock = 0
 31 	(lk == 0)			// waitlock(&lk)
 32 	if
 33 	:: r_want ->			// someone is sleeping
 34 		atomic {		// spinlock on sleep queue
 35 			(sleep_q == 0) -> sleep_q = 1
 36 		}
 37 		r_want = 0
 38 #ifdef PROPOSED_FIX
 39 		(lk == 0)		// waitlock(&lk)
 40 #endif
 41 		if
 42 		:: (State == Wakeme) ->
 43 			State = Running
 44 		:: else ->
 45 		fi;
 46 		sleep_q = 0
 47 	:: else ->
 48 	fi
 49 	goto wakeup
 50 }
</pre>
	<div class="boxed">
	To verify this model we need a few more Spin features than
	we have discussed so far. First, to allow the model checker to
	find non-progress cycles (infinite executions that fail to include
	at least one state labeled with a progress tag), we need to pass
	an different run argument to Spin. Like this:
	<pre>	$ spin -search -l -f ex_5.pml</pre>
	Which, if an error is reported, can be followed with the replay command:
	<pre>
	$ spin -p -replay ex_5.pml</pre>

	The first command directs spin to perform the
	verification with a search for non-progress loops (<tt>-l</tt>),
	while restricting to <i>fair</i> loops (<tt>-f</tt>).
	<br>
	Without going into too much detail, the counter-example that we
	would find if we omit the <tt>-f</tt>
	option could be classified as "unrealistic",
	because it ignores normal process scheduling rules that allow
	processes that are not blocked to eventually execute. This is reasonable
	<i>finite progress</i> criterion for non-blocked processes.
	By default though, the model checker will report <i>all</i> possible
	counter-examples, and not just the <i>reasonable</i> ones:
	it takes a demonic approach to finding errors. (Plus, just like in
	real life, restricting to <i>reasonable</i> behavior is usually
	somewhat more complex than not doing so...)<p>
	</div>
<p>
<h2><tt><font color=blue>6.</font> Verifying A Go-Back-N Sliding Window Protocol</tt></h2>
<p>
This go-back-n sliding window protocol follows the description
from <a href="#R13">Tanenbaum</a> in 1989.
The model below includes some annotations, with printf statements,
to facilitate the interpretation of simulation trails.
<pre>
  1 #define MaxSeq	3	 // file: ex_6.pml
  2 #define inc(x)	x = (x+1)%(MaxSeq+1)
  3 
  4 mtype = { red, white, blue } // for Wolper's test
  5 
  6 bool sent_r, sent_b		 // initialized to false
  7 bool received_r, received_b	 // initialized to false
  8 
  9 chan q[2] = [MaxSeq] of { mtype, byte, byte }
 10 chan source = [0] of { mtype }
 11 
 12 active [2] proctype p5()
 13 {	byte NextFrame, AckExp, FrameExp, r, s, nbuf, i
 14 	byte  frames[MaxSeq+1]
 15 	chan  inp, out
 16 	mtype ball
 17 
 18 	inp = q[_pid]
 19 	out = q[1-_pid]
 20 
 21 	do
 22 	:: nbuf < MaxSeq ->
 23 		nbuf++
 24 		if
 25 		:: _pid%2 -> source?ball
 26 		:: else
 27 		fi
 28 		frames[NextFrame] = ball
 29 		out!ball, NextFrame, (FrameExp + MaxSeq) % (MaxSeq + 1)
 30 		printf("MSC: nbuf: %d\n", nbuf)
 31 		inc(NextFrame)
 32 	:: inp?ball,r,s ->
 33 		if
 34 		:: r == FrameExp ->
 35 			printf("MSC: accept %e %d\n", ball, r)
 36 			if
 37 			:: !(_pid%2) && ball == red -> received_r = true
 38 			:: !(_pid%2) && ball == blue -> received_b = true
 39 			:: else
 40 			fi
 41 			inc(FrameExp)
 42 		:: else ->
 43 			printf("MSC: reject\n")
 44 		fi
 45 	 	do
 46 		:: ((AckExp <= s) && (s <  NextFrame)) ||
 47 		   ((AckExp <= s) && (NextFrame <  AckExp)) ||
 48 		   ((s <  NextFrame) && (NextFrame <  AckExp)) ->
 49 			nbuf--
 50 			printf("MSC: nbuf: %d\n", nbuf)
 51 			inc(AckExp)
 52 		:: else ->
 53 			printf("MSC: %d %d %d\n", AckExp, s, NextFrame)
 54 			break
 55 		od
 56 	:: timeout ->
 57 		NextFrame = AckExp
 58 		printf("MSC: timeout\n")
 59 		i = 1
 60 		do
 61 		:: i <= nbuf ->
 62 			if
 63 			:: _pid%2 -> ball = frames[NextFrame]
 64 			:: else
 65 			fi	
 66 			out!ball, NextFrame, (FrameExp + MaxSeq) % (MaxSeq + 1)
 67 			inc(NextFrame)
 68 			i++
 69 		:: else ->
 70 			break
 71 		od
 72 	od
 73 }
 74 
 75 active proctype Source()
 76 {
 77 	do
 78 	:: source!white
 79 	:: source!red ->
 80 		sent_r = true
 81 		break
 82 	od
 83 	do
 84 	:: source!white
 85 	:: source!blue ->
 86 		sent_b = true
 87 		break
 88 	od
 89 end:	do
 90 	:: source!white
 91 	od
 92 }
 93 
 94 ltl p1 { (<> sent_r -> <> (received_r && !received_b)) }
</pre>
	<div class="boxed">
	Perform a simulation, to see approximately how the
	protocol executes, for instance as follows, limiting
	the number of steps to the first 200:
	<pre>	$ spin -u200 ex_6.pml</pre>
	Notice that in this case, because of the printf statements
	in the model, we don't really need to add the <tt>-p</tt>
	to the simulator.
	The two processes named <tt>p5</tt> are printing messages
	to indicate key steps in their execution.
	To verify the model for safety properties (assertion violations
	or reachable invalid end-states) we can say:
	<pre>	$ spin -search ex_6.pml</pre>
	The verifier will then warn us about a problem:
	<pre>	error: max search depth too small</pre>
	The error notice says that the default search depth was not sufficient
	to perform a full search. To fix that we have to use
	a larger depth limit than the default (10,000 steps).
	<br>
	There's also another change we may want to make at this step, e.g.,
	to temporarily ignore the LTL claim in a first check.
	We can do so by using the compilation directive <tt>-noclaim</tt>.
	This leads to the following command line:
	<pre>
	$ spin -search -O2 -noclaim -m100000 ex_6.pml</pre>
	This gives us a first impression of the complexity of the search,
	which is still quite manageable, but requires a fair amount of memory.<p>
	</div>

Next we want to verify that this protocol correctly transfers data,
without loss or reordering.
This type of verification can be simplified by making use
of <a href="#R14">Wolper's</a> data independence theorem.
To do so, the protocol must be able to transfer at least
three colored messages (balls).
In our version of the model we made sure that
only one process transmits the colored balls,
while the other checks that they are accepted in the proper sequence.
The return direction transmits only dummy balls of one single type
<tt>none</tt>, which the other side accepts without check.
<p>
The LTL property <tt>p1</tt> that we specified at the end of the file
can be used to prove that every execution sequence where a red message is
sent eventually contains a state where a red message
is received, and in that state no blue message could have been received yet.
This establishes that the blue message cannot overtake the red message,
and the red message cannot be lost.

	<div class="boxed">
	The LTL property will be verified by default, unless you
	disable it with the <b>-noclaim</b> parameter. There's also
	only one LTL property in this case -- if there was more than
	one you'd have to choose the one to use in the verification,
	for instance as: <tt>spin -O2 -search -ltl p1 -m100000 ex_6.pml</tt> .
	<pre>
	$ spin -search -O2 -m100000 ex_6.pml # leave the LTL property enabled</pre>
	Notice that the search completes faster than before,
	requiring a smaller statespace to be explored, because we limited
	the verification to the specific problem of finding a counter-example
	to the LTL property. For that, not all possible behaviors are relevant.
	(I.e., we are exploring the <i>intersection</i> of program behavior and
	property behavior only.)<p>
	</div>

<h2><tt>References</tt></h2>
<ul>
<li><a name="R2"> Bartlett, K.A.</a>, Scantlebury, R.A., and Wilkinson, P.T.
`A note on reliable full-duplex transmission over half-duplex lines,'
Comm. of the ACM, 1969, Vol. 12, No. 5, 260-265, Figure 3c.

<!--
<li><a name="R3">C.H. West</a>, 
`General technique for communications protocol validation,'
IBM J. Res. Develop., 1978, Vol. 22, No. 3, pp. 393-404.
-->

<li><a name="R4">E.W. Dijkstra</a>,
`Solution to a problem in concurrent programming control,'
<i>Comm. of the ACM</i>, 1965, Vol 8, No. 9, p. 569.

<li><a name="R5">M. Raynal</a>,
<i>Algorithms for Mutual Exclusion</i>,
MIT Press, Cambridge, Mass., 1986, 107 pgs.
(The 1986 edition is a translation from the original
French version published in 1984.)

<li><a name="R6">L. Lamport</a>,
`The mutual exclusion problem -- parts I and II,'
<i>Journal of the ACM</i>, Vol. 33, No. 2, April 1986, pp. 313-347.

<li><a name="R7">G.L. Peterson</a>,
`Myths about the mutual exclusion problem,'
<i>Inf. Proc. Letters</i>, 1981, Vol. 12, No. 3, pp. 115-116.

<li><a name="R8">G. Berthelot, and R. Terrat,</a>
`Petri Net Theory for the correctness of protocols,'
<i>IEEE Trans. on Comm.</i>, Vol COM-30, No. 12, Dec. 1982, pp. 2497-2505.

<!--
<li><a name="R9">R.M. Needham, A.J. Herbert</a>,
<i>The Cambridge Distributed Computing System</i>,
Addison-Wesley Publ., London, 1982, p. 154.
-->

<li><a name="R10">L.M. Ruane</a>,
`Process synchronization in the UTS kernel,'
<i>Computing Systems</i>, (Usenix, Summer 1990), Vol. 3, No. 3, pp. 387--421.

<li><a name="R11">D. Dolev, M. Klawe, and M. Rodeh,</a>
`An O(n log n) unidirectional distributed algorithm
for extrema finding in a circle,'
<i>Journal of Algorithms</i>, Vol 3. (1982), pp. 245-260.

<li><a name="R12">M. Raynal</a>,
<i>Distributed algorithms and protocols</i>,
John Wiley and Sons, New York, 1992.

<li><a name="R13">A. Tanenbaum</a>,
<i>Computer Networks</i>, 2nd Ed.,
Prentice Hall, Englewood Cliffs, NJ., 1989, p. 214, 232-233.

<li><a name="R14">P. Wolper</a>,
``Specifying interesting properties of programs in propositional temporal logic,''
<i>Proc. 13th ACM Symposium on Principles of Programming Languages</i>,
St. Petersburg Beach, Fla., January 1986, pp. 148-193.

</ul>
<p><p><p><hr>
<table cols=3>
<tr>
<td valign=top width=210>
<a href="http://spinroot.com/spin/Man/index_html">Spin Online References</a><br>
<a href="http://spinroot.com/spin/Man/promela.html">ProMeLa Manual Pages</a><br>
<a href="http://spinroot.com/spin/Man/grammar.html">ProMeLa Grammar Rules</a><br>
<a href="http://spinroot.com/spin/">Spin HomePage</a>
</td>
<td valign=top width=100 align=center></td>
<td valign=top width=400 align=right>
<font size="3"><b><tt>(Page Updated: 19 September 2014)</tt></font></b></td></tr>
</table>

</td><td width=15%> </td></tr></table>
</html>