Skip to content

Instantly share code, notes, and snippets.

@mratsim

mratsim/event_notifier.tla

Last active December 16, 2019 23:47
Show Gist options
  • Save mratsim/06f2c96afb5ab500bff45d431f590919 to your computer and use it in GitHub Desktop.
Save mratsim/06f2c96afb5ab500bff45d431f590919 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
event_notifier.tla
------------------- MODULE event_notifiers -----------------------
(*
Formal specification of the event_notifiers datastructure.
It allows a single consumer to be put to sleep and being woken up
by multiple producers so that the consumer is able to consume the incoming messages (steal requests).
It combines a prepare phase "intendToSleep" with commit phase "wait".
In between the consumer sends a message to its parent that it is going to sleep.
The commit phase is aborted when any producers signal an incoming message.
There should be no deadlock, i.e. an incoming message being signaled but the consumer stays sleeping
as in the runtome the main thread may be the only one awake and wouldn't be able to awaken its children
in that case.
*)
EXTENDS Integers, TLC, Sequences, FiniteSets
CONSTANTS NumThreads, ConsumerTID
ASSUME NumThreads > 1
ASSUME ConsumerTID > 0
ASSUME ConsumerTID < NumThreads
MaxID == NumThreads-1
ParentTID == ConsumerTID \div 2
producers == (0..MaxID) \ {ConsumerTID, ParentTID}
(* PlusCal options (-termination) *)
(* --algorithm event_notifier
variables
consumerState = "Busy";
signaled = FALSE; \* Simulate a condition variable
msgToParent = "None"; \* Simulate a message to parent. I.e. an opportunity for thread interleaving
macro intendToSleep() begin
consumerState := "IntendToSleep"
end macro
\* Everything in a macro happens atomically
macro atomicCompareExchange(result, current, expected, newVal) begin
if current = expected then
current := newVal;
result := TRUE;
else
result := FALSE;
end if;
end macro;
\* Consumer wait until it is signaled to wakeup
procedure wait()
variables casSuccess = FALSE;
begin
W1: atomicCompareExchange(casSuccess, consumerState, "IntendToSleep", "Parked");
if casSuccess then
W2: while consumerState = "Parked" do
\* The while loop protects against spurious wakeups
W3: await signaled;
signaled := FALSE;
end while;
end if;
W4: assert consumerState \in {"Parked", "ShouldWakeup"};
W5: consumerState := "Busy";
W8: return;
end procedure;
\* Notify the potentially waiting consumer that it should wake up
procedure notify()
variables localConsumerState = "N/A"; \* local view of the consumer state
begin
N1: localConsumerState := consumerState;
N2: if localConsumerState \in {"Busy", "ShouldWakeup"} then
N3: return;
end if;
N4: consumerState := "ShouldWakeup";
N5: while TRUE do
N6: signaled := TRUE;
N7: if consumerState /= "Busy" then
N8: skip;
else
N9: return;
end if;
end while;
end procedure;
procedure mayRequestWork()
begin MaySteal:
either
\* Sometimes you have enough work
NoSteal: skip;
or
\* Sometimes you don't and you steal
Steal: call notify();
end either;
ReqRET: return;
end procedure
procedure mayShareWork()
\* A parent can also share work with a
\* a child that sent it "Waiting"
begin MayShare:
either
\* sometimes the parent doesn't have work
NoWork: skip;
or
\* Sometimes it has some
Share0: if msgToParent = "Waiting" then
Share1: call notify(); \* wakeup the child
Share2: msgToParent := "None"; \* dequeue the child steal request
end if;
end either;
ShareRET: return;
end procedure;
\* Not fair because they might never steal
process producer \in producers
begin Coworkers:
call mayRequestWork();
end process;
\* a parent will always run at least the termination
fair process parent = ParentTID
\* The order of work sharing and work stealing is arbitrary
begin ParentWork:
either
PMayRW0: call mayRequestWork();
PMaySW0: call mayShareWork();
or
PMaySW1: call mayShareWork();
PMayRW1: call mayRequestWork();
end either;
\* But it will for sure tell the consumer to terminate at one point
Terminate: call notify();
end process;
process consumer = ConsumerTID
begin ConsumerWork:
either
\* if we have work we work on it
FoundWork: skip;
or
\* we signal our intent to sleep, tell our parent and then sleep
Sleeping0: intendToSleep();
Sleeping1: msgToParent := "Waiting";
Sleeping2: call wait();
end either;
end process;
end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES consumerState, signaled, msgToParent, pc, stack, casSuccess,
localConsumerState
vars == << consumerState, signaled, msgToParent, pc, stack, casSuccess,
localConsumerState >>
ProcSet == (producers) \cup {ParentTID} \cup {ConsumerTID}
Init == (* Global variables *)
/\ consumerState = "Busy"
/\ signaled = FALSE
/\ msgToParent = "None"
(* Procedure wait *)
/\ casSuccess = [ self \in ProcSet |-> FALSE]
(* Procedure notify *)
/\ localConsumerState = [ self \in ProcSet |-> "N/A"]
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self \in producers -> "Coworkers"
[] self = ParentTID -> "ParentWork"
[] self = ConsumerTID -> "ConsumerWork"]
W1(self) == /\ pc[self] = "W1"
/\ IF consumerState = "IntendToSleep"
THEN /\ consumerState' = "Parked"
/\ casSuccess' = [casSuccess EXCEPT ![self] = TRUE]
ELSE /\ casSuccess' = [casSuccess EXCEPT ![self] = FALSE]
/\ UNCHANGED consumerState
/\ IF casSuccess'[self]
THEN /\ pc' = [pc EXCEPT ![self] = "W2"]
ELSE /\ pc' = [pc EXCEPT ![self] = "W4"]
/\ UNCHANGED << signaled, msgToParent, stack, localConsumerState >>
W2(self) == /\ pc[self] = "W2"
/\ IF consumerState = "Parked"
THEN /\ pc' = [pc EXCEPT ![self] = "W3"]
ELSE /\ pc' = [pc EXCEPT ![self] = "W4"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
W3(self) == /\ pc[self] = "W3"
/\ signaled
/\ signaled' = FALSE
/\ pc' = [pc EXCEPT ![self] = "W2"]
/\ UNCHANGED << consumerState, msgToParent, stack, casSuccess,
localConsumerState >>
W4(self) == /\ pc[self] = "W4"
/\ Assert(consumerState \in {"Parked", "ShouldWakeup"},
"Failure of assertion at line 59, column 9.")
/\ pc' = [pc EXCEPT ![self] = "W5"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
W5(self) == /\ pc[self] = "W5"
/\ consumerState' = "Busy"
/\ pc' = [pc EXCEPT ![self] = "W8"]
/\ UNCHANGED << signaled, msgToParent, stack, casSuccess,
localConsumerState >>
W8(self) == /\ pc[self] = "W8"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ casSuccess' = [casSuccess EXCEPT ![self] = Head(stack[self]).casSuccess]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << consumerState, signaled, msgToParent,
localConsumerState >>
wait(self) == W1(self) \/ W2(self) \/ W3(self) \/ W4(self) \/ W5(self)
\/ W8(self)
N1(self) == /\ pc[self] = "N1"
/\ localConsumerState' = [localConsumerState EXCEPT ![self] = consumerState]
/\ pc' = [pc EXCEPT ![self] = "N2"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess >>
N2(self) == /\ pc[self] = "N2"
/\ IF localConsumerState[self] \in {"Busy", "ShouldWakeup"}
THEN /\ pc' = [pc EXCEPT ![self] = "N3"]
ELSE /\ pc' = [pc EXCEPT ![self] = "N4"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
N3(self) == /\ pc[self] = "N3"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ localConsumerState' = [localConsumerState EXCEPT ![self] = Head(stack[self]).localConsumerState]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << consumerState, signaled, msgToParent, casSuccess >>
N4(self) == /\ pc[self] = "N4"
/\ consumerState' = "ShouldWakeup"
/\ pc' = [pc EXCEPT ![self] = "N5"]
/\ UNCHANGED << signaled, msgToParent, stack, casSuccess,
localConsumerState >>
N5(self) == /\ pc[self] = "N5"
/\ pc' = [pc EXCEPT ![self] = "N6"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
N6(self) == /\ pc[self] = "N6"
/\ signaled' = TRUE
/\ pc' = [pc EXCEPT ![self] = "N7"]
/\ UNCHANGED << consumerState, msgToParent, stack, casSuccess,
localConsumerState >>
N7(self) == /\ pc[self] = "N7"
/\ IF consumerState /= "Busy"
THEN /\ pc' = [pc EXCEPT ![self] = "N8"]
ELSE /\ pc' = [pc EXCEPT ![self] = "N9"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
N8(self) == /\ pc[self] = "N8"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "N5"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
N9(self) == /\ pc[self] = "N9"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ localConsumerState' = [localConsumerState EXCEPT ![self] = Head(stack[self]).localConsumerState]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << consumerState, signaled, msgToParent, casSuccess >>
notify(self) == N1(self) \/ N2(self) \/ N3(self) \/ N4(self) \/ N5(self)
\/ N6(self) \/ N7(self) \/ N8(self) \/ N9(self)
MaySteal(self) == /\ pc[self] = "MaySteal"
/\ \/ /\ pc' = [pc EXCEPT ![self] = "NoSteal"]
\/ /\ pc' = [pc EXCEPT ![self] = "Steal"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
NoSteal(self) == /\ pc[self] = "NoSteal"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "ReqRET"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
Steal(self) == /\ pc[self] = "Steal"
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "notify",
pc |-> "ReqRET",
localConsumerState |-> localConsumerState[self] ] >>
\o stack[self]]
/\ localConsumerState' = [localConsumerState EXCEPT ![self] = "N/A"]
/\ pc' = [pc EXCEPT ![self] = "N1"]
/\ UNCHANGED << consumerState, signaled, msgToParent,
casSuccess >>
ReqRET(self) == /\ pc[self] = "ReqRET"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << consumerState, signaled, msgToParent,
casSuccess, localConsumerState >>
mayRequestWork(self) == MaySteal(self) \/ NoSteal(self) \/ Steal(self)
\/ ReqRET(self)
MayShare(self) == /\ pc[self] = "MayShare"
/\ \/ /\ pc' = [pc EXCEPT ![self] = "NoWork"]
\/ /\ pc' = [pc EXCEPT ![self] = "Share0"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
NoWork(self) == /\ pc[self] = "NoWork"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "ShareRET"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
Share0(self) == /\ pc[self] = "Share0"
/\ IF msgToParent = "Waiting"
THEN /\ pc' = [pc EXCEPT ![self] = "Share1"]
ELSE /\ pc' = [pc EXCEPT ![self] = "ShareRET"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
Share1(self) == /\ pc[self] = "Share1"
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "notify",
pc |-> "Share2",
localConsumerState |-> localConsumerState[self] ] >>
\o stack[self]]
/\ localConsumerState' = [localConsumerState EXCEPT ![self] = "N/A"]
/\ pc' = [pc EXCEPT ![self] = "N1"]
/\ UNCHANGED << consumerState, signaled, msgToParent,
casSuccess >>
Share2(self) == /\ pc[self] = "Share2"
/\ msgToParent' = "None"
/\ pc' = [pc EXCEPT ![self] = "ShareRET"]
/\ UNCHANGED << consumerState, signaled, stack, casSuccess,
localConsumerState >>
ShareRET(self) == /\ pc[self] = "ShareRET"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << consumerState, signaled, msgToParent,
casSuccess, localConsumerState >>
mayShareWork(self) == MayShare(self) \/ NoWork(self) \/ Share0(self)
\/ Share1(self) \/ Share2(self) \/ ShareRET(self)
Coworkers(self) == /\ pc[self] = "Coworkers"
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "mayRequestWork",
pc |-> "Done" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "MaySteal"]
/\ UNCHANGED << consumerState, signaled, msgToParent,
casSuccess, localConsumerState >>
producer(self) == Coworkers(self)
ParentWork == /\ pc[ParentTID] = "ParentWork"
/\ \/ /\ pc' = [pc EXCEPT ![ParentTID] = "PMayRW0"]
\/ /\ pc' = [pc EXCEPT ![ParentTID] = "PMaySW1"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
PMayRW0 == /\ pc[ParentTID] = "PMayRW0"
/\ stack' = [stack EXCEPT ![ParentTID] = << [ procedure |-> "mayRequestWork",
pc |-> "PMaySW0" ] >>
\o stack[ParentTID]]
/\ pc' = [pc EXCEPT ![ParentTID] = "MaySteal"]
/\ UNCHANGED << consumerState, signaled, msgToParent, casSuccess,
localConsumerState >>
PMaySW0 == /\ pc[ParentTID] = "PMaySW0"
/\ stack' = [stack EXCEPT ![ParentTID] = << [ procedure |-> "mayShareWork",
pc |-> "Terminate" ] >>
\o stack[ParentTID]]
/\ pc' = [pc EXCEPT ![ParentTID] = "MayShare"]
/\ UNCHANGED << consumerState, signaled, msgToParent, casSuccess,
localConsumerState >>
PMaySW1 == /\ pc[ParentTID] = "PMaySW1"
/\ stack' = [stack EXCEPT ![ParentTID] = << [ procedure |-> "mayShareWork",
pc |-> "PMayRW1" ] >>
\o stack[ParentTID]]
/\ pc' = [pc EXCEPT ![ParentTID] = "MayShare"]
/\ UNCHANGED << consumerState, signaled, msgToParent, casSuccess,
localConsumerState >>
PMayRW1 == /\ pc[ParentTID] = "PMayRW1"
/\ stack' = [stack EXCEPT ![ParentTID] = << [ procedure |-> "mayRequestWork",
pc |-> "Terminate" ] >>
\o stack[ParentTID]]
/\ pc' = [pc EXCEPT ![ParentTID] = "MaySteal"]
/\ UNCHANGED << consumerState, signaled, msgToParent, casSuccess,
localConsumerState >>
Terminate == /\ pc[ParentTID] = "Terminate"
/\ stack' = [stack EXCEPT ![ParentTID] = << [ procedure |-> "notify",
pc |-> "Done",
localConsumerState |-> localConsumerState[ParentTID] ] >>
\o stack[ParentTID]]
/\ localConsumerState' = [localConsumerState EXCEPT ![ParentTID] = "N/A"]
/\ pc' = [pc EXCEPT ![ParentTID] = "N1"]
/\ UNCHANGED << consumerState, signaled, msgToParent, casSuccess >>
parent == ParentWork \/ PMayRW0 \/ PMaySW0 \/ PMaySW1 \/ PMayRW1
\/ Terminate
ConsumerWork == /\ pc[ConsumerTID] = "ConsumerWork"
/\ \/ /\ pc' = [pc EXCEPT ![ConsumerTID] = "FoundWork"]
\/ /\ pc' = [pc EXCEPT ![ConsumerTID] = "Sleeping0"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
FoundWork == /\ pc[ConsumerTID] = "FoundWork"
/\ TRUE
/\ pc' = [pc EXCEPT ![ConsumerTID] = "Done"]
/\ UNCHANGED << consumerState, signaled, msgToParent, stack,
casSuccess, localConsumerState >>
Sleeping0 == /\ pc[ConsumerTID] = "Sleeping0"
/\ consumerState' = "IntendToSleep"
/\ pc' = [pc EXCEPT ![ConsumerTID] = "Sleeping1"]
/\ UNCHANGED << signaled, msgToParent, stack, casSuccess,
localConsumerState >>
Sleeping1 == /\ pc[ConsumerTID] = "Sleeping1"
/\ msgToParent' = "Waiting"
/\ pc' = [pc EXCEPT ![ConsumerTID] = "Sleeping2"]
/\ UNCHANGED << consumerState, signaled, stack, casSuccess,
localConsumerState >>
Sleeping2 == /\ pc[ConsumerTID] = "Sleeping2"
/\ stack' = [stack EXCEPT ![ConsumerTID] = << [ procedure |-> "wait",
pc |-> "Done",
casSuccess |-> casSuccess[ConsumerTID] ] >>
\o stack[ConsumerTID]]
/\ casSuccess' = [casSuccess EXCEPT ![ConsumerTID] = FALSE]
/\ pc' = [pc EXCEPT ![ConsumerTID] = "W1"]
/\ UNCHANGED << consumerState, signaled, msgToParent,
localConsumerState >>
consumer == ConsumerWork \/ FoundWork \/ Sleeping0 \/ Sleeping1
\/ Sleeping2
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == parent \/ consumer
\/ (\E self \in ProcSet: \/ wait(self) \/ notify(self)
\/ mayRequestWork(self) \/ mayShareWork(self))
\/ (\E self \in producers: producer(self))
\/ Terminating
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in producers : /\ WF_vars(producer(self))
/\ WF_vars(mayRequestWork(self))
/\ WF_vars(notify(self))
/\ /\ WF_vars(parent)
/\ WF_vars(mayRequestWork(ParentTID))
/\ WF_vars(mayShareWork(ParentTID))
/\ WF_vars(notify(ParentTID))
/\ WF_vars(consumer) /\ WF_vars(wait(ConsumerTID))
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment