From 08d80286ae4e6bc63f441c58848c9927ef854515 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 11 Jun 2020 08:58:56 -0700 Subject: [PATCH 1/8] Add definition of `OpenSpec` that allows the variables `inbox` and `count` to change independently of its next-state relation `Next`. In other words, we expect `inbox` and `count` to be shared variables with another component/spec. Signed-off-by: Markus Alexander Kuppe --- specifications/ewd998/EWD998ChanID.tla | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) 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. From 09aedf75236b73b2aa8496fdd8a854ca3c45cccf Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 11 Jun 2020 09:49:03 -0700 Subject: [PATCH 2/8] Experiment with *extending* EWD998ChanID to add functionality to shutdown/terminate nodes after termination *detection* by high-level specs. Signed-off-by: Markus Alexander Kuppe --- .../ewd998/EWD998ChanIDTerminationExtends.tla | 128 ++++++++++++++++++ 1 file changed, 128 insertions(+) create mode 100644 specifications/ewd998/EWD998ChanIDTerminationExtends.tla 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 +============================================================================= From 527d34c9f6a7188e61b8bab77e6da3ef9621cf37 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 11 Jun 2020 10:26:51 -0700 Subject: [PATCH 3/8] *Refine* (not extend as in previous commit) the spec EWD998ChanID to add shutdown functionality. Signed-off-by: Markus Alexander Kuppe --- .../ewd998/EWD998ChanIDTermination.tla | 232 ++++++++++++++++++ 1 file changed, 232 insertions(+) create mode 100644 specifications/ewd998/EWD998ChanIDTermination.tla 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 + +============================================================================= From 6ffadc8972c6c1339200536d09eef34bd1d85eea Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 12 Jun 2020 16:29:25 -0700 Subject: [PATCH 4/8] Basic concept how two component specification can combined. Signed-off-by: Markus Alexander Kuppe --- specifications/composition/Composition.tla | 99 ++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 specifications/composition/Composition.tla diff --git a/specifications/composition/Composition.tla b/specifications/composition/Composition.tla new file mode 100644 index 00000000..0d643c9d --- /dev/null +++ b/specifications/composition/Composition.tla @@ -0,0 +1,99 @@ +---------------------------- MODULE Composition ---------------------------- +(**************************************************************************) +(* Background reading: Conjoining Specifications by Abadi and Lamport *) +(* https://lamport.azurewebsites.net/pubs/abadi-conjoining.pdf *) +(* *) +(* Spec A and B are two components that together are composed into a *) +(* larger system. It's toy example in the sense that minimize *) +(* interaction of A and B to behaviors where first A takes its steps *) +(* followed by B. Variable y in A and B represents the control wire *) +(* that A and B use to synchronize. *) +(* Variable z has been added to make the example more interesting--it *) +(* only appears in spec A but *not* B. *) +(* *) +(**************************************************************************) +EXTENDS Naturals, Sequences + +(* COMPONENT Spec A *) +------------ MODULE A ------------ +VARIABLES x, \* Abstract/very high-level representation of the overall computation. + \* Think of it as some computation going on. At a certain state + \* of the computation, the composed system transitions into the + \* next phase. + y, \* Represents the phase that the composed system is in. + \* This toy example has three phases: <<"A", "B", "C">>. + z \* z is the variable that is only going to be present in spec A. +varsA == <> + +InitA == + /\ x = 0 + /\ y = "A" + /\ z = TRUE + +NextA == + /\ y = "A" + /\ x' = x + 1 + /\ IF x' = 5 + THEN y' = "B" + ELSE UNCHANGED y + /\ z' = ~ z + +================================== + +(* COMPONENT Spec B *) +VARIABLES x, + y +varsB == <> + +\* ++Observation: This is most likely not the original Init predicate of a +\* standalone B component, unless perhaps we consider spec A +\* the environment of spec B. In this particular example, +\* InitB is superfluouos anyway. However, if one would want +\* to prove something about spec B, we probably need an init +\* predicate (=> Conjoining Specifications). +InitB == + /\ x \in Nat \* Spec B may starts with x being any natural number, + \* which is where A left off. + /\ y \in {"A", "B"} \* Phase A or B, otherwise InitA /\ InitB in Spec + \* below will equal FALSE. + +NextB == + /\ y = "B" + /\ x' = x + 1 + /\ IF x' = 10 \* (Make sure values is greater than in spec A) + THEN y' = "C" \* Phase C of the composed system (or ultimate termination). + ELSE UNCHANGED y + +----------------------------------------------------------------------------- + +(* This *extends* component spec B to defines what happens to the variables + in spec A, which are not defined in B, when B takes a step. *) +VARIABLES restOfTheUniverse + +\* Note that TLC doesn't complain about restOfTheUniverse +\* not appearing in InitB. +OpenNextB == + /\ NextB + /\ UNCHANGED <> + +vars == + <> + +(* Composition of A and B (A /\ B) *) +(* Down here we know about the internals *) +(* of spec A and B (whitebox component). *) + +INSTANCE A WITH z <- restOfTheUniverse + +Spec == InitA /\ InitB /\ [][ \/ [NextA]_vars + \/ [OpenNextB]_vars + ]_vars + +Inv == y \in {"A","B","C"} +THEOREM Spec => Inv + +============================================================================= +\* Modification History +\* Last modified Fri Jun 12 16:30:33 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 From 72d67ae48854abe720747fe86bcc5ac17e4885e6 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 12 Jun 2020 16:45:06 -0700 Subject: [PATCH 5/8] If spec A has more than a one variable that does not appear in the other spec, we unfortunately have to adapt the composition and create more restsOfTheUniverse. The next-state relation of this composition evaluates to false after the initial state, because it defines variables z and zz to always have equal values. This is only satisfied in the special case where the values of variables z and zz in A are equal throughout all behaviors (e.g. Init changed to ... /\ zz = TRUE). Signed-off-by: Markus Alexander Kuppe --- specifications/composition/Composition.tla | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/specifications/composition/Composition.tla b/specifications/composition/Composition.tla index 0d643c9d..e80a4a33 100644 --- a/specifications/composition/Composition.tla +++ b/specifications/composition/Composition.tla @@ -23,12 +23,14 @@ VARIABLES x, \* Abstract/very high-level representation of the overall computati y, \* Represents the phase that the composed system is in. \* This toy example has three phases: <<"A", "B", "C">>. z \* z is the variable that is only going to be present in spec A. -varsA == <> + ,zz \* The more the merrier. +varsA == <> InitA == /\ x = 0 /\ y = "A" /\ z = TRUE + /\ zz= FALSE \* Could happen to be zz=TRUE. NextA == /\ y = "A" @@ -37,6 +39,7 @@ NextA == THEN y' = "B" ELSE UNCHANGED y /\ z' = ~ z + /\ zz'= ~ zz ================================== @@ -83,7 +86,7 @@ vars == (* Down here we know about the internals *) (* of spec A and B (whitebox component). *) -INSTANCE A WITH z <- restOfTheUniverse +INSTANCE A WITH z <- restOfTheUniverse, zz <- restOfTheUniverse Spec == InitA /\ InitB /\ [][ \/ [NextA]_vars \/ [OpenNextB]_vars @@ -94,6 +97,6 @@ THEOREM Spec => Inv ============================================================================= \* Modification History -\* Last modified Fri Jun 12 16:30:33 PDT 2020 by markus +\* Last modified Fri Jun 12 16:44:17 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 From 666bd5672b5e11ed4e8d5a88debbb6ed93ab25e5 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 12 Jun 2020 17:31:24 -0700 Subject: [PATCH 6/8] Nothing to see/Removal of variable zz. Signed-off-by: Markus Alexander Kuppe --- specifications/composition/Composition.tla | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/specifications/composition/Composition.tla b/specifications/composition/Composition.tla index e80a4a33..773449a4 100644 --- a/specifications/composition/Composition.tla +++ b/specifications/composition/Composition.tla @@ -23,14 +23,12 @@ VARIABLES x, \* Abstract/very high-level representation of the overall computati y, \* Represents the phase that the composed system is in. \* This toy example has three phases: <<"A", "B", "C">>. z \* z is the variable that is only going to be present in spec A. - ,zz \* The more the merrier. -varsA == <> +varsA == <> InitA == /\ x = 0 /\ y = "A" /\ z = TRUE - /\ zz= FALSE \* Could happen to be zz=TRUE. NextA == /\ y = "A" @@ -39,7 +37,6 @@ NextA == THEN y' = "B" ELSE UNCHANGED y /\ z' = ~ z - /\ zz'= ~ zz ================================== @@ -86,7 +83,7 @@ vars == (* Down here we know about the internals *) (* of spec A and B (whitebox component). *) -INSTANCE A WITH z <- restOfTheUniverse, zz <- restOfTheUniverse +INSTANCE A WITH z <- restOfTheUniverse Spec == InitA /\ InitB /\ [][ \/ [NextA]_vars \/ [OpenNextB]_vars @@ -97,6 +94,6 @@ THEOREM Spec => Inv ============================================================================= \* Modification History -\* Last modified Fri Jun 12 16:44:17 PDT 2020 by markus +\* Last modified Fri Jun 12 17:30:28 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 From e794bb8e64f0e99d358551909dd62324cb8d39a8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 12 Jun 2020 17:35:19 -0700 Subject: [PATCH 7/8] If the composition of A and B is such that the every composite behavior is the concatenation of a behavior defined by A and a behavior defined by B, we won't need the variable `y`. Instead, Spec is changed to use ITE with ENABLED evaluated on the next-state relation of spec A. Signed-off-by: Markus Alexander Kuppe --- specifications/composition/Composition.tla | 35 ++++++++-------------- 1 file changed, 13 insertions(+), 22 deletions(-) diff --git a/specifications/composition/Composition.tla b/specifications/composition/Composition.tla index 773449a4..96874ab0 100644 --- a/specifications/composition/Composition.tla +++ b/specifications/composition/Composition.tla @@ -20,30 +20,23 @@ VARIABLES x, \* Abstract/very high-level representation of the overall computati \* Think of it as some computation going on. At a certain state \* of the computation, the composed system transitions into the \* next phase. - y, \* Represents the phase that the composed system is in. - \* This toy example has three phases: <<"A", "B", "C">>. z \* z is the variable that is only going to be present in spec A. -varsA == <> +varsA == <> InitA == /\ x = 0 - /\ y = "A" /\ z = TRUE NextA == - /\ y = "A" + /\ x < 6 /\ x' = x + 1 - /\ IF x' = 5 - THEN y' = "B" - ELSE UNCHANGED y /\ z' = ~ z ================================== (* COMPONENT Spec B *) -VARIABLES x, - y -varsB == <> +VARIABLES x +varsB == <> \* ++Observation: This is most likely not the original Init predicate of a \* standalone B component, unless perhaps we consider spec A @@ -54,15 +47,10 @@ varsB == <> InitB == /\ x \in Nat \* Spec B may starts with x being any natural number, \* which is where A left off. - /\ y \in {"A", "B"} \* Phase A or B, otherwise InitA /\ InitB in Spec - \* below will equal FALSE. NextB == - /\ y = "B" + /\ x < 10 /\ x' = x + 1 - /\ IF x' = 10 \* (Make sure values is greater than in spec A) - THEN y' = "C" \* Phase C of the composed system (or ultimate termination). - ELSE UNCHANGED y ----------------------------------------------------------------------------- @@ -77,7 +65,7 @@ OpenNextB == /\ UNCHANGED <> vars == - <> + <> (* Composition of A and B (A /\ B) *) (* Down here we know about the internals *) @@ -85,15 +73,18 @@ vars == INSTANCE A WITH z <- restOfTheUniverse -Spec == InitA /\ InitB /\ [][ \/ [NextA]_vars - \/ [OpenNextB]_vars +Spec == InitA /\ InitB /\ [][ IF ENABLED NextA THEN [NextA]_vars + ELSE [OpenNextB]_vars ]_vars -Inv == y \in {"A","B","C"} +Inv == x \in 0..10 THEOREM Spec => Inv +\* Not a theorem due to no fairness constraint. +Live == + <>[](x = 10) ============================================================================= \* Modification History -\* Last modified Fri Jun 12 17:30:28 PDT 2020 by markus +\* Last modified Fri Jun 12 17:34:09 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 From fc16cdc094507300b3d7905430b76c17704f2c1a Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 15 Jun 2020 21:29:00 -0700 Subject: [PATCH 8/8] Compose Compute, Detect Termination (EWD998), and Shutdown. Signed-off-by: Markus Alexander Kuppe --- specifications/composition/Composition.tla | 182 +++++++++++++-------- 1 file changed, 117 insertions(+), 65 deletions(-) diff --git a/specifications/composition/Composition.tla b/specifications/composition/Composition.tla index 96874ab0..649d134d 100644 --- a/specifications/composition/Composition.tla +++ b/specifications/composition/Composition.tla @@ -2,89 +2,141 @@ (**************************************************************************) (* Background reading: Conjoining Specifications by Abadi and Lamport *) (* https://lamport.azurewebsites.net/pubs/abadi-conjoining.pdf *) -(* *) -(* Spec A and B are two components that together are composed into a *) -(* larger system. It's toy example in the sense that minimize *) -(* interaction of A and B to behaviors where first A takes its steps *) -(* followed by B. Variable y in A and B represents the control wire *) -(* that A and B use to synchronize. *) -(* Variable z has been added to make the example more interesting--it *) -(* only appears in spec A but *not* B. *) -(* *) (**************************************************************************) -EXTENDS Naturals, Sequences - -(* COMPONENT Spec A *) ------------- MODULE A ------------ -VARIABLES x, \* Abstract/very high-level representation of the overall computation. - \* Think of it as some computation going on. At a certain state - \* of the computation, the composed system transitions into the - \* next phase. - z \* z is the variable that is only going to be present in spec A. -varsA == <> - -InitA == +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 - /\ z = TRUE - -NextA == - /\ x < 6 - /\ x' = x + 1 - /\ z' = ~ z + /\ 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 *) -VARIABLES x -varsB == <> +(* COMPONENT Spec B (Safra's termination detection) *) +------------ MODULE B ------------ +VARIABLES active, \* Shared with component A. + inactive \* Shared with component C. +vars == <> -\* ++Observation: This is most likely not the original Init predicate of a -\* standalone B component, unless perhaps we consider spec A -\* the environment of spec B. In this particular example, -\* InitB is superfluouos anyway. However, if one would want -\* to prove something about spec B, we probably need an init -\* predicate (=> Conjoining Specifications). -InitB == - /\ x \in Nat \* Spec B may starts with x being any natural number, - \* which is where A left off. +Type == + /\ inactive \subseteq Nodes + /\ active \in [ Nodes -> BOOLEAN ] -NextB == - /\ x < 10 - /\ x' = x + 1 +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 == <> -(* This *extends* component spec B to defines what happens to the variables - in spec A, which are not defined in B, when B takes a step. *) -VARIABLES restOfTheUniverse +Type == + /\ inactive \subseteq Nodes -\* Note that TLC doesn't complain about restOfTheUniverse -\* not appearing in InitB. -OpenNextB == - /\ NextB - /\ UNCHANGED <> +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) -(* Composition of A and B (A /\ B) *) -(* Down here we know about the internals *) -(* of spec A and B (whitebox component). *) +THEOREM Spec => []TypeOK -INSTANCE A WITH z <- restOfTheUniverse +(* The system eventually converges to shutdown. This, however, does + *not* hold because component spec A could keep computing forever. *) +AlwaysShutdown == + <>[][C!Next]_vars -Spec == InitA /\ InitB /\ [][ IF ENABLED NextA THEN [NextA]_vars - ELSE [OpenNextB]_vars - ]_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 -Inv == x \in 0..10 -THEOREM Spec => Inv +(* 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 -\* Not a theorem due to no fairness constraint. -Live == - <>[](x = 10) ============================================================================= \* Modification History -\* Last modified Fri Jun 12 17:34:09 PDT 2020 by markus +\* 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