Created
September 22, 2022 01:17
-
-
Save thalesmg/3db6766585e2092fe05920d3c6f861cc to your computer and use it in GitHub Desktop.
Simple two-phase commit in Alloy 6
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
<?xml version="1.0"?> | |
<alloy> | |
<view> | |
<defaultnode/> | |
<defaultedge/> | |
<node> | |
<type name="Int"/> | |
<type name="Node"/> | |
<type name="Nope"/> | |
<type name="String"/> | |
<type name="univ"/> | |
<type name="Yep"/> | |
<type name="ordering/Ord"/> | |
<type name="seq/Int"/> | |
</node> | |
<node showlabel="no" shape="Dbl Octagon" color="Red"> | |
<set name="this/TransactionCoordinator" type="Node"/> | |
</node> | |
<node style="Dashed" shape="Circle" color="Green"> | |
<type name="Value"/> | |
</node> | |
<node visible="no" shape="Inv Triangle" color="Gray"> | |
<type name="Vote"/> | |
</node> | |
<edge attribute="yes"> | |
<relation name="proposed"> <type name="Node"/> <type name="Value"/> </relation> | |
</edge> | |
<edge visible="no" attribute="yes"> | |
<relation name="proposals_sent"> <type name="Node"/> <type name="Node"/> </relation> | |
<relation name="responses_recv"> <type name="Node"/> <type name="Vote"/> <type name="Node"/> </relation> | |
</edge> | |
</view> | |
</alloy> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module twophasecommit_ideal | |
sig Value {} | |
/* abstract sig Vote {} */ | |
/* one sig Yep extends Vote {} */ | |
/* one sig Nope extends Vote {} */ | |
enum Vote {Yep, Nope} | |
sig Node { | |
var val: one Value, | |
var proposed: lone Value, | |
var voted: lone Vote | |
} | |
one sig TransactionCoordinator in Node { | |
var proposals_sent: set Node, | |
var responses_recv: Vote -> Node | |
} | |
fact init { | |
no proposed | |
no proposals_sent | |
no voted | |
no responses_recv | |
} | |
pred stutter { | |
val' = val | |
proposed' = proposed | |
proposals_sent' = proposals_sent | |
voted' = voted | |
responses_recv' = responses_recv | |
} | |
pred send_proposal[tc: TransactionCoordinator, v: Value, n : Node] { | |
// precondition: this node did not receive a proposal yet | |
n not in tc.proposals_sent | |
// effect | |
tc.val = v | |
tc.proposed' = v | |
tc.proposals_sent' = tc.proposals_sent + n | |
proposed' = proposed + n->v | |
// frame conditions | |
val' = val | |
voted' = voted | |
responses_recv' = responses_recv | |
} | |
pred send_response[tc: TransactionCoordinator, vote: Vote, n : Node] { | |
// preconditions | |
no n.voted | |
some n.proposed | |
// effect | |
n.voted' = vote | |
tc.responses_recv' = tc.responses_recv + vote->n | |
// frame conditions | |
val' = val | |
proposed' = proposed | |
proposals_sent' = proposals_sent | |
all m : Node - n | m.voted' = m.voted | |
} | |
pred send_decision_abort[tc: TransactionCoordinator, n: Node] { | |
// preconditions | |
all m : Node | some tc.responses_recv.m | |
some m : Node | tc.responses_recv.m = Nope | |
// effect | |
val' = val | |
proposed' = proposed - n->Value | |
// frame conditions | |
voted' = voted | |
proposals_sent' = proposals_sent | |
responses_recv' = responses_recv | |
} | |
pred send_decision_commit[tc: TransactionCoordinator, n: Node] { | |
// preconditions | |
all m : Node | tc.responses_recv.m = Yep | |
some n.proposed | |
// effect | |
n.val' = n.proposed | |
all m : Node - n | { | |
m.val' = m.val | |
} | |
proposed' = proposed - n->Value | |
// frame conditions | |
voted' = voted | |
proposals_sent' = proposals_sent | |
responses_recv' = responses_recv | |
} | |
fact step { | |
always ( | |
stutter or | |
(some v: Value, n : Node, tc: TransactionCoordinator | | |
send_proposal[tc, v, n]) or | |
(some vote: Vote, n : Node, tc: TransactionCoordinator | | |
send_response[tc, vote, n]) or | |
(some n: Node, tc: TransactionCoordinator | | |
send_decision_abort[tc, n]) or | |
(some n: Node, tc: TransactionCoordinator | | |
send_decision_commit[tc, n]) | |
) | |
} | |
pred fairness { | |
all tc: TransactionCoordinator, n: Node | { | |
(eventually historically (n not in tc.proposals_sent)) | |
=> (eventually some v: Value, tc: TransactionCoordinator | | |
send_proposal[tc, v, n]) | |
(eventually always (n in tc.proposals_sent)) | |
=> (eventually some v: Vote, tc: TransactionCoordinator | | |
send_response[tc, v, n]) | |
(eventually always (n in Vote.(tc.responses_recv))) | |
=> (eventually some tc: TransactionCoordinator | | |
(send_decision_abort[tc, n] or send_decision_commit[tc, n])) | |
} | |
} | |
pred ReachesConclusion { | |
Node = TransactionCoordinator.proposals_sent | |
all m : Node | some TransactionCoordinator.responses_recv.m | |
no proposed | |
} | |
pred Commited { | |
ReachesConclusion | |
all m : Node | m.voted = Yep | |
} | |
assert ReachesConclusion0 { | |
eventually ReachesConclusion | |
} | |
assert ReachesConclusion { | |
fairness => eventually ReachesConclusion | |
} | |
assert CommitMeansAgreement { | |
Commited => all disj n1, n2 : Node | n1.val = n2.val | |
} | |
check ReachesConclusion0 for 3 but 1..15 steps | |
check ReachesConclusion for 3 but 1..15 steps | |
check CommitMeansAgreement for 3 but 1..15 steps | |
run example0 { | |
#Node > 1 | |
} | |
run example { | |
#Node > 1 | |
eventually ReachesConclusion | |
} | |
run same_votes { | |
#Node > 1 | |
eventually (all n : Node | some v : Vote | TransactionCoordinator.responses_recv.n = v) | |
} | |
run commit_example { | |
#Node > 1 | |
eventually { | |
ReachesConclusion | |
all m : Node | m.voted = Yep | |
} | |
} | |
run abort_example { | |
#Node > 1 | |
eventually { | |
ReachesConclusion | |
some m : Node | m.voted = Nope | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment