Skip to content

Commit 9a0d78f

Browse files
shazqadeershazqadeer
committed
cleanup
1 parent 09b98b7 commit 9a0d78f

File tree

2 files changed

+106
-103
lines changed

2 files changed

+106
-103
lines changed

‎Test/civl/samples/2pc-parallel.bpl‎

Lines changed: 104 additions & 103 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,32 @@
1-
// Running the file: boogie 2pc-parallel.bpl /keepQuantifier
1+
/// RUN: %parallel-boogie "%s" > "%t"
2+
// RUN: %diff "%s.expect" "%t"
23

34
/*
45
2pc protocol:
5-
A transaction needs to be executed at every replica. Every replica executes each step of the transaction but does not mark the transaction as complete until the coordinator runs the 2pc protocol to collectively decide whether to commit or abort the transaction. There are two phases in the protocol. In the first phase, the coordinator sends vote requests to all replicas. The replicas then send a reply (yes/no) to the coordinator. If all replies are yes, then the coordinator sends a commit decision to all replicas, otherwise it sends an abort decision. After receiving the decision from the coordinator, the transaction is marked as complete at each replica if it was a commit decision, or cancelled if it was an abort decision.
6+
A transaction needs to be executed at every replica. Every replica executes each step of the transaction
7+
but does not mark the transaction as complete until the coordinator runs the 2pc protocol to collectively
8+
decide whether to commit or abort the transaction.
69
7-
Model proved below:
8-
Let's say there are multiple transactions at each replica that are marked as incomplete. It is now the coordinator's job to start the 2pc protocol for all of these transactions, and it does so concurrently. The goal is that we don't ever commit conflicting transactions because we can't control the order in which these transactions are applied at each replica. If conflicting transactions are committed, the data may no longer be same across all replicas.
10+
There are two phases in the protocol. In the first phase, the coordinator sends vote requests to all replicas.
11+
The replicas then send a reply (yes/no) to the coordinator. If all replies are yes, then the coordinator sends
12+
a commit decision to all replicas, otherwise it sends an abort decision. After receiving the decision from the
13+
coordinator, the transaction is marked as complete at each replica if it was a commit decision, or cancelled
14+
if it was an abort decision.
915
10-
Proof obligation: We have a ghost variable, committed_transactions, which keeps track of all transactions that have been committed so far. Before adding a transaction to this set, we assert that the transaction being added does not conflict with any previously committed transactions. If this assertion is shown to hold in all executions of the protocol, it should imply that we never commit conflicting transactions.
16+
Model proved below:
17+
Let's say there are multiple transactions at each replica that are marked as incomplete. Then multiple instances
18+
of the coordinator may be running concurrently, each executing the 2pc protocol one transaction.
19+
The goal is to ensure that we don't ever commit conflicting transactions; this condition is used to
20+
abstractly model consistency of committed transactions.
21+
We model the conflict relation between transactions using a 2-d array Conflict with axioms.
22+
23+
Proof obligation:
24+
We have a ghost variable, committed_transactions, which keeps track of all transactions that have been committed so far.
25+
Before adding a transaction to this set, we assert that the transaction being added does not conflict with any previously
26+
committed transactions. If this assertion is shown to hold in all executions of the protocol, it should imply that
27+
we never commit conflicting transactions.
1128
*/
1229

13-
14-
1530
type TransactionId;
1631
type ReplicaId = int;
1732

@@ -29,36 +44,59 @@ axiom (forall xid0: TransactionId :: Conflict[xid0][xid0] == true);
2944
var {:layer 0,1} locked_transactions: [ReplicaId](Set TransactionId);
3045
var {:layer 0,1} committed_transactions: Set TransactionId;
3146

