From 4af59b379a9ca7319684a7a3f2838d34c74cf1c2 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 22 Sep 2024 10:28:41 -0700 Subject: [PATCH] [Civl] Rearrange Paxos code to model natural flow of messages (#950) --- Test/civl/paxos/PaxosActions.bpl | 62 ++++++++++++++-------------- Test/civl/paxos/PaxosImpl.bpl | 70 ++++++++++++++++---------------- 2 files changed, 66 insertions(+), 66 deletions(-) diff --git a/Test/civl/paxos/PaxosActions.bpl b/Test/civl/paxos/PaxosActions.bpl index b7200b952..b1b29b8e5 100644 --- a/Test/civl/paxos/PaxosActions.bpl +++ b/Test/civl/paxos/PaxosActions.bpl @@ -20,6 +20,23 @@ asserts Round(r); call {:linear joinPermissions} create_asyncs(JoinPAs(r)); } +async atomic action {:layer 2} A_Join(r: Round, n: Node, {:linear_in} p: One Permission) +modifies joinedNodes; +{ + assert Round(r); + assert p->val == JoinPerm(r, n); + + assume + {:add_to_pool "Round", r, r-1} + {:add_to_pool "Node", n} + true; + + if (*) { + assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' < r); + joinedNodes[r][n] := true; + } +} + async atomic action {:layer 2} A_Propose(r: Round, {:linear_in} ps: Set Permission) creates A_Vote, A_Conclude; modifies voteInfo; @@ -56,29 +73,14 @@ asserts voteInfo[r] is None; } } -async atomic action {:layer 2} A_Conclude(r: Round, v: Value, {:linear_in} p: One Permission) -modifies decision; +async atomic action {:layer 2} A_Vote(r: Round, n: Node, v: Value, {:linear_in} p: One Permission) +modifies joinedNodes, voteInfo; { - var {:pool "NodeSet"} q: NodeSet; - assert Round(r); - assert p->val == ConcludePerm(r); + assert p->val == VotePerm(r, n); assert voteInfo[r] is Some; assert voteInfo[r]->t->value == v; - - assume {:add_to_pool "Round", r} {:add_to_pool "NodeSet", q} true; - - if (*) { - assume IsSubset(q, voteInfo[r]->t->ns) && IsQuorum(q); - decision[r] := Some(v); - } -} - -async atomic action {:layer 2} A_Join(r: Round, n: Node, {:linear_in} p: One Permission) -modifies joinedNodes; -{ - assert Round(r); - assert p->val == JoinPerm(r, n); + assert !voteInfo[r]->t->ns[n]; assume {:add_to_pool "Round", r, r-1} @@ -86,29 +88,27 @@ modifies joinedNodes; true; if (*) { - assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' < r); + assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' <= r); + voteInfo[r] := Some(VoteInfo(v, voteInfo[r]->t->ns[n := true])); joinedNodes[r][n] := true; } } -async atomic action {:layer 2} A_Vote(r: Round, n: Node, v: Value, {:linear_in} p: One Permission) -modifies joinedNodes, voteInfo; +async atomic action {:layer 2} A_Conclude(r: Round, v: Value, {:linear_in} p: One Permission) +modifies decision; { + var {:pool "NodeSet"} q: NodeSet; + assert Round(r); - assert p->val == VotePerm(r, n); + assert p->val == ConcludePerm(r); assert voteInfo[r] is Some; assert voteInfo[r]->t->value == v; - assert !voteInfo[r]->t->ns[n]; - assume - {:add_to_pool "Round", r, r-1} - {:add_to_pool "Node", n} - true; + assume {:add_to_pool "Round", r} {:add_to_pool "NodeSet", q} true; if (*) { - assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' <= r); - voteInfo[r] := Some(VoteInfo(v, voteInfo[r]->t->ns[n := true])); - joinedNodes[r][n] := true; + assume IsSubset(q, voteInfo[r]->t->ns) && IsQuorum(q); + decision[r] := Some(v); } } diff --git a/Test/civl/paxos/PaxosImpl.bpl b/Test/civl/paxos/PaxosImpl.bpl index 33631e9ab..0b4ecb290 100644 --- a/Test/civl/paxos/PaxosImpl.bpl +++ b/Test/civl/paxos/PaxosImpl.bpl @@ -121,6 +121,24 @@ requires call YieldInvChannels(); async call Propose(r, ps'); } +yield procedure {:layer 1} +Join(r: Round, n: Node, {:layer 1}{:linear_in} p: One Permission) +refines A_Join; +requires {:layer 1} Round(r) && Node(n) && p->val == JoinPerm(r, n); +requires call YieldInv(); +{ + var doJoin: bool; + var lastVoteRound: Round; + var lastVoteValue: Value; + + call doJoin, lastVoteRound, lastVoteValue := JoinUpdate(r, n); + if (doJoin) { + call SendJoinResponse(r, n, lastVoteRound, lastVoteValue); + call {:layer 1} permJoinChannel := SendJoinResponseIntro(JoinResponse(n, lastVoteRound, lastVoteValue), p, permJoinChannel); + call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]); + } +} + yield right procedure {:layer 1} ProposeHelper(r: Round) returns (maxRound: Round, maxValue: Value, {:layer 1} ns: NodeSet) modifies permJoinChannel, joinChannel; requires {:layer 1} Round(r); @@ -201,6 +219,23 @@ requires call YieldInvChannels(); call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(maxValue, NoNodes()))]); } +yield procedure {:layer 1} +Vote(r: Round, n: Node, v: Value, {:layer 1}{:linear_in} p: One Permission) +refines A_Vote; +requires {:layer 1} Round(r) && Node(n) && p->val == VotePerm(r, n); +requires call YieldInv(); +{ + var doVote:bool; + + call doVote := VoteUpdate(r, n, v); + if (doVote) { + call SendVoteResponse(r, n); + call {:layer 1} permVoteChannel := SendVoteResponseIntro(VoteResponse(n), p, permVoteChannel); + call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]); + call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(voteInfo[r]->t->value, voteInfo[r]->t->ns[n := true]))]); + } +} + yield procedure {:layer 1} Conclude(r: Round, v: Value, {:layer 1}{:linear_in} p: One Permission) refines A_Conclude; @@ -238,41 +273,6 @@ requires call YieldInvChannels(); } } -yield procedure {:layer 1} -Join(r: Round, n: Node, {:layer 1}{:linear_in} p: One Permission) -refines A_Join; -requires {:layer 1} Round(r) && Node(n) && p->val == JoinPerm(r, n); -requires call YieldInv(); -{ - var doJoin: bool; - var lastVoteRound: Round; - var lastVoteValue: Value; - - call doJoin, lastVoteRound, lastVoteValue := JoinUpdate(r, n); - if (doJoin) { - call SendJoinResponse(r, n, lastVoteRound, lastVoteValue); - call {:layer 1} permJoinChannel := SendJoinResponseIntro(JoinResponse(n, lastVoteRound, lastVoteValue), p, permJoinChannel); - call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]); - } -} - -yield procedure {:layer 1} -Vote(r: Round, n: Node, v: Value, {:layer 1}{:linear_in} p: One Permission) -refines A_Vote; -requires {:layer 1} Round(r) && Node(n) && p->val == VotePerm(r, n); -requires call YieldInv(); -{ - var doVote:bool; - - call doVote := VoteUpdate(r, n, v); - if (doVote) { - call SendVoteResponse(r, n); - call {:layer 1} permVoteChannel := SendVoteResponseIntro(VoteResponse(n), p, permVoteChannel); - call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]); - call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(voteInfo[r]->t->value, voteInfo[r]->t->ns[n := true]))]); - } -} - //////////////////////////////////////////////////////////////////////////////// // Trusted lemmas for the proof of Propose and Conclude