Skip to content

Commit

Permalink
Add Misra Reachability Algorithm
Browse files Browse the repository at this point in the history
  • Loading branch information
Leslie Lamport authored and lemmy committed Apr 15, 2019
1 parent 41ccaa4 commit 59ac7a1
Show file tree
Hide file tree
Showing 16 changed files with 1,310 additions and 0 deletions.
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ Do you have your own case study that you like to share with the community? Send
| 59 | TwoPhase | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/TwoPhase">Two-phase handshaking</a> | Stephan Merz | | &#10004; | Nat |
| 60 | VoldemortKV | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/VoldemortKV">Voldemort distributed key value store</a> | Murat Demirbas | | &#10004; | FinSet, Int, Seq |
| 61 | Missionaries and Cannibals | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/MissionariesAndCannibals">Missionaries and Cannibals</a> | Leslie Lamport | | &#10004; | FinSet, Int |
| 62 | Misra Reachability Algorithm | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/MisraReachability">Misra Reachability Algorithm</a> | Leslie Lamport | &#10004; | &#10004; | Int, Seq, FiniteSets, TLC, TLAPS, NaturalsInduction |


## License
Expand Down
Binary file added specifications/MisraReachability/ParReach.pdf
Binary file not shown.
235 changes: 235 additions & 0 deletions specifications/MisraReachability/ParReach.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,235 @@
------------------------------ MODULE ParReach ------------------------------
(***************************************************************************)
(* This module describes an algorithm that is a multiprocess *)
(* implementation of the algorithm in module Reachable. You should *)
(* understand that algorithm before reading further in this module. *)
(* *)
(* Here, this module's algorithm will be called the parallel algorithm and *)
(* module Reachable's algorithm will be called Misra's algorithm. The *)
(* parallel algorithm computes the same thing as Misra's algorithm -- *)
(* namely, it terminates if and only if the set of nodes reachable from *)
(* Root is finite, in which case the variable `marked' equals that *)
(* reachable set when the algorithm terminates. The parallel algorithm *)
(* does this by implementing Misra's algorithm under a refinement mapping *)
(* such that *)
(* *)
(* - The parallel algorithm's `marked' variable implements the Misra *)
(* algorithm's variable of the same name. *)
(* *)
(* - The parallel algorithm has terminated if and only if Misra's *)
(* algorithm has. *)
(***************************************************************************)
EXTENDS Reachability, Integers, FiniteSets

(***************************************************************************)
(* The Misra algorithm's constants Nodes and Succ are imported from module *)
(* Reachability. Its Root constant is declared here, as is the set Procs *)
(* of processes that execute the parallel algorithm. *)
(***************************************************************************)
CONSTANT Root, Procs

ASSUME RootAssump == Root \in Nodes
ASSUME ProcsAssump == /\ Procs # {}
/\ IsFiniteSet(Procs)

Reachable == ReachableFrom({Root})
(*************************************************************************)
(* This definition is copied from module Reachable. (We don't want to *)
(* extend that module because it would lead to name conflicts with the *)
(* TLA+ translation of the algorithm in this module.) *)
(*************************************************************************)
-----------------------------------------------------------------------------
(****************************************************************************
The algorithm executed by each process is the same as Misra's
algorithm, except that where the Misra algorithm adds to `marked' a
node v in vroot and adds the nodes in Succ[v] to vroot in a single
step, the parallel algorithm first adds v to `marked' and then adds the
nodes in Succ[v] one at a time to vroot in separate steps.
Note that one process can add node v to `marked', and then another
process can remove v from vroot before the first process has added any
nodes in Succ[v] to vroot. This implies that a process can find vroot
equal to {} and terminate before `marked' contains all the nodes
reachable from Root. This doesn't affect correctness of the parallel
algorithm because, as long as `marked' doesn't contain all the nodes it
should, there will be at least one process that hasn't terminated.
However, it can cause inefficiency because processes can terminate
while there is still useful work for them to do. In practice, the
evaluation of the test vroot /= {} can be implemented in a way that
makes it impossible or perhaps very unlikely to obtain the value FALSE
if there are still nodes being added to vroot. Devising such an
implementation is a nice exercise that will not be discussed here.
Here is the algorithm's PlusCal code. The initial values of the
process-local variables u and toVroot don't matter. It's always a good
idea to make them "type correct", and the initial value of toVroot is
an obvious choice that also makes the refinement mapping a little
simpler.
--algorithm ParallelReachability {
variables marked = {}, vroot = {Root};
fair process (p \in Procs)
variables u = Root, toVroot = {} ;
{ a: while (vroot /= {})
{ with (v \in vroot) { u := v };
b: if (u \notin marked)
{ marked := marked \cup {u};
toVroot := Succ[u] ;
c: while (toVroot /= {})
{ with (w \in toVroot) {
vroot := vroot \cup {w} ;
toVroot := toVroot \ {w} }
}
}
else { vroot := vroot \ {u} }
}
}
}
Here is the TLA+ translation of the PlusCal code.
***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES marked, vroot, pc, u, toVroot

vars == << marked, vroot, pc, u, toVroot >>

ProcSet == (Procs)

Init == (* Global variables *)
/\ marked = {}
/\ vroot = {Root}
(* Process p *)
/\ u = [self \in Procs |-> Root]
/\ toVroot = [self \in Procs |-> {}]
/\ pc = [self \in ProcSet |-> "a"]

a(self) == /\ pc[self] = "a"
/\ IF vroot /= {}
THEN /\ \E v \in vroot:
u' = [u EXCEPT ![self] = v]
/\ pc' = [pc EXCEPT ![self] = "b"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
/\ u' = u
/\ UNCHANGED << marked, vroot, toVroot >>

b(self) == /\ pc[self] = "b"
/\ IF u[self] \notin marked
THEN /\ marked' = (marked \cup {u[self]})
/\ toVroot' = [toVroot EXCEPT ![self] = Succ[u[self]]]
/\ pc' = [pc EXCEPT ![self] = "c"]
/\ vroot' = vroot
ELSE /\ vroot' = vroot \ {u[self]}
/\ pc' = [pc EXCEPT ![self] = "a"]
/\ UNCHANGED << marked, toVroot >>
/\ u' = u

c(self) == /\ pc[self] = "c"
/\ IF toVroot[self] /= {}
THEN /\ \E w \in toVroot[self]:
/\ vroot' = (vroot \cup {w})
/\ toVroot' = [toVroot EXCEPT ![self] = toVroot[self] \ {w}]
/\ pc' = [pc EXCEPT ![self] = "c"]
ELSE /\ pc' = [pc EXCEPT ![self] = "a"]
/\ UNCHANGED << vroot, toVroot >>
/\ UNCHANGED << marked, u >>

p(self) == a(self) \/ b(self) \/ c(self)

Next == (\E self \in Procs: p(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
/\ \A self \in Procs : WF_vars(p(self))

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

(***************************************************************************)
(* The formula Inv defined below is the inductive invariant needed to *)
(* prove that the parallel algorithm implements the safety part of Misra's *)
(* algorithm. In addition to type correctness, it asserts two simple *)
(* relations between the values of the local variables u and toVroot and *)
(* the control state of the process: *)
(* *)
(* - toVroot = {} except when control is at c *)
(* *)
(* - u is in vroot \cup marked when control is at b. This is invariant *)
(* because u is an element of vroot when control arrives at b, and *)
(* an element is removed from vroot only after it is added to `marked'. *)
(* *)
(* The fact that such a simple invariant is needed to prove that each step *)
(* of the parallel algorithm implements a step allowed by Misra's *)
(* algorithm means that the easiest way to show that the parallel *)
(* algorithm is correct, given the correctness of Misra's algorithm, is to *)
(* show that it implements Misra's algorithm. *)
(***************************************************************************)
Inv == /\ marked \in SUBSET Nodes
/\ vroot \in SUBSET Nodes
/\ u \in [Procs -> Nodes]
/\ toVroot \in [Procs -> SUBSET Nodes]
/\ pc \in [Procs -> {"a", "b", "c", "Done"}]
/\ \A q \in Procs : /\ (pc[q] \in {"a", "b", "Done"}) => (toVroot[q] = {})
/\ (pc[q] = "b") => (u[q] \in vroot \cup marked)

(***************************************************************************)
(* To define a refinement mapping from states of the parallel algorithm to *)
(* states of Misra's algorithm, we must define the expressions in this *)
(* module that represent the values of the Misra algorithm's variables. *)
(* The value of the variable `marked' of Misra's algorithm is represented *)
(* by the value of variable `marked' of the parallel algorithm. The *)
(* values of the variables vroot and pc of Misra's algorithm are *)
(* represented by the expressions vrootBar and pcBar defined below. *)
(* *)
(* For the parallel algorithm to implement Misra's algorithm under this *)
(* refinement mapping, the same b step that adds node u to `marked' must *)
(* also add Succ[u] to vrootBar. The c steps that move individual *)
(* elements of Succ[u] from toVroot must leave vrootBar unchanged. (Those *)
(* steps implement stuttering steps of Misra's algorithm.) This leads us *)
(* to the following definition of vrootBar. *)
(***************************************************************************)
vrootBar == vroot \cup UNION {toVroot[i] : i \in Procs}

(***************************************************************************)
(* Since the variable pc of Misra's algorithm always equals "a" or "Done", *)
(* and we want it to equal "Done" if and only if the parallel algorithm *)
(* has terminated, the definition of pcBar is obvious. *)
(***************************************************************************)
pcBar == IF \A q \in Procs : pc[q] = "Done" THEN "Done" ELSE "a"

R == INSTANCE Reachable WITH vroot <- vrootBar, pc <- pcBar
(*************************************************************************)
(* For every definition Op in module Reachable, this statement defines *)
(* the operator R!Op in the current module to have as its definition the *)
(* expression obtained from the definition of Op in module Reachable by *)
(* substituting vrootBar for vroot and pcBar for pc. *)
(*************************************************************************)

(***************************************************************************)
(* The following theorem is the TLA+ assertion of the statement that the *)
(* parallel algorithm implements Misra's algorithm under the refinement *)
(* mapping defined above. It can be checked by TLC for models large *)
(* enough to make us reasonably confident that it is correct. (To check *)
(* it, use models with behavior specification spec that check the temporal *)
(* property R!Spec.) *)
(***************************************************************************)
THEOREM Spec => R!Spec

(***************************************************************************)
(* By the definition of formula Spec of module Reachable, this theorem *)
(* follows from the following two theorems, the first showing that the *)
(* parallel algorithm implements the safety part of Misra's algorithm *)
(* (which implies partial correctness) and the second showing that it *)
(* implements the fairness part of that algorithm (which implies *)
(* termination). Module ParReachProofs contains a TLAPS checked proof of *)
(* the first theorem. *)
(***************************************************************************)
THEOREM Spec => R!Init /\ [][R!Next]_R!vars
THEOREM Spec => WF_R!vars(R!Next)
=============================================================================
\* Modification History
\* Last modified Sun Apr 14 16:53:23 PDT 2019 by lamport
\* Created Mon Apr 08 10:48:52 PDT 2019 by lamport
Binary file not shown.
70 changes: 70 additions & 0 deletions specifications/MisraReachability/ParReachProofs.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
--------------------------- MODULE ParReachProofs ---------------------------
(***************************************************************************)
(* This module contains TLAPS checked proofs of the safety properties *)
(* asserted in module ParReach--namely, the invariance of Inv and that the *)
(* parallel alorithm implements the safety part of Misra's algorithm under *)
(* the refinement mapping defined there. *)
(***************************************************************************)
EXTENDS ParReach, Integers, TLAPS

LEMMA TypeInvariant == Spec => []Inv
<1>1. Init => Inv
BY RootAssump DEF Init, Inv, ProcSet
<1>2. Inv /\ [Next]_vars => Inv'
BY SuccAssump DEF Inv, Next, vars, ProcSet, p, a, b, c
<1>3. QED
BY <1>1, <1>2, PTL DEF Spec

THEOREM Spec => R!Init /\ [][R!Next]_R!vars
<1>1. Init => R!Init
BY ProcsAssump DEF Init, R!Init, pcBar, vrootBar, ProcSet
<1>2. Inv /\ [Next]_vars => [R!Next]_R!vars
<2> SUFFICES ASSUME Inv,
[Next]_vars
PROVE [R!Next]_R!vars
OBVIOUS
<2> USE DEF Inv, Next, vars, R!Next, R!vars, vrootBar, pcBar
<2>1. ASSUME NEW self \in Procs,
a(self)
PROVE [R!Next]_R!vars
<3>1. ASSUME vroot # {}
PROVE UNCHANGED R!vars
BY <2>1, <3>1 DEF a
<3>2. ASSUME vroot = {}
PROVE [R!Next]_R!vars
<4>1. ASSUME vrootBar = {}
PROVE [R!Next]_R!vars
BY <2>1, <3>2, <4>1 DEF a, R!a
<4>2. ASSUME vrootBar # {}
PROVE UNCHANGED R!vars
<5>1. \E q \in Procs \ {self} : pc[q] # "Done"
BY <4>2, <3>2, <2>1 DEF a
<5>2. pcBar' # "Done"
BY <5>1, <3>2, <2>1 DEF a
<5>. QED
BY <5>2, <3>2, <2>1 DEF a
<4>3. QED
BY <4>1, <4>2
<3>3. QED
BY <3>1, <3>2 DEF R!Next
<2>2. ASSUME NEW self \in Procs,
b(self)
PROVE [R!Next]_R!vars
BY <2>2 DEF b, R!a
<2>3. ASSUME NEW self \in Procs,
c(self)
PROVE [R!Next]_R!vars
BY <2>3 DEF c
<2>4. CASE UNCHANGED vars
BY <2>4
<2>5. QED
BY <2>1, <2>2, <2>3, <2>4 DEF Next, p
<1>3. QED
BY <1>1, <1>2, TypeInvariant, PTL DEF Spec



=============================================================================
\* Modification History
\* Last modified Sun Apr 14 16:55:36 PDT 2019 by lamport
\* Created Sat Apr 13 14:37:54 PDT 2019 by lamport
43 changes: 43 additions & 0 deletions specifications/MisraReachability/README
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
Misra Reachability Algorithm

This example is built around a simple sequential algorithm by Jayadev
Misra for computing the set of nodes in a directed graph thaa are
reachable from a given node. It includes a multiprocess algorithm
that implements Misra's algorithm and TLAPS checked proofs that the
two algorithms satisfy their safety property. Proofs are in separate
modules so the algorithms can be read independently from the proofs.
Here is what each module contains, in the order one might want to read
them.

Reachable
Misra's algorithm written in PlusCal, its correctness properties, and
an informal proof of its correctness.

Reachability
The TLA+ definitions of a directed graph and reachability.
It is imported by module Reachable.

ParReach
The parallel implementation of Misra's algorithm written in PlusCal
and the TLA+ formulation of the assertion that it implements
Misra's algorithm under a suitable refinement mapping.

ReachableProofs
The TLAPS checked proofs that the algorithm of module Reachable
satisfies its desired safety property. The proof assumes some
properties of reachability in a directed graph.

ReachabilityTest
Defines operators that TLC can use to check the correctness of the
properties of directed graphs assumed by the proofs in module
ReachableProofs.

ParReachProofs
A TLAPS checked proof that the parallel algorithm of module ParReach
implements the safety part of Misra's algorithm, under the refinement
mapping defined in that module.

ReachabilityProofs
TLAPS checked proofs of the reachability properties used in the proofs
of module ReachableProofs.

Binary file not shown.
Loading

0 comments on commit 59ac7a1

Please sign in to comment.