02158  Concurrent Programming - Lab 2: Verification with SPIN <font color="#B70000">- with comments and solutions</font>
Technical University of Denmark DTU
02158 Concurrent Programming        Fall 2024
Lab 2: Verification with SPIN - with comments and solutions
Home Plan Material  

Comments and solutions proposals added in red

Purpose

To get aquainted with the SPIN model checker and its JSpin GUI.

 
The lab will guide you through most of the operations needed to use SPIN for basic verification.

Time and Place

Assistance for this programming lab will be available in Building 303A, area EAST, Thursday October 3, 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. You may also like to have a look at the jSpin User Manual.

For these lab instructions it is assumed that you use a combination of SPIN and jSpin as found on the G-bar servers (available through ThinLinc).

If you prefer to use your own computer (which you probably do), you must install SPIN and jSpin in due time before the lab. The installation may be quite challenging (especially on Windows and Mac).

See the course wiki for detailed instructions (and contribute if you can).

If you for some reason cannot make JSpin work, you will have to run SPIN/JSpin on the G-bar servers using the desctiption found here.

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 (without a sweat?)

  1. Download the small Promela program spin1.pml and start the graphical user interface by the command
    jspin

  2. Open the model. You may edit it within the tool using standard edit shortcuts.

  3. Study the model. Note the process Check that constantly may choose to check whether a property is satisfied and provoke an error if not. Thereby it effectivly checks a global invariant.

  4. Check the syntax of the model: Press the Check button (for syntax check). In the console pane at the button, you can see that SPIN is run on the Promela model in order to do the syntax check. Any syntax errors are reported in the panel to the right.

  5. Try to make at typo and check the syntax again.

     
    Caveat: The jSpin tool saves the current Promela model under the original name (without any backup!) whenever it makes any kind of check, simulation or verification. Therefore you either have to exernally save copies of versions (espicially correct ones) or undo your changes.

  6. The tool may generate a graphical representation of the model corresponding to a transition diagram for each process. In this context it is called an automaton. To see the automata of the current model click the button SpinSpider and in the pop-up windows select a format of png and select the Automata choice to the right. Now pressing the Run button in the pop-up, the automata will be displayed. Make sure that you understand these. (Archs labelled 1 are just empty transitions where 1 represents a true guard.)

     

    Caveat: The SpinSpider tool also offers to generate a diagram of the reachable state space (ie. the transition graph). Unfortunately, however, this part is quite buggy and is considered deprecated by the author himself. Thus, SpinSpider should be used for checking the validity of the automata corresponding to the Promela model only.

  7. Run an interactive simulation:

     
    Pressing the Interactive button starts an simulation where you may choose among enabled transitions (when more than one is possible) using a pop-up choice bar. The output of the simulation is presented in the right panel and shows:

    The process id, the process name, the line number, the action and the value of variables as before the chosen step.
     
    It is possible to specify which variables to track during the simulation using the Output menu. See the jSpin user manual for details.

     
    (Tip: If statements or variable names are cut off, you may increase their width under the Output menu.)

    The selection bar should be closed in order to end the simulation.

    It is also possible to run a random simulation by pressing Random. The simulation runs of a limited amount of steps. [The default number is 250, but can be changed with the -u option of spin.]

  8. Run a verification:

     
    Ensure that Safety mode is chosen and press the Verify button. In the bottom panel, the verification steps are seen:

    1. First spin is run to generate the pan.c program

    2. The pan.c program is compiled into an executable pan

    3. The pan program is run to do the verification proper.
    The output of the verification is shown in the right panel. The main result is emphasized with bullets. However, you should also study the other sections of the output.

     

     
    NOTE: Since the invariant is checked by a separate process, no assertions need be added.

  9. Change the value of N to 15 and press Verify again. Now the output starts with
    error: max search depth too small
    which means that the verification has not been exhaustive because the maximum path length (sequence of distinct states) has been reached.

     
    Caveat: Notice that the verification still says *** no errors ***, but this is with respect to the limited search performed. Always check the start of your output for any error indications as they may render the error count irrelevant.

    To make an exhaustive search, the maximum search depth must be increased. This is done in the Settings menu under Max depth. Try to increase it, until the verification completes.

    (Tip: increase by a factor of 10 in each attempt.)

  10. 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 jspin. In this program the increments and decrements have been broken down to atomic actions having only one critical reference each.

    Inspect the automatas for the refined processes (as above) and recognize the non-atomic operations.

  11. 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 (as described above) 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 important because we discover an error:

    pan:1: assertion violated

    You can also see, that an error trail has been stored. Try to run a simulation using the trail by pressing the Guided button.

    (Tip: Use the Maximize buttton to let the right panel take over the whole upper part letting you see the simulation line by line.)

  12. Since nothing really critical happens for the first many steps, we would like to get to the error faster. This can be accomplished in different ways, but for safety properties the easiest way is to use breadth-first search. This has to be done by passing an option to the compilation of the pan.c program:
    Under the Options menu, choose C Compiler and in the pop-up window add -DBFS to the existing options.

     
    Now, when you rerun the verification you should find that the error trail has a length of 9. Run the trail using guided simulation and see how the invariant is violated.

