Skip to content

Commit d4b60a1

Browse files
jthemphilljthemphill
authored
Add Dining Philosophers example (#28)
* Add Dining Philosophers example * Chandy-Misra starvation-free solution * Follow suggestions on #28
1 parent 8fc7bc6 commit d4b60a1

File tree

2 files changed

+241
-0
lines changed

2 files changed

+241
-0
lines changed

‎specifications/DiningPhilosophers/DiningPhilosophers.cfg

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
\* Add statements after this line.
2+
SPECIFICATION Spec
3+
CONSTANT
4+
NP = 5
5+
INVARIANT
6+
TypeOK
7+
ExclusiveAccess
8+
PROPERTY
9+
NobodyStarves

‎specifications/DiningPhilosophers/DiningPhilosophers.tla

+232
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,232 @@
1+
---- MODULE DiningPhilosophers ----
2+
3+
(*
4+
TLA+ / PlusCal implementation of the Dining Philosophers problem.
5+
Based on the exercise given in https://learntla.com/temporal-logic/operators/
6+
7+
This is an implementation of the Chandy-Misra solution.
8+
https://en.wikipedia.org/wiki/Dining_philosophers_problem#Chandy/Misra_solution
9+
10+
In Dijkstra's original formulation of the problem, philosophers may not speak
11+
to each other and cannot hand forks to each other.
12+
13+
In the Chandy-Misra formulation, philosophers may hand forks directly to each
14+
other.
15+
16+
I ran this with alygin's TLA+ extension for VSCode:
17+
https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus
18+
"> TLA+: Parse module" updates the translated TLA+ to match the PlusCal
19+
'algorithm' above.
20+
"> TLA+: Check model with TLC" checks the model's correctness.
21+
22+
You can also use TLA+ Toolbox. You may need to "create a model" and
23+
use the UI to add the invariants and properties at the bottom of this file.
24+
*)
25+
26+
EXTENDS Integers, TLC
27+
28+
CONSTANTS
29+
\* Number of philosophers
30+
NP
31+
32+
ASSUME
33+
/\ NP \in Nat \ {0}
34+
35+
(* --algorithm DiningPhilosophers
36+
37+
variables
38+
forks = [
39+
fork \in 1..NP |-> [
40+
\* We start with each fork held by the lowest-number philosopher
41+
\* adjacent to the fork.
42+
holder |-> IF fork = 2 THEN 1 ELSE fork,
43+
\* Each fork starts out "dirty". Eating causes a fork to become
44+
\* dirty, after which the philosopher must clean the fork and hand
45+
\* it to their neighbor.
46+
clean |-> FALSE
47+
]
48+
]
49+
50+
define
51+
LeftFork(p) == p
52+
RightFork(p) == IF p = NP THEN 1 ELSE p + 1
53+
54+
LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1
55+
RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1
56+
57+
IsHoldingBothForks(p) ==
58+
forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p
59+
BothForksAreClean(p) ==
60+
forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean
61+
62+
CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p)
63+
end define;
64+
65+
\* This spawns 'NP' parallel Philosopher processes.
66+
\*
67+
\* A process looks kind of like an object oriented class, but '\in 1..NP' means
68+
\* it's really just an integer between 1 and NP. Use 'self' to access that
69+
\* integer.
70+
\*
71+
\* If you remove the 'fair' in 'fair process', each process can stop at any
72+
\* time and will never run again. Dining philosophers don't randomly die while
73+
\* clenching forks in the original problem, so let's keep the processes fair.
74+
fair process Philosopher \in 1..NP
75+
\* This acts like a member variable and you can access it like one. But we're
76+
\* actually creating an array with one element per process, and the "member
77+
\* variable" we access is just the corresponding bucket in that array.
78+
variables hungry = TRUE;
79+
begin
80+
Loop:
81+
while TRUE do
82+
\* Check if we're holding dirty forks that other philosophers might
83+
\* want.
84+
if
85+
/\ forks[LeftFork(self)].holder = self
86+
/\ ~forks[LeftFork(self)].clean
87+
then
88+
forks[LeftFork(self)] := [
89+
holder |-> LeftPhilosopher(self),
90+
clean |-> TRUE
91+
];
92+
elsif
93+
/\ forks[RightFork(self)].holder = self
94+
/\ ~forks[RightFork(self)].clean
95+
then
96+
forks[RightFork(self)] := [
97+
holder |-> RightPhilosopher(self),
98+
clean |-> TRUE
99+
];
100+
end if;
101+
if hungry then
102+
if CanEat(self) then
103+
Eat:
104+
hungry := FALSE;
105+
forks[LeftFork(self)].clean := FALSE ||
106+
forks[RightFork(self)].clean := FALSE;
107+
end if;
108+
else
109+
Think:
110+
hungry := TRUE;
111+
end if;
112+
end while;
113+
end process;
114+
115+
end algorithm; *)
116+
\* BEGIN TRANSLATION (chksum(pcal) = "8d8268d4" /\ chksum(tla) = "16352822")
117+
VARIABLES forks, pc
118+
119+
(* define statement *)
120+
LeftFork(p) == p
121+
RightFork(p) == IF p = NP THEN 1 ELSE p + 1
122+
123+
LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1
124+
RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1
125+
126+
IsHoldingBothForks(p) ==
127+
forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p
128+
BothForksAreClean(p) ==
129+
forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean
130+
131+
CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p)
132+
133+
VARIABLE hungry
134+
135+
vars == << forks, pc, hungry >>
136+
137+
ProcSet == (1..NP)
138+
139+
Init == (* Global variables *)
140+
/\ forks = [
141+
fork \in 1..NP |-> [
142+
143+
144+
holder |-> IF fork = 2 THEN 1 ELSE fork,
145+
146+
147+
148+
clean |-> FALSE
149+
]
150+
]
151+
(* Process Philosopher *)
152+
/\ hungry = [self \in 1..NP |-> TRUE]
153+
/\ pc = [self \in ProcSet |-> "Loop"]
154+
155+
Loop(self) == /\ pc[self] = "Loop"
156+
/\ IF /\ forks[LeftFork(self)].holder = self
157+
/\ ~forks[LeftFork(self)].clean
158+
THEN /\ forks' = [forks EXCEPT ![LeftFork(self)] = [
159+
holder |-> LeftPhilosopher(self),
160+
clean |-> TRUE
161+
]]
162+
ELSE /\ IF /\ forks[RightFork(self)].holder = self
163+
/\ ~forks[RightFork(self)].clean
164+
THEN /\ forks' = [forks EXCEPT ![RightFork(self)] = [
165+
holder |-> RightPhilosopher(self),
166+
clean |-> TRUE
167+
]]
168+
ELSE /\ TRUE
169+
/\ forks' = forks
170+
/\ IF hungry[self]
171+
THEN /\ IF CanEat(self)
172+
THEN /\ pc' = [pc EXCEPT ![self] = "Eat"]
173+
ELSE /\ pc' = [pc EXCEPT ![self] = "Loop"]
174+
ELSE /\ pc' = [pc EXCEPT ![self] = "Think"]
175+
/\ UNCHANGED hungry
176+
177+
Think(self) == /\ pc[self] = "Think"
178+
/\ hungry' = [hungry EXCEPT ![self] = TRUE]
179+
/\ pc' = [pc EXCEPT ![self] = "Loop"]
180+
/\ forks' = forks
181+
182+
Eat(self) == /\ pc[self] = "Eat"
183+
/\ hungry' = [hungry EXCEPT ![self] = FALSE]
184+
/\ forks' = [forks EXCEPT ![LeftFork(self)].clean = FALSE,
185+
![RightFork(self)].clean = FALSE]
186+
/\ pc' = [pc EXCEPT ![self] = "Loop"]
187+
188+
Philosopher(self) == Loop(self) \/ Think(self) \/ Eat(self)
189+
190+
Next == (\E self \in 1..NP: Philosopher(self))
191+
192+
Spec == /\ Init /\ [][Next]_vars
193+
/\ \A self \in 1..NP : WF_vars(Philosopher(self))
194+
195+
\* END TRANSLATION
196+
197+
----
198+
(* Invariant helpers *)
199+
----
200+
201+
(* TRUE iff philosophers p and q share a fork between them. *)
202+
ShareFork(p, q) ==
203+
{LeftFork(p), RightFork(p)} \cap {LeftFork(q), RightFork(q)} /= {}
204+
205+
----
206+
(* Invariants *)
207+
----
208+
209+
(*
210+
TLA+ and PlusCal are dynamically-typed, but we can roll our own typechecking
211+
with an invariant.
212+
*)
213+
TypeOK ==
214+
/\ forks \in [1..NP -> [holder: 1..NP, clean: BOOLEAN]]
215+
/\ hungry \in [1..NP -> BOOLEAN]
216+
/\ pc \in [1..NP -> {"Loop", "Eat", "Think"}]
217+
218+
(* If two philosophers share a fork, they cannot eat at the same time. *)
219+
ExclusiveAccess ==
220+
\A p,q \in 1..NP:
221+
p /= q /\ ShareFork(p, q) => ~(pc[p] = "Eat" /\ pc[q] = "Eat")
222+
223+
----
224+
(* Properties *)
225+
----
226+
227+
(*
228+
Every philosopher will eventually get to eat again.
229+
*)
230+
NobodyStarves == \A p \in 1..NP: []<>(~hungry[p])
231+
232+
====

0 commit comments

Comments
 (0)