diff --git a/specifications/composition/Composition.tla b/specifications/composition/Composition.tla new file mode 100644 index 00000000..649d134d --- /dev/null +++ b/specifications/composition/Composition.tla @@ -0,0 +1,142 @@ +---------------------------- MODULE Composition ---------------------------- +(**************************************************************************) +(* Background reading: Conjoining Specifications by Abadi and Lamport *) +(* https://lamport.azurewebsites.net/pubs/abadi-conjoining.pdf *) +(**************************************************************************) +EXTENDS Integers, Sequences + +Nodes == 1..3 \* Fixed to 1..3 here but should be a constant. + +(* COMPONENT Spec A (Computation) *) +------ MODULE A -------- +VARIABLES x, \* Private to this component. + active \* Shared with component spec B. +vars == <> + +Type == + /\ x \in 0..10 + /\ active \in [ Nodes -> BOOLEAN ] + +Init == + /\ x = 0 + /\ active \in [ Nodes -> BOOLEAN ] + +Next == + \* Not all nodes are inactive. + /\ \E i \in DOMAIN active : active[i] = TRUE + \* Mimic some computation. + /\ x' \in 1..10 + \* Computation changed the activation of 0 to N nodes. + /\ active' \in [ Nodes -> BOOLEAN ] + +================================== + +(* COMPONENT Spec B (Safra's termination detection) *) +------------ MODULE B ------------ +VARIABLES active, \* Shared with component A. + inactive \* Shared with component C. +vars == <> + +Type == + /\ inactive \subseteq Nodes + /\ active \in [ Nodes -> BOOLEAN ] + +Init == + /\ inactive = {} + /\ active \in [ Nodes -> BOOLEAN ] + +Next == + \* Since this high-level composition abstracts away communication, + \* we could abstract termination detection into a single step: + \* /\ \A i \in DOMAIN active : active[i] = FALSE + \* /\ inactive' = Nodes + \* However, we want to model the possible interleavings of the + \* A and B spec. + /\ \E i \in DOMAIN active: + active[i] = FALSE /\ i \notin inactive + /\ inactive' = inactive \cup { + CHOOSE i \in DOMAIN active: + active[i] = FALSE /\ i \notin inactive + } + /\ UNCHANGED active + +================================== + +(* COMPONENT Spec C (orderly/graceful shutdown) *) +------------ MODULE C ------------ +VARIABLES inactive \* Shared with component spec B. +vars == <> + +Type == + /\ inactive \subseteq Nodes + +Init == + /\ inactive \subseteq Nodes + +IOExit == TRUE \* Shutdown via sys.exit + +Next == + /\ inactive = Nodes + /\ UNCHANGED inactive + /\ IOExit +================================== + +----------------------------------------------------------------------------- + +(* Component specification. *) +VARIABLES x, active, inactive +vars == + <> + +A == INSTANCE A +B == INSTANCE B +C == INSTANCE C + +TypeOK == + /\ A!Type + /\ B!Type + /\ C!Type + +Init == + /\ A!Init + /\ B!Init + /\ C!Init + +\* PlusPy will most certainly not be able to evaluate this +\* Next formula. Might have to introduce an auxiliary variable +\* that represents the phase/stage of composed system. +Next == + \/ /\ ENABLED A!Next + /\ [A!Next]_vars + /\ UNCHANGED <> + \/ /\ ENABLED B!Next + /\ [B!Next]_vars + /\ UNCHANGED <> + \/ /\ [C!Next]_vars + /\ UNCHANGED <> + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +THEOREM Spec => []TypeOK + +(* The system eventually converges to shutdown. This, however, does + *not* hold because component spec A could keep computing forever. *) +AlwaysShutdown == + <>[][C!Next]_vars + +(* Unless all nodes are inactive at startup, some computation will occur. *) +ComputationIfSomeActive == + [n \in Nodes |-> FALSE] # active => <>[](x \in 1..10) +THEOREM Spec => ComputationIfSomeActive + +(* Iff - from some point onward - all nodes will become + inactive, the composed system will eventually shutdown. *) +ShutdownIfNoComputation == + <>[][~ A!Next]_vars => <>[][C!Next]_vars +THEOREM Spec => ShutdownIfNoComputation + +============================================================================= +\* Modification History +\* Last modified Mon Jun 15 17:37:21 PDT 2020 by markus +\* Last modified Fri Jun 12 16:30:19 PDT 2020 by Markus Kuppe +\* Created Fri Jun 12 10:30:09 PDT 2020 by Leslie Lamport diff --git a/specifications/ewd998/EWD998ChanID.tla b/specifications/ewd998/EWD998ChanID.tla index d2caa23d..4a665c6a 100644 --- a/specifications/ewd998/EWD998ChanID.tla +++ b/specifications/ewd998/EWD998ChanID.tla @@ -202,6 +202,30 @@ Next(n) == Spec == Init /\ [][\E n \in Node: Next(n)]_vars /\ \A n \in Node: WF_vars(System(n)) +OpenSpec == + Init /\ [][\E n \in Nodes: Next(n)]_<> \* Allow variables inbox + \* and count to change + \* even if no actions + \* of the next-state + \* relations are enabled. + \* A lower-level spec, + \* may want to send + \* messages (of a new + \* type). + \* We can't simply rewrite Spec to + \* I /\ []N_v with v declared as a constant + \* to be able to subst v with vars in model: + \* + \* CONSTANT v + \* Spec == Init /\ [][\E n \in Nodes: Next(n)_v + \* + \* vars is not constant-level and thus rejected + \* by level-checking. Also, it would mean that + \* the actual meaning of the spec requires us + \* to look at the model. And what about the + \* fairness constraint anyway?!? + /\ \A n \in Nodes: WF_vars(System(n)) + Max3TokenRounds == \* Termination is detected within a maximum of three token rounds after the \* system is terminated. diff --git a/specifications/ewd998/EWD998ChanIDTermination.tla b/specifications/ewd998/EWD998ChanIDTermination.tla new file mode 100644 index 00000000..2c00ac68 --- /dev/null +++ b/specifications/ewd998/EWD998ChanIDTermination.tla @@ -0,0 +1,232 @@ +---------------------- MODULE EWD998ChanIDTermination ---------------------- +(***************************************************************************) +(* This spec has the following two notable differences: *) +(* - Add SendTermination and RecvTermination actions that model how the *) +(* Initiator notifies the ring about final termination. *) +(* - Introduce a new message type TrmMsg that the initiator sends to *) +(* notify the other nodes about termination. Here, the initiator *) +(* sends N-1 messages (one to each node), but an implementation could *) +(* e.g. use a broadcast or multicast (which would make for a nice *) +(* example at the PlusPy level) *) +(* *) +(* Minor/Hack: *) +(* - Hacks TypeOK to account for the set of Messages having changed *) +(* without being included in the refinement mapping. *) +(***************************************************************************) +EXTENDS Integers, Sequences, FiniteSets, Naturals, Utils + + +CONSTANT Nodes +ASSUME IsFiniteSet(Nodes) /\ Nodes # {} + +N == Cardinality(Nodes) + +\* Choose a node to be the initiator of a fresh token. We don't care which one it +\* is as long as it is always the same. +Initiator == CHOOSE n \in Nodes : TRUE + +\* Organize Nodes in a ring. +RingOfNodes == + CHOOSE r \in [ Nodes -> Nodes ]: IsSimpleCycle(Nodes, r) + +Color == {"white", "black"} + +VARIABLES + active, + color, + counter, + inbox + +vars == <> + +EWD998ChanID == INSTANCE EWD998ChanID \* Straight forward refinement mapping + \* because we only *add* functionality. + +\* Define a new message type. +TrmMsg == [type |-> "trm"] + +\* Wow, this is ugly! It would be cleaner to declare a Message constant in +\* EWD998, but that would mean that its definition has to happen in a TLC +\* model for model checking. A TLC model cannot reference the definitions +\* of TokenMsg and BasicMsg in EWD998. +\*Message == {EWD998ChanID!EWD998Chan!TokenMsg, +\* EWD998ChanID!EWD998Chan!BasicMsg, +\* TrmMsg} +\* +\*\* Poor mans re-define of TypeOK here because we re-defined Message above. +\*TypeOK == +\* /\ EWD998ChanID!EWD998Chan!TypeOK +\* /\ inbox \in [Nodes -> Seq(Message)] +\* +\* Instead of the hacks above, I've used TLC's definition override to hack +\* TrmMsg into Messages: +\* Message[EWD998ChanId] <- +\* {EWD998ChanID!EWD998Chan!TokenMsg, EWD998ChanID!EWD998Chan!BasicMsg, TrmMsg} +\* This lets us check TypeOK and Inv. + +------------------------------------------------------------------------------ + +Init == + (* Rule 0 *) + /\ counter = [n \in Nodes |-> 0] \* c properly initialized + /\ inbox = [n \in Nodes |-> IF n = Initiator + THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >> + ELSE <<>>] \* with empty channels. + (* EWD840 *) + /\ active \in [Nodes -> BOOLEAN] + /\ color \in [Nodes -> Color] + +InitiateProbe == + /\ \A j \in 1..Len(inbox[Initiator]) : + /\ inbox[Initiator][j].type # "trm" + (* Rule 1 *) + /\ \E j \in 1..Len(inbox[Initiator]): + \* Token is at node the Initiator. + /\ inbox[Initiator][j].type = "tok" + /\ \* Previous round inconsistent, if: + \/ inbox[Initiator][j].color = "black" + \/ color[Initiator] = "black" + \* Implicit stated in EWD998 as c0 + q > 0 means that termination has not + \* been achieved: Initiate a probe if the token's color is white but the + \* number of in-flight messages is not zero. + \/ counter[Initiator] + inbox[Initiator][j].q # 0 + /\ inbox' = [inbox EXCEPT ![RingOfNodes[Initiator]] = Append(@, + [type |-> "tok", q |-> 0, + (* Rule 6 *) + color |-> "white"]), + ![Initiator] = RemoveAt(@, j) ] \* consume token message from inbox[0]. + (* Rule 6 *) + /\ color' = [ color EXCEPT ![Initiator] = "white" ] + \* The state of the nodes remains unchanged by token-related actions. + /\ UNCHANGED <> + +PassToken(n) == + (* Rule 2 *) + /\ ~ active[n] \* If machine i is active, keep the token. + /\ \E j \in 1..Len(inbox[n]) : + /\ inbox[n][j].type = "tok" + \* the machine nr.i+1 transmits the token to machine nr.i under q := q + c[i+1] + /\ LET tkn == inbox[n][j] + IN inbox' = [inbox EXCEPT ![RingOfNodes[n]] = + Append(@, [tkn EXCEPT !.q = tkn.q + counter[n], + !.color = IF color[n] = "black" + THEN "black" + ELSE tkn.color]), + ![n] = RemoveAt(@, j) ] \* pass on the token. + (* Rule 7 *) + /\ color' = [ color EXCEPT ![n] = "white" ] + \* The state of the nodes remains unchanged by token-related actions. + /\ UNCHANGED <> + +System(n) == \/ /\ n = Initiator + /\ InitiateProbe + \/ /\ n # Initiator + /\ PassToken(n) + +----------------------------------------------------------------------------- + +SendMsg(n) == + \* Only allowed to send msgs if node i is active. + /\ active[n] + (* Rule 0 *) + /\ counter' = [counter EXCEPT ![n] = @ + 1] + \* Non-deterministically choose a receiver node. + /\ \E j \in Nodes \ {n} : + \* Send a message (not the token) to j. + /\ inbox' = [inbox EXCEPT ![j] = Append(@, [type |-> "pl" ] ) ] + \* Note that we don't blacken node i as in EWD840 if node i + \* sends a message to node j with j > i + /\ UNCHANGED <> + +\* RecvMsg could write the incoming message to a (Java) buffer from which the (Java) implementation consumes it. +RecvMsg(n) == + (* Rule 0 *) + /\ counter' = [counter EXCEPT ![n] = @ - 1] + (* Rule 3 *) + /\ color' = [ color EXCEPT ![n] = "black" ] + \* Receipt of a message activates node n. + /\ active' = [ active EXCEPT ![n] = TRUE ] + \* Consume a message (not the token!). + /\ \E j \in 1..Len(inbox[n]) : + /\ inbox[n][j].type = "pl" + /\ inbox' = [inbox EXCEPT ![n] = RemoveAt(@, j) ] + /\ UNCHANGED <<>> + +Deactivate(n) == + /\ active[n] + /\ active' = [active EXCEPT ![n] = FALSE] + /\ UNCHANGED <> + +Environment(n) == + \/ SendMsg(n) + \/ RecvMsg(n) + \/ Deactivate(n) + +----------------------------------------------------------------------------- + +(* *) +SendTermination == + \* Don't send termination message multiple times. If - due to a + \* cosmic ray - the initiator doesn't correctly terminate, don't + \* let it interfere with future systems... + /\ \A j \in 1..Len(inbox[Initiator]) : + /\ inbox[Initiator][j].type # "trm" + \* Safra's termination conditions: + /\ active[Initiator] = FALSE + /\ color[Initiator] = "white" + /\ \E j \in 1..Len(inbox[Initiator]) : + /\ inbox[Initiator][j].type = "tok" + /\ inbox[Initiator][j].color = "white" + /\ counter[Initiator] + inbox[Initiator][j].q = 0 + \* Don't remove the token msg from inbox[Initiator] + \* because it would mess up Inv, i.e. tpos. +\* /\ inbox' = [inbox EXCEPT ![n] = RemoveAt(@, j) ] + \* Send termination message to all nodes (including self). + /\ inbox' = [ node \in Nodes |-> inbox[node] \o <>] + \* TODO: Doesn't this re-enable the InitiateProbe action above? + \* Account for the new messages sent. + /\ counter' = [counter EXCEPT ![Initiator] = N] + \* The state of the nodes remains unchanged by token-related actions. + /\ UNCHANGED <> + +(* Override with Sys.exit in PlusPy to gracefully terminate the runtime. *) +Terminate(n) == TRUE \*PrintT("sys.exit") + +(* *) +RecvTermination(n) == + /\ \E j \in 1..Len(inbox[n]) : + /\ inbox[n][j].type = "trm" + /\ Terminate(n) + /\ UNCHANGED vars + +Termination(n) == + \/ /\ n = Initiator + /\ SendTermination + \/ /\ n # Initiator + /\ RecvTermination(n) + +------------------------------------------------------------------------------ + +Next(n) == + \/ System(n) + \/ Environment(n) + \/ Termination(n) + +Spec == + Init /\ [][\E n \in Nodes: Next(n)]_vars + /\ \A n \in Nodes: + /\ WF_vars(System(n)) + /\ WF_vars(Environment(n)) + /\ WF_vars(Termination(n)) + +------------------------------------------------------------------------------ + +\* Iff - from some point onward - none of the nodes send out +\* payload messages, all nodes will eventually terminate. +TerminationMessagesIfNoPayloadMessages == + <>[][\A n \in Nodes : ~ SendMsg(n)]_vars => + <>[][\A n \in Nodes : RecvTermination(n)]_vars + +THEOREM Spec => TerminationMessagesIfNoPayloadMessages + +============================================================================= diff --git a/specifications/ewd998/EWD998ChanIDTerminationExtends.tla b/specifications/ewd998/EWD998ChanIDTerminationExtends.tla new file mode 100644 index 00000000..98db6f83 --- /dev/null +++ b/specifications/ewd998/EWD998ChanIDTerminationExtends.tla @@ -0,0 +1,128 @@ +------------------- MODULE EWD998ChanIDTerminationExtends ------------------- +(***************************************************************************) +(* This spec has the following notable differences compared to EWDChanID: *) +(* - Add SendTermination and RecvTermination actions that model how the *) +(* Initiator notifies the ring about final termination. *) +(* - Introduce a new message type TrmMsg that the initiator sends to *) +(* notify the other nodes about termination. Here, the initiator *) +(* sends N-1 messages (one to each node), but an implementation could *) +(* e.g. use a broadcast or multicast (which would make for a nice *) +(* example at the PlusPy level) *) +(* *) +(* Minor/Hack: *) +(* - Hacks TypeOK to account for the set of Messages having changed *) +(* without being included in the refinement mapping. *) +(***************************************************************************) +EXTENDS EWD998ChanID + +\* Declare and define a new message type. +TrmMsg == [type |-> "trm"] +TMessage == Message \cup {TrmMsg} + +------------------------------------------------------------------------------ + +(* *) +SendTermination(n) == + /\ n = Initiator + /\ active[Initiator] = FALSE + /\ color[Initiator] = "white" + \* Don't send termination message multiple times determined by looking at + \* global state (an actual implementation obviously won't need this). + /\ \A j \in 1..Len(inbox[n]) : + /\ inbox[n][j].type # "trm" + /\ \E j \in 1..Len(inbox[n]) : + /\ inbox[n][j].type = "tok" + /\ inbox[n][j].color = "white" + /\ counter[Initiator] + inbox[n][j].q = 0 + \* Don't remove the token msg from inbox[Initiator] + \* because it would mess up Inv, i.e. tpos. +\* /\ inbox' = [inbox EXCEPT ![n] = RemoveAt(@, j) ] + \* Send termination message to all nodes (including self). + /\ inbox' = [ node \in Nodes |-> inbox[node] \o <>] + \* The state of the nodes remains unchanged by token-related actions. + /\ UNCHANGED <> + +(* Override with Sys.exit in PlusPy to gracefully terminate the runtime. *) +Terminate(n) == TRUE \*PrintT("sys.exit") + +(* *) +RecvTermination(n) == + /\ \E j \in 1..Len(inbox[n]) : + /\ inbox[n][j].type = "trm" + /\ Terminate(n) + /\ UNCHANGED vars + +Termination(n) == + \/ SendTermination(n) + \/ RecvTermination(n) + +------------------------------------------------------------------------------ + +TTypeOK == + /\ TypeOK!1 + /\ TypeOK!2 + /\ TypeOK!3 + \* Seq(Messages) fails because we can't subst EWD998ChanID!Message + \* with TMessage above (to do that we'd have to *refine* EWD998ChanID). +\* /\ TypeOK!4 + /\ inbox \in [Nodes -> Seq(TMessage)] + /\ TypeOK!5 + +TSystem(n) == + IF n = Initiator + THEN InitiateProbe + ELSE PassToken(n) + +TEnvironment(n) == + \/ SendMsg(n) \/ RecvMsg(n) \/ Deactivate(n) + +\* We want the existential at the outermost level because of how PlusPy +\* maps the actual/physical nodes to the logical spec nodes. +TNext(n) == + \/ TSystem(n) + \/ TEnvironment(n) + \/ Termination(n) + +TSpec == + Init /\ [][\E n \in Nodes: TNext(n)]_vars + /\ \A n \in Nodes: + /\ WF_vars(TSystem(n)) + /\ WF_vars(TEnvironment(n)) + /\ WF_vars(Termination(n)) + +THEOREM TSpec => Inv \* This is EWD998Chan!Inv all the way up. + +------------------------------------------------------------------------------ + +\* Iff termination is detected by EWD998, there are no payload messages +\* in any node's inbox. +InvA == + EWD998!terminationDetected => + \A n \in Nodes: + \A msg \in Range(inbox[n]): + msg.type # "pl" + +\* Iff there is a termination message in any node's inbox, there are no +\* payload messages in any inbox. +InvB == + (\E n \in Nodes: + \E msg \in Range(inbox[n]): msg.type = "trm") + => + (\A n2 \in Nodes: + \A msg2 \in Range(inbox[n2]): msg2.type # "pl") + +THEOREM TSpec => (InvB /\ InvA) + +\* TerminationMessages does *not* hold because nodes can keep +\* sending (payload) messages indefinitely. +TerminationMessages == + <>[][\A n \in Nodes : RecvTermination(n)]_vars + +\* Iff - from some point onward - none of the nodes send out +\* payload messages, all nodes will eventually terminate. +TerminationMessagesIfNoPayloadMessages == + <>[][\A n \in Nodes : ~ SendMsg(n)]_vars => + <>[][\A n \in Nodes : RecvTermination(n)]_vars + +THEOREM TSpec => TerminationMessagesIfNoPayloadMessages +=============================================================================