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
51
|
// Mutual exclusion algorithm for n processes with a shared lock
// Process identifiers
typedef unsigned (1..2) pid_t;
// For n processes, the system has (n + 2) << (n - 1) states.
// pending processes
place pending (0..#pid_t) pid_t;
// processes in critical section
place critical (0..1) pid_t;
// quiescent processes (redundant place)
place quiet (0..#pid_t) pid_t: (pid_t p: p) minus
(place pending union place critical);
// flag: is the critical section available (redundant place)
place lock (0..1) bool (true): (place critical equals empty)#true;
trans Request
in {
place quiet: x;
}
out {
place pending: x;
};
trans GoCrit
in {
place pending: x;
place lock: true;
}
out {
place critical: x;
}
strongly_fair pid_t p: p == x;
trans Release
in {
place critical: x;
} out {
place quiet: x;
place lock: true;
};
// weak fairness for trans Request should not hold:
// []<>((>pid_t subset place quiet) => (>pid_t subset place pending))
// strong fairness for trans Request should not hold:
// ([]<>(>pid_t subset place quiet)) => ([]<>(>pid_t subset place pending))
// accessability property should hold:
// []((>pid_t subset place pending) => <>(>pid_t subset place critical))
|
