verif/Spin/Test/pathfinder

   1 /*
   2  * Models the Pathfinder scheduling algorithm and explains the
   3  * cause of the recurring reset problem during the mission on Mars
   4  *
   5  * there is a high priority process, that consumes
   6  * data produced by a low priority process.
   7  * data consumption and production happens under
   8  * the protection of a mutex lock
   9  * the mutex lock conflicts with the scheduling priorities
  10  * which can deadlock the system if high() starts up
  11  * while low() has the lock set
  12  * there are 12 reachable states in the full (non-reduced)
  13  * state space -- two of which are deadlock states
  14  * partial order reduction cannot be used here because of
  15  * the 'provided' clause that models the process priorities
  16  */
  17
  18 mtype = { free, busy, idle, waiting, running };
  19
  20 show mtype h_state = idle;
  21 show mtype l_state = idle;
  22 show mtype mutex = free;
  23
  24 active proctype high()  /* can run at any time */
  25 {
  26 end:    do
  27         :: h_state = waiting;
  28                 atomic { mutex == free -> mutex = busy };
  29                 h_state = running;
  30
  31                 /* critical section - consume data */
  32
  33                 atomic { h_state = idle; mutex = free }
  34         od
  35 }
  36
  37 active proctype low() provided (h_state == idle) /* scheduling rule */
  38 {
  39 end:    do
  40         :: l_state = waiting;
  41                 atomic { mutex == free -> mutex = busy};
  42                 l_state = running;
  43
  44                 /* critical section - produce data */
  45
  46                 atomic { l_state = idle; mutex = free }
  47         od
  48
  49 }
  50