From a9a134cdf37bb1380b4007b9752db0ae8897e238 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sat, 20 Jan 2024 21:35:25 -0800 Subject: [PATCH] Add version of Voting.tla that can be analyzed by Apalache. This includes an inductive invariant that establishes consistency. Signed-off-by: Giuliano Losa --- specifications/Paxos/VotingApalache.tla | 129 ++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 specifications/Paxos/VotingApalache.tla diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla new file mode 100644 index 00000000..f5bad2c2 --- /dev/null +++ b/specifications/Paxos/VotingApalache.tla @@ -0,0 +1,129 @@ +------------------------------- MODULE VotingApalache ------------------------------- + +(***********************************************************************************) +(* This is a version of Voting.tla that can be analyzed by the `^Apalache^' *) +(* model-checker. Here are the differences compared to Voting.tla: *) +(* *) +(* * We give concrete definitions for the constants *) +(* *) +(* * We fix the number of ballots *) +(* *) +(* * We add the necessary type annotation on variables *) +(* *) +(* * We rewrite SafeAt and ShowsSafeAt to avoid ranges of integers with *) +(* non-constant bounds (which `^Apalache^' does not support). *) +(* *) +(* Ideally, we would have instantiated Voting.tla, made the appropriate *) +(* substitutions, and reused the rest. However, the presence of TLAPS proofs in *) +(* Consensus.tla and Voting.tla seem to make `^Apalache^' fail. *) +(* *) +(* We also give an inductive invariant that proves the Safety property. On a *) +(* desktop computer bought in 2022, `^Apalache^' takes 1 minute and 45 seconds to *) +(* check that the invariant is inductive when there are for 3 values, 3 processes, *) +(* and 4 ballots. Instructions to run `^Apalache^' appear at the end of the *) +(* specification. *) +(***********************************************************************************) + +EXTENDS Integers, FiniteSets + +Value == {"V1_OF_VALUE","V2_OF_VALUE","V3_OF_VALUE"} +Acceptor == {"A1_OF_ACCEPTOR","A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"} +\* The quorums are the sets of 2 acceptors: +Quorum == { + {"A1_OF_ACCEPTOR","A2_OF_ACCEPTOR"}, + {"A1_OF_ACCEPTOR","A3_OF_ACCEPTOR"}, + {"A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"}} + +MaxBal == 3 \* 1m45s with MaxBal=3 +Ballot == 0..MaxBal \* NOTE: has to be finite for `^Apalache^' because it is used as the domain of a function + +VARIABLES + \* @type: ACCEPTOR -> Set(<>); + votes, + \* @type: ACCEPTOR -> Int; + maxBal + +TypeOK == + /\ votes \in [Acceptor -> SUBSET (Ballot\times Value)] + /\ maxBal \in [Acceptor -> Ballot\cup {-1}] + +VotedFor(a, b, v) == <> \in votes[a] + +ChosenAt(b, v) == + \E Q \in Quorum : \A a \in Q : VotedFor(a, b, v) + +chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)} + +DidNotVoteAt(a, b) == \A v \in Value : ~ VotedFor(a, b, v) + +CannotVoteAt(a, b) == /\ maxBal[a] > b + /\ DidNotVoteAt(a, b) +NoneOtherChoosableAt(b, v) == + \E Q \in Quorum : + \A a \in Q : VotedFor(a, b, v) \/ CannotVoteAt(a, b) + +SafeAt(b, v) == \A c \in Ballot : c < b => NoneOtherChoosableAt(c, v) + +ShowsSafeAt(Q, b, v) == + /\ \A a \in Q : maxBal[a] \geq b + \* NOTE: `^Apalache^' does not support non-constant integer ranges (e.g. we cannot write (c+1)..(b-1)) + /\ \E c \in Ballot\cup {-1} : + /\ c < b + /\ (c # -1) => \E a \in Q : VotedFor(a, c, v) + /\ \A d \in Ballot : c < d /\ d < b => \A a \in Q : DidNotVoteAt(a, d) + +Init == + /\ votes = [a \in Acceptor |-> {}] + /\ maxBal = [a \in Acceptor |-> -1] + +IncreaseMaxBal(a, b) == + /\ b > maxBal[a] + /\ maxBal' = [maxBal EXCEPT ![a] = b] + /\ UNCHANGED votes + +VoteFor(a, b, v) == + /\ maxBal[a] \leq b + /\ \A vt \in votes[a] : vt[1] # b + /\ \A c \in Acceptor \ {a} : + \A vt \in votes[c] : (vt[1] = b) => (vt[2] = v) + /\ \E Q \in Quorum : ShowsSafeAt(Q, b, v) + /\ votes' = [votes EXCEPT ![a] = @ \cup {<>}] + /\ maxBal' = [maxBal EXCEPT ![a] = b] + +Next == \E a \in Acceptor, b \in Ballot : + \/ IncreaseMaxBal(a, b) + \/ \E v \in Value : VoteFor(a, b, v) + +(********************************************************************************) +(* Next, we define an inductive invariant that shows consistency. We reuse *) +(* definitions from Voting.tla and add the property NoVoteAfterMaxBal, which is *) +(* needed to make the invariant inductive. *) +(********************************************************************************) + +VotesSafe == \A a \in Acceptor, b \in Ballot, v \in Value : + VotedFor(a, b, v) => SafeAt(b, v) + +OneValuePerBallot == + \A a1, a2 \in Acceptor, b \in Ballot, v1, v2 \in Value : + VotedFor(a1, b, v1) /\ VotedFor(a2, b, v2) => (v1 = v2) + +NoVoteAfterMaxBal == \A a \in Acceptor, b \in Ballot, v \in Value : + <> \in votes[a] => /\ b <= maxBal[a] + +Consistency == \A v,w \in chosen : v = w + +\* This invariant is inductive and establishes consistency: +Invariant == + /\ TypeOK + /\ VotesSafe + /\ OneValuePerBallot + /\ NoVoteAfterMaxBal + /\ Consistency + +\* To install `^Apalache,^' see the `^Apalache^' website at `^https://apalache.informal.systems/^' +\* To check that the invariant holds initially, run: +\* ${APALACHE_HOME}/script/run-docker.sh check --init=Init --inv=Invariant --length=0 VotingApalache.tla +\* To check that the invariant is preserved, run: +\* ${APALACHE_HOME}/script/run-docker.sh check '--tuning-options=search.invariantFilter=1->.*' --init=Invariant --inv=Invariant --length=1 VotingApalache.tla + +=====================================================================================