0b55f123 |
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 | |