B: Verification of a given Mutual Exclusion Algorithm

The following deals with the mutual exclusion algorithm defined in the Exercise Share.2 [Aux p.3] (known from Exercise Class 2 last week).

  1. Download spin3.pml, open it in jSpin and study it. Understand how it models the algorithm given in Share.2 including the non-atomicity of the program statements  c1 = !c2 , and  c2 = !c1 . You may generate the automata to clearly see this.

     
    [In this model, the mutual exclusion is expressed by local assertions as an alternative to checking a global invariant in an extra process.]

  2. Make an interactive simulation where you alternate the steps between the two processes. As you may recall, this should lead you to an assertion violation.

  3. 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 rewriting them to single Promela statements.

     
    Ascertain the atomicity of the statements by checking the automata. If you used the atomic{...} solution, the individuel transtions are still there, but are red in order to indicate that they are executed without any interleavings.

    Make sure that breadth-first search is still activated (as described in A.12) and try to verify the system. This shows that mutual exclusion still does not hold - something that some of you might have discovered during the Exercise Class.

    Run the error trail in the simulator and recognize that the "other flag" may change between the step of setting your own flag and testing the other flag again.

  4. 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 algorithm implements mutual exclusion correctly.

  5. At the bottom of the program, the following liveness properties have been added as LTL-formulas:

    They have been commented out in order not to interfere with the the safety verification above.

     
    To select one of the internal formulas for verification, you may simply uncomment it. Alternatively, you may uncomment all of them and then enter the name of the desired formula, eg. obl1, in the LTL formula text field and click on the LTL name button.

     
    Now, set the verification mode to Acceptance and do the verification. If selecting by name, check that the proper formula is chosen by checking the name after the -N option given to spin.

    Caveat: The breadt-first search option must not be enabled when doing acceptance verification.

    If a liveness property does not hold, the simulation trace will end in a cycle sequence (from <<<<<START OF CYCLE>>>>>) which is understood to be repeated forever. Try to find this sequence and understand how it violates the liveness property.

    (Tip: To find the shortest cycle sequence, add the option -i (for iteration) to the Options for Pan. The warning that this options only works for safety properties may be ignored. Actually, the option may work also for liveness properties.)

    You should find, that with weak fairness turned on, obligingness and resolution are satisfied, but not fairness, since the other process may freely enter and leave the region inbetween tests.

  6. Does it make any difference for any of the properties if weak fairness is turned off? Explain this.

    Without weak fairness none of the properties hold.

    NOTE: In general, it does not make sense to turn off weak fairness for a critical region program, since it allows a process to stall in the region and thereby block it, while the other process eagerly tries to enter it. Also, without weak fairness, any process which does not block, may take over the full computation.

C: Construction and verification of a Mutual Exclusion Algorithm

[This problem will be part of Mandatory Assignment 2.]

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.

  1. Download and open 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 ok[i] where the Coordinator grants access to P[i].

  2. Write a proposal for the exit protocol and the code for the Coordinator.

  3. Verify that mutual exclusion is satisfied for your solution. (If not go back one step.)

  4. Try to increase N and see how high you can get. You will here see the effect of state explosion.

  5. 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 formulation of the LTL property. Add the LTL property as an internal formula at the bottom of the Promela program.

     
    (Note: The verification output may ask you to recompile with -DNFAIR=3. This option should be added to the Options for C Compiler.)

    Caveat: As decribed in the [Spin] note, the x in P[x]@entry is not the index of P[0], but the processs identifier of P[0], which happens to be 0 as well, as P is the first process type to be instantiated.

  6. If your solution is not fair, how can it be made so?

    You will have to provide a solution yourself as part of Mandatory 2

Alternative SPIN Environments

JSpin provides a simple and fairly familiar environment for running SPIN, but does not give direct access to all the features of the underlying SPIN verification program (only indirectly through command-line options). Especially the simulation facilities of jSpin are fairly basic. Therefore you may like to try out alternative approaches before using SPIN for the mandatory assignment.

Good luck!

Hans Henrik Løvengreen, Oct 3, 2024