Skip to content

Instantly share code, notes, and snippets.

@autonomousapps
Created September 29, 2019 19:48
Show Gist options
  • Save autonomousapps/a8ebcb368fef211899fa6bda097c14f7 to your computer and use it in GitHub Desktop.
Save autonomousapps/a8ebcb368fef211899fa6bda097c14f7 to your computer and use it in GitHub Desktop.
------------------------------- MODULE dekker -------------------------------
EXTENDS TLC, Integers
CONSTANT Threads
(*--algorithm dekker
variables
flag = [t \in Threads |-> FALSE],
next_thread \in Threads;
define
\* At most one thread is in the critical section at a time
AtMostOneCritical == \A t1, t2 \in Threads:
t1 /= t2 => ~(pc[t1] = "CS" /\ pc[t2] = "CS")
\* All threads eventually reach the critical section
Liveness == \A t \in Threads: <>(pc[t] = "CS")
end define;
fair process thread \in Threads
begin
P1: flag[self] := TRUE;
P2:
while \E t \in Threads \ {self}: flag[t] do
P2_1:
if next_thread /= self then
P2_1_1: flag[self] := FALSE;
P2_1_2: await next_thread = self;
P2_1_3: flag[self] := TRUE;
end if;
end while;
CS: skip; \* CS means "critical section"
P3: with t \in Threads \ {self} do
next_thread := t;
end with;
P4: goto P1;
end process;
end algorithm;*)
\* BEGIN TRANSLATION
VARIABLES flag, next_thread, pc
(* define statement *)
AtMostOneCritical == \A t1, t2 \in Threads:
t1 /= t2 => ~(pc[t1] = "CS" /\ pc[t2] = "CS")
Liveness == \A t \in Threads: <>(pc[t] = "CS")
vars == << flag, next_thread, pc >>
ProcSet == (Threads)
Init == (* Global variables *)
/\ flag = [t \in Threads |-> FALSE]
/\ next_thread \in Threads
/\ pc = [self \in ProcSet |-> "P1"]
P1(self) == /\ pc[self] = "P1"
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "P2"]
/\ UNCHANGED next_thread
P2(self) == /\ pc[self] = "P2"
/\ IF \E t \in Threads \ {self}: flag[t]
THEN /\ pc' = [pc EXCEPT ![self] = "P2_1"]
ELSE /\ pc' = [pc EXCEPT ![self] = "CS"]
/\ UNCHANGED << flag, next_thread >>
P2_1(self) == /\ pc[self] = "P2_1"
/\ IF next_thread /= self
THEN /\ pc' = [pc EXCEPT ![self] = "P2_1_1"]
ELSE /\ pc' = [pc EXCEPT ![self] = "P2"]
/\ UNCHANGED << flag, next_thread >>
P2_1_1(self) == /\ pc[self] = "P2_1_1"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "P2_1_2"]
/\ UNCHANGED next_thread
P2_1_2(self) == /\ pc[self] = "P2_1_2"
/\ next_thread = self
/\ pc' = [pc EXCEPT ![self] = "P2_1_3"]
/\ UNCHANGED << flag, next_thread >>
P2_1_3(self) == /\ pc[self] = "P2_1_3"
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "P2"]
/\ UNCHANGED next_thread
CS(self) == /\ pc[self] = "CS"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "P3"]
/\ UNCHANGED << flag, next_thread >>
P3(self) == /\ pc[self] = "P3"
/\ \E t \in Threads \ {self}:
next_thread' = t
/\ pc' = [pc EXCEPT ![self] = "P4"]
/\ flag' = flag
P4(self) == /\ pc[self] = "P4"
/\ pc' = [pc EXCEPT ![self] = "P1"]
/\ UNCHANGED << flag, next_thread >>
thread(self) == P1(self) \/ P2(self) \/ P2_1(self) \/ P2_1_1(self)
\/ P2_1_2(self) \/ P2_1_3(self) \/ CS(self) \/ P3(self)
\/ P4(self)
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == (\E self \in Threads: thread(self))
\/ Terminating
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in Threads : WF_vars(thread(self))
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================
\* Modification History
\* Last modified Sun Sep 29 12:39:24 PDT 2019 by tony
\* Created Sun Sep 29 12:18:45 PDT 2019 by tony
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment