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