diff --git a/manifest.json b/manifest.json index fa336cc3..f9da5ef7 100644 --- a/manifest.json +++ b/manifest.json @@ -1262,6 +1262,20 @@ } ] }, + { + "path": "specifications/Paxos/Voting2.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/Paxos/ApaVoting2.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, { "path": "specifications/Paxos/Paxos.tla", "communityDependencies": [], diff --git a/specifications/Paxos/ApaVoting2.tla b/specifications/Paxos/ApaVoting2.tla new file mode 100644 index 00000000..af7a79e1 --- /dev/null +++ b/specifications/Paxos/ApaVoting2.tla @@ -0,0 +1,38 @@ +--------------------------- MODULE ApaVoting2 ------------------------------- + +(*********************************************************************************) +(* In this module we instantiate VotingApalache with small constants in order to *) +(* run the `^Apalache^' model-checker. We also give type annotations for the *) +(* variables, which are required by `^Apalache^'. *) +(*********************************************************************************) + +EXTENDS Integers + +Value == {"V1_OF_VALUE","V2_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 == 2 +Ballot == 0..MaxBal \* NOTE: we have to make this a finite set for `^Apalache^' + +VARIABLES + \* @type: ACCEPTOR -> Set(<>); + votes, + \* @type: ACCEPTOR -> Int; + maxBal + +INSTANCE Voting2 + +\* To install `^Apalache,^' see the `^Apalache^' website at `^https://apalache.informal.systems/^'. +\* Note that this is not necessary if you are using the devcontainer, as `^Apalache,^' is already installed. +\* To check that the invariant holds initially, run: +\* apalache-mc check --init=Init --inv=Invariant --length=0 MCVotingApalache.tla +\* To check that the invariant is preserved, run: +\* apalache-mc check '--tuning-options=search.invariantFilter=1->.*' --init=Invariant --inv=Invariant --length=1 MCVotingApalache.tla + +=================================================================================== + diff --git a/specifications/Paxos/README b/specifications/Paxos/README index c6022b6f..231e6c05 100644 --- a/specifications/Paxos/README +++ b/specifications/Paxos/README @@ -29,4 +29,11 @@ MCPaxos three specifications above. The Toolbox makes it unnecessary for the user to write such specs, essentially producing them itself from the models defined by the user. - \ No newline at end of file + +Voting2 + A version of the Voting specification that can be analyzed + by the Apalache model-checker. Also contains an inductive + invariant that Apalache can verify for small system sizes. +ApaVoting2 + Specification used to model-check Voting2 with the Apalache + model-checker. diff --git a/specifications/Paxos/Voting2.tla b/specifications/Paxos/Voting2.tla new file mode 100644 index 00000000..3fcbf8f0 --- /dev/null +++ b/specifications/Paxos/Voting2.tla @@ -0,0 +1,110 @@ +------------------------------- MODULE Voting2 ------------------------------- + +(***********************************************************************************) +(* 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 make Ballot a constant in order to be able to substitute a finite set *) +(* for model-checking with Apalache. *) +(* *) +(* * We rewrite SafeAt and ShowsSafeAt to avoid ranges of integers with *) +(* non-constant bounds (which `^Apalache^' does not support). *) +(* *) +(* We also give an inductive invariant that proves the consistency property. On a *) +(* desktop computer from 2022, `^Apalache^' takes 1 minute and 45 seconds to check *) +(* that the invariant is inductive when there are 3 values, 3 processes, and 4 *) +(* ballots. For model-checking with `^Apalache,^'see `^ApaVoting2.tla^'. *) +(***********************************************************************************) + +EXTENDS Integers + +CONSTANTS + Value, + Acceptor, + Quorum, + Ballot + +VARIABLES + votes, + 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) + +Spec == Init /\ [][Next]_<> + +(********************************************************************************) +(* 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 + +=====================================================================================