2 * Models the Pathfinder scheduling algorithm and explains the
3 * cause of the recurring reset problem during the mission on Mars
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
18 mtype = { free, busy, idle, waiting, running };
20 show mtype h_state = idle;
21 show mtype l_state = idle;
22 show mtype mutex = free;
24 active proctype high() /* can run at any time */
28 atomic { mutex == free -> mutex = busy };
31 /* critical section - consume data */
33 atomic { h_state = idle; mutex = free }
37 active proctype low() provided (h_state == idle) /* scheduling rule */
41 atomic { mutex == free -> mutex = busy};
44 /* critical section - produce data */
46 atomic { l_state = idle; mutex = free }