32-
function noConflicts(xids: (Set TransactionId), xid: TransactionId) : bool {
47+
function noConflicts(xids: (Set TransactionId), xid: TransactionId) : bool
48+
{
3349
!(exists x: TransactionId :: Set_Contains(xids, x) && Conflict[x][xid])
3450
}
3551

36-
function allVoteRequests(xid: TransactionId) : Set VoteRequest {
52+
function allVoteRequests(xid: TransactionId) : Set VoteRequest
53+
{
3754
Set((lambda vr:VoteRequest :: vr->xid == xid && 1 <= vr->rid && vr->rid < n+1))
3855
}
3956

40-
function remainingVoteRequests(xid: TransactionId, i:int) : Set VoteRequest {
57+
function remainingVoteRequests(xid: TransactionId, i:int) : Set VoteRequest
58+
{
4159
Set((lambda vr:VoteRequest :: vr->xid == xid && i <= vr->rid && vr->rid < n+1))
4260
}
4361

44-
right action {:layer 1, 1} voting_action ( {:linear} vr: One VoteRequest) returns (result : Vote)
62+
yield procedure {:layer 1} TPC({:linear} xid: One TransactionId, {:linear_in} vrs: (Set VoteRequest))
63+
requires {:layer 1} vrs == allVoteRequests(xid->val);
64+
requires call LockedNoConflicts();
65+
requires call CommittedSubsetLocked();
66+
requires call XidNotInCommitted(xid);
4567
{
46-
if(*) {
47-
result := NO();
48-
}
49-
else {
50-
if(noConflicts(locked_transactions[vr->val->rid], vr->val->xid)) {
51-
locked_transactions[vr->val->rid] := Set_Add(locked_transactions[vr->val->rid], vr->val->xid);
52-
result := YES();
53-
}
54-
else {
55-
result := NO();
68+
var d: Decision;
69+
var votes: [ReplicaId]Vote;
70+
var {:linear} vrs': Set VoteRequest;
71+
var i: int;
72+
73+
d := COMMIT();
74+
vrs' := vrs;
75+
76+
call votes, vrs' := voting_loop_yield_procedure(xid->val, vrs', n);
77+
78+
i := 1;
79+
while (i <= n)
80+
invariant {:layer 1} (forall {:pool "J"} j:int :: {:add_to_pool "J", j} 1 <= j && j < i ==> (d == COMMIT() ==> (votes[j] == YES())));
81+
{
82+
if (votes[i] == NO())
83+
{
84+
d := ABORT();
5685
}
86+
i := i+1;
5787
}
58-
}
5988

60-
yield procedure {:layer 0} voting_procedure ({:linear} vr: One VoteRequest) returns (result : Vote);
61-
refines voting_action;
89+
call finalize_loop_yield_procedure(d, xid, vrs');
90+
91+
if (d == COMMIT())
92+
{
93+
par LockedNoConflicts() | CommittedSubsetLocked() | XidNotInCommitted(xid) | XidInLocked(xid);
94+
95+
assume {:add_to_pool "J", 1} true;
96+
97+
call add_to_committed_transactions_procedure(xid);
98+
}
99+
}
62100

63101
yield right procedure {:layer 1} voting_loop_yield_procedure(xid: TransactionId, {:linear_in} vrs: Set VoteRequest, i: int) returns (votes: [ReplicaId]Vote, {:linear} vrs': Set VoteRequest)
64102
requires {:layer 1} vrs == Set((lambda vr:VoteRequest :: vr->xid == xid && 1 <= vr->rid && vr->rid < i+1));
@@ -70,54 +108,22 @@ ensures {:layer 1} (forall j:int :: 1 <= j && j < n+1 ==> IsSubset(old(locked_tr
70108
ensures {:layer 1} (forall j:int :: 1 <= j && j < i+1 ==> votes[j] != NONE());
71109
modifies locked_transactions;
72110
{
73-
// var i: int;
74111
var {:linear} vr: One VoteRequest;
75112
var out: Vote;
76-
vrs' := vrs;
77-
// i := 1;
78-
// while( i<=n )
79-
// invariant {:layer 1} (forall j:int :: 1 <= j && j < i && replica_votes[VoteRequest(xid, j)] == YES() ==> Set_Contains(locked_transactions[j], xid));
80-
// invariant {:layer 1} IsSubset(remainingVoteRequests(xid, i)->val, vrs'->val);
81-
// invariant {:layer 1} vrs' == allVoteRequests(xid);
82-
// invariant {:layer 1} (forall j:int, xid1: TransactionId, xid2: TransactionId :: (1 <= j && j < n+1 && xid1 != xid2 && Set_Contains(locked_transactions[j], xid1) && Set_Contains(locked_transactions[j], xid2)) ==> !Conflict[xid1][xid2]);
83-
// invariant {:layer 1} (forall j:int, xid0: TransactionId :: 1 <= j && j < n+1 && Set_Contains(committed_transactions, xid0) ==> Set_Contains(locked_transactions[j], xid0));
84-
// invariant {:layer 1} (forall j:int :: 1 <=j && j < n+1 ==> IsSubset(old(locked_transactions)[j]->val, locked_transactions[j]->val));
85-
// invariant {:layer 1} (forall j:int :: 1 <= j && j < i ==> replica_votes[VoteRequest(xid, j)] != NONE());
86-
// {
87-
// call vr := One_Get(vrs', VoteRequest(xid, i));
88-
// call voting_procedure(vr);
89-
// i := i + 1;
90-
// call One_Put(vrs', vr);
91-
92-
if(1 <= i)
93-
{
94-
call vr := One_Get(vrs', VoteRequest(xid, i));
95-
par votes, vrs' := voting_loop_yield_procedure(xid, vrs', i-1) | out := voting_procedure(vr);
96-
votes[i] := out;
97-
call One_Put(vrs', vr);
98-
}
99-
// }
100-
}
101113

102-
left action {:layer 1, 1} finalize_action (d: Decision, {:linear} vr: One VoteRequest)
103-
{
104-
if(d == COMMIT())
105-
{
106-
107-
}
108-
else
114+
vrs' := vrs;
115+
if (1 <= i)
109116
{
110-
locked_transactions[vr->val->rid] := Set_Remove(locked_transactions[vr->val->rid], vr->val->xid);
117+
call vr := One_Get(vrs', VoteRequest(xid, i));
118+
par votes, vrs' := voting_loop_yield_procedure(xid, vrs', i-1) | out := voting_procedure(vr);
119+
votes[i] := out;
120+
call One_Put(vrs', vr);
111121
}
112122
}
113123

114-
115-
yield procedure {:layer 0} finalize_procedure (d: Decision, {:linear} vr: One VoteRequest);
116-
refines finalize_action;
117-
118124
yield left procedure {:layer 1} finalize_loop_yield_procedure(d: Decision, {:linear} xid: One TransactionId, {:linear_in} vrs: Set VoteRequest)
119125
requires {:layer 1} vrs == allVoteRequests(xid->val);
120-
requires {:layer 1} (forall j:int :: d == COMMIT() && 1 <= j && j < n+1 ==> Set_Contains(locked_transactions[j], xid->val));
126+
requires {:layer 1} (forall j:int :: {:add_to_pool "J", j} d == COMMIT() && 1 <= j && j < n+1 ==> Set_Contains(locked_transactions[j], xid->val));
121127
ensures {:layer 1} (forall j:int :: d == COMMIT() && 1 <=j && j < n+1 ==> Set_Contains(locked_transactions[j], xid->val));
122128
preserves call LockedNoConflicts();
123129
preserves call CommittedSubsetLocked();
@@ -128,10 +134,11 @@ modifies locked_transactions;
128134
var i: int;
129135
var {:linear} vr: One VoteRequest;
130136
var {:linear} vrs': Set VoteRequest;
137+
131138
vrs' := vrs;
132139
i := 1;
133140

134-
while(i <= n)
141+
while (i <= n)
135142
invariant {:layer 1} (forall j:int :: d == COMMIT() && 1 <= j && j < i ==> Set_Contains(locked_transactions[j], xid->val));
136143
invariant {:layer 1} (forall j:int :: d == COMMIT() && (i <= j) && (j < n+1) ==> Set_Contains(locked_transactions[j], xid->val));
137144
invariant {:layer 1} vrs' == remainingVoteRequests(xid->val, i);
@@ -146,61 +153,55 @@ modifies locked_transactions;
146153
}
147154
}
148155

149-
atomic action {:layer 1, 1} add_to_committed_transactions({:linear} xid: One TransactionId){
150-
assert (forall xid0: TransactionId :: Set_Contains(committed_transactions, xid0) ==> !Conflict[xid0][xid->val]);
151-
committed_transactions := Set_Add(committed_transactions, xid->val);
152-
}
153-
154-
yield procedure {:layer 0} add_to_committed_transactions_procedure ({:linear} xid: One TransactionId);
155-
refines add_to_committed_transactions;
156-
157-
158-
yield procedure {:layer 1} TPC({:linear} xid: One TransactionId, {:linear_in} vrs: (Set VoteRequest))
159-
requires {:layer 1} vrs == allVoteRequests(xid->val);
160-
requires call LockedNoConflicts();
161-
requires call CommittedSubsetLocked();
162-
requires call XidNotInCommitted(xid);
156+
right action {:layer 1, 1} voting_action ( {:linear} vr: One VoteRequest) returns (result : Vote)
163157
{
164-
var d: Decision;
165-
var votes: [ReplicaId]Vote;
166-
var {:linear} vrs': Set VoteRequest;
167-
var i: int;
168-
d := COMMIT();
169-
vrs' := vrs;
170-
171-
call votes, vrs' := voting_loop_yield_procedure(xid->val, vrs', n);
172-
173-
i := 1;
174-
while(i <= n)
175-
invariant {:layer 1} (forall j:int :: 1 <= j && j < i ==> (d == COMMIT() ==> (votes[j] == YES())));
158+
if (*)
176159
{
177-
if(votes[i] == NO())
160+
result := NO();
161+
}
162+
else
163+
{
164+
if (noConflicts(locked_transactions[vr->val->rid], vr->val->xid))
178165
{
179-
d := ABORT();
166+
locked_transactions[vr->val->rid] := Set_Add(locked_transactions[vr->val->rid], vr->val->xid);
167+
result := YES();
168+
}
169+
else
170+
{
171+
result := NO();
180172
}
181-
i := i+1;
182173
}
174+
}
175+
yield procedure {:layer 0} voting_procedure ({:linear} vr: One VoteRequest) returns (result : Vote);
176+
refines voting_action;
183177

184-
call finalize_loop_yield_procedure(d, xid, vrs');
185-
186-
if (d == COMMIT())
178+
left action {:layer 1, 1} finalize_action (d: Decision, {:linear} vr: One VoteRequest)
179+
{
180+
if (d != COMMIT())
187181
{
188-
par LockedNoConflicts() | CommittedSubsetLocked() | XidNotInCommitted(xid) | XidInLocked(xid);
182+
locked_transactions[vr->val->rid] := Set_Remove(locked_transactions[vr->val->rid], vr->val->xid);
183+
}
184+
}
185+
yield procedure {:layer 0} finalize_procedure (d: Decision, {:linear} vr: One VoteRequest);
186+
refines finalize_action;
189187

190-
assume {:add_to_pool "J", 1} true;
191188

192-
call add_to_committed_transactions_procedure(xid);
193-
}
189+
atomic action {:layer 1, 1} add_to_committed_transactions({:linear} xid: One TransactionId)
190+
{
191+
assert (forall xid0: TransactionId :: Set_Contains(committed_transactions, xid0) ==> !Conflict[xid0][xid->val]);
192+
committed_transactions := Set_Add(committed_transactions, xid->val);
194193
}
194+
yield procedure {:layer 0} add_to_committed_transactions_procedure ({:linear} xid: One TransactionId);
195+
refines add_to_committed_transactions;
195196

196197
yield invariant {:layer 1} LockedNoConflicts();
197-
invariant {:layer 1} (forall {:pool "J"} j:int, xid1: TransactionId, xid2: TransactionId :: (1 <= j && j < n+1 && xid1 != xid2 && Set_Contains(locked_transactions[j], xid1) && Set_Contains(locked_transactions[j], xid2)) ==> !Conflict[xid1][xid2]);
198+
invariant {:layer 1} (forall {:pool "J"} j:int, xid1: TransactionId, xid2: TransactionId :: {:add_to_pool "J", j} (1 <= j && j < n+1 && xid1 != xid2 && Set_Contains(locked_transactions[j], xid1) && Set_Contains(locked_transactions[j], xid2)) ==> !Conflict[xid1][xid2]);
198199

199200
yield invariant {:layer 1} CommittedSubsetLocked();
200-
invariant {:layer 1} (forall {:pool "J"} j:int, xid0: TransactionId :: 1 <= j && j < n+1 && Set_Contains(committed_transactions, xid0) ==> Set_Contains(locked_transactions[j], xid0));
201+
invariant {:layer 1} (forall {:pool "J"} j:int, xid0: TransactionId :: {:add_to_pool "J", j} 1 <= j && j < n+1 && Set_Contains(committed_transactions, xid0) ==> Set_Contains(locked_transactions[j], xid0));
201202

202203
yield invariant {:layer 1} XidInLocked({:linear} xid: One TransactionId);
203-
invariant (forall {:pool "J"} j:int ::1 <=j && j < n+1 ==> Set_Contains(locked_transactions[j], xid->val));
204+
invariant (forall {:pool "J"} j:int :: {:add_to_pool "J", j} 1 <= j && j < n+1 ==> Set_Contains(locked_transactions[j], xid->val));
204205

205206
yield invariant {:layer 1} XidNotInCommitted({:linear} xid: One TransactionId);
206207
invariant !Set_Contains(committed_transactions, xid->val);

‎Test/civl/samples/2pc-parallel.bpl.expect‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
2+
Boogie program verifier finished with 7 verified, 0 errors

0 commit comments

Comments
 (0)