Assistance for this programming lab
will be available in the G-databar, Building 308, rooms 15+16,
Thursday, September 18, 15.00-17.00.
Preparations
You should read about the SPIN verification tool in [Spin].
You may find further information about SPIN at
spinroot.com, in particular
the online reference for the modelling language
Promela.
Instructions
The lab is divided into three parts, A, B, and C.
In the first two, you are going to experiment with given algorithms.
In the third, you should construct and verify an algorithm yourselves.
A: Basic SPINning
SPIN is installed in the G-databar. You may also install it on your
own computer. Note, however, that SPIN is Unix-biased and may take some
effort to install under Windows.
Now download the small Promela program
spin1.pml and start the SPIN graphical user
interface xspin by
xspin spin1.pml
You may edit the model within the tool. Alternatively, you may edit
it with your favorite editor and then reopen it in xspin.
Study the model. Note the process Check that constantly may
choose to check the assertion and provoke an error if not satisfied.
Run an interactive simulation: In Run... choose Set
simulation parameters. In the parameter window, under Display Mode select
Time Sequence Panel and under Simulation Style choose
interactive. Now Start the simulation and perform some steps
by selecting among the enabled actions.
The windows should be closed when done - otherwise they just stay around.
[Note: the Message Sequence Chart (MSC) is not of much use when
channels are not used and may be deselected.]
Run a verification: In Run... choose Set
verification parameters. For now, you don't have to change
anything, just press Run.
After a few seconds a verification output windows appears and after a
few more seconds, the verification ouput is ready.
This is what it looks like on success!
Change the value of N to 15 and select Re(run)
Verification. Now the output says
error: max search depth too small
and a window appears suggesting you to increase the search
depth. To do this, in Run... choose Set
verification parameters and click on [Set Advanced Options]
to get a parameter panel. Now set Maxmum Search Depth
to 50000 and repeat the verification.
The verification demonstrates that the invariant is satisfied.
Normally this would not be the case if these processes were
implemented as threads. The reason is, that Promela defines each
assignment to be atomic, whereas in reality this is not the
case if it has more than one critical reference.
Download spin2.pml and open it from
xspin. In this program the
increments and decrements have been broken down to atomic actions
having only one critical reference each.
We are now looking for errors. Whenever this is the case, the
search depth should be set low, in order to get a
short error trace.
Set the search depth to 50 and run the verification. Now, we still get
the seach depth error meaning that we did not get to every reachable
state. However, this is not so interesting because we also get
pan: assertion violated
A window pops up, suggesting to run an error trace in the simulation
mode. Do so, single stepping through the trace.
Since nothing really critical happens for the first many steps, we
would like to get to the error faster. In the advanced verification
parameter setting select Find shortest trail (iterative) and
rerun the verification. Now the error is found after (effectively)
only 8 steps.
B: Verification of a given Mutual Exclusion Algorithm
The following deals with the mutual exclusion algorithm defined in the
Exercise Share.2 (known from Exercise Class 2 this week).
Download the Promela model
spin3.pml and study it. See how it models
the algorithm given in Share.2 including the non-atomicity of the
program statements c1 = !c2 , and c2 = !c1 .
Start xspin and open spin3.pml. Make sure the
search depth is small (say 100) and try to verify the system.
Activate Find shortest trail and run it the simulator.
Now, you should model the program statements c1 = !c2 , and c2 = !c1 as being atomic. This can be done
by enlosing them with the atomic construct or simply by writing
them as single Promela statements.
Verify that mutual exclusion still does not hold - something that
came as a surprise to some of you during the Exercise Class.
Now download the program spin4.pml
where the break condition in the entry protocol has been changed to
using the local flag.
Verify that this algoritm works correctly.
Try to verify the following liveness properties
(download the .ltl-files and load them with the LTL
Property manager):
Obligingness for process 1: [] ((at_entry_1 && [] !
at_entry_2 ) -> <> at_crit_1)
(found in spin4_obl1.ltl)
Fairness[]( at_entry_1 -> <> at_crit_1)
(found in spin4_fair1.ltl)
You should first verify the system with weak fairness turned
on. If the property does not hold, the simulation trace will end in a
cycle sequence which is assumed to be repeated forever. Try to
find this sequence and understand how it violates the liveness property.
Does it make any difference if weak fairness is turned off?
C: Construction and verification of a Mutual Exclusion Algorithm
In the following you should propose and verify a solution to the
mutual exclusion problem for N processes using a coordinator
process. See [Andrews Figure 3.12] for a similar solution to the
barrier problem.
Download the Promela model
spin5.pml and study its structure. For a
given number N, the procesess P[0], P[1], ..., P[N-1]
should establish a critical region by communicating with a
Coordinator process. A proposal for the entry-protocol has
been made using two arrays of boolean flags:
enter[i] where P[i] requests the critical region and
in[i] where the Coordinator grants access to
P[i].
Write a proposal for the exit protcol and the code for the
Coordinator.
Verify that mutual exclusion is satisfied for your solution. Try to
increase N and see how high you can get.
Determine whether your solution is fair (eg. towards process
P[0]). The labels of this process may be referred to as
P[0]@entry and P[0]@crit in the necessary
#defines within the LTL Property manager.
