1. SPIN Tutorial

1. Install Spin on your machine. Go through test-1 to 6 in README_tests.txt in the /Examples of your installation to test your installation and to get familiar with the basic workflow with Spin.

2. Consider the following "hello" program in Promela. It prints a number of "Hello" messages to the screen, and can non-deterministically decide to stop.

   byte x ;
   
   active proctype P1() {
     do /* repeat forever */
     :: x = x+1 ; printf("Hello (%u)!\n", x) ;
     :: break ;
     od ;
     assert x<3 ;
     printf("\nBye!\n") ;
   }
   

   1. Find out how you can "run" the program. See here for SPIN's options.

      [spoiler]

   Note that when you run a program, you only produce one execution. This does NOT verify all possible executions.

   2. The program contains an assertion. Now, verify whether the program will never violate the assertion. Use SPIN to generate a pan. Compile and run the pan. Analyze the report. If it indicates an error is found, use SPIN again to trace the resulting error trail. See here for compile options to produce pan, and pan's runtime options. Options needed to trace are part of SPIN's runtime options, see here.

      [spoiler]

3. Consider the Promela program below. The sender cycles over the value of x, every time sending it to the receiver. At the receiver we also model that it may receive a corrupted data item, afterwhich it becomes stuck.

   chan link = [2] of {byte} ;
   
   proctype sender(chan c) {
     byte x = 0 ;
     do /* repeat forever */
     :: printf("Sending %u\n", x) ; c!x ; x = (x+1)%4 ;
     od ;
   }
   
   proctype receiver(chan c) {
     byte r ;
     byte trash ;
     bool corrupt = false ;
     do /* repeat forever */
     :: c?r     -> corrupt = false ; printf("Receiving %u\n", r) ;
     :: c?trash -> corrupt = true  ; printf("CORRUPTED\n") ; (false) ;
     od ;
   }
   
   init {
     run sender(link) ;
     run receiver(link) ;
   }
   

   1. Run the model checker on this model. It will report an error, but the model does not even have any assertion nor LTL formula. What kind of error is that? Debug the error trail.

      [spoiler]

   2. Express the following property in LTL: "If x is 0 (at the sender), this value will eventually be received". You can proceed to verify the property. It is not a valid property; see if you can trace the error trail.

      You can write your ltl formula in your model-file. Check the topic ltl in Promela Language Reference.

      When you run pan to check an LTL formula, you need to turn on the -a option. If you need to impose process-level fairness, add -f option. Check the manual of pan's runtime options. If you have multiple ltl formulas, -N option allows to to select.

      You would need a way to refer to a local variable from your LTL formula. Check the topic remote reference (remoterefs) in Promela Language Reference.

   [spoiler]

   3. Indeed, the above future property is not valid, because the program can become stuck after corruption. But, if the data never got corrupted, will every value x sent be eventually received? Can you express that as an LTL formula and verify it?

   4. (Challenging) What if we want to express a more general property: "if x is the value sent by the sender, this value will eventually be received". Note that now you want to quantify over the values of x. Unfortunately, SPIN does not allow quantifications to be expressed in LTL formulas. Can you find a way to get around this?

Assignment

#define N 4
#define FREE  N
#define TRUE  1
#define FALSE 0
#define NEXT(i) (i+1)%N
byte fork[N] ;
bool eating[N] ;

proctype Philosopher(byte i) {
   do
   :: atomic {
        ((fork[i]==FREE) && (fork[NEXT(i)]==FREE)) ;
        fork[i] = i ;
        fork[NEXT(i)] = i
      }
      /* prove that here we do indeed have the forks: */
      assert (fork[i]==i) && (fork[NEXT(i)]==i) ;
      eating[i] = TRUE ;
      eating[i] = FALSE ;
      fork[i] = FREE ;
      fork[NEXT(i)] = FREE
   od
}

init {
   byte k = 0 ;
   /* initially, all forks are free */
   do
   :: k<N  -> fork[k] = FREE ; k++
   :: k==N -> break
   od
   k = 0 ;
   /* create the philosophers and run them: */
   atomic {
     do
     :: k<N  -> run Philosopher(k) ; k++
     :: k==N -> break
     od
   }
}

1. The solution claims to be deadlock free. Verify this. (Figure out first how do you want to express "deadlock free")
2. Unfortunately, the program is not starvation free. For example, the two neighbors of Philosopher(0) can alternatingly grab their forks, and thus preventing the guard of Phil(0) to be ever enabled. Weak nor strong fairness will not help in this case.
   However, for executions where Phil(1) and Phil(3) defer from eating, we can still verify that Phil(0) will eventually eat. Verify this.
3. The solution above is distributed (it does not use a central process that dictates the order/schedule of the philosophers) and non-deterministic (there is pre-set order of when the philosophers eat). These are good properties for the philosophers. However, the solution is not ideal because it assumes that Phil(i) can lock the two forks it needs atomically. Come up with a solution that does not need such an assumption, and moreover is deadlock free (well, if you are up to it, you can also try to come up with a solution that is also starvation free). Verify your solution.
   Your solution should remain distributed and non-deterministic.