Skip to content

Commit

Permalink
cleanup example for tutorial
Browse files Browse the repository at this point in the history
  • Loading branch information
@FedericoAureliano
FedericoAureliano committed Nov 28, 2024
1 parent 92a01ed commit 45f5269
Show file tree
Hide file tree
Showing 4 changed files with 64 additions and 183 deletions.
10 changes: 5 additions & 5 deletions Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1108,7 +1108,7 @@ private void
{
EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};");
EmitLine(
$"invariant _{InvariantPrefix}{inv.Name}: {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} globally");
$"invariant _{InvariantPrefix}{inv.Name}: {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} globally");
}

EmitLine("");
Expand Down Expand Up @@ -1357,7 +1357,7 @@ private void GenerateEntryHandler(State s, List<Invariant> goals, List<Invariant
{
EmitLine($"\trequires {InvariantPrefix}{inv.Name}();");
EmitLine(
$"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(s)}");
$"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(s)}");
}

EmitLine("{");
Expand Down Expand Up @@ -1439,7 +1439,7 @@ private void GenerateEventHandler(State s, PEvent ev, List<Invariant> goals, Lis
{
EmitLine($"\trequires {InvariantPrefix}{inv.Name}();");
EmitLine(
$"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(handler)}");
$"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(handler)}");
}

switch (handler)
Expand Down Expand Up @@ -1739,7 +1739,7 @@ private void GenerateStmt(IPStmt stmt, Machine specMachine, List<Invariant> goal
foreach (var inv in goals)
{
EmitLine(
$"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(fstmt)}");
$"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}");
}

if (generateSanityChecks)
Expand Down Expand Up @@ -1788,7 +1788,7 @@ private void GenerateStmt(IPStmt stmt, Machine specMachine, List<Invariant> goal
foreach (var inv in goals)
{
EmitLine(
$"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name} at {GetLocation(fstmt)}");
$"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}");
}

EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions();");
Expand Down
104 changes: 59 additions & 45 deletions Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
enum Vote {YES, NO}
type tVoteResp = (source: machine, vote: Vote);
type tVoteResp = (source: machine);

event eVoteReq;
event eVoteResp: tVoteResp;
event eYes: tVoteResp;
event eNo: tVoteResp;
event eAbort;
event eCommit;

Expand All @@ -24,42 +24,43 @@ machine Coordinator
}

state WaitForResponses {
on eVoteResp do (resp: tVoteResp) {
on eYes do (resp: tVoteResp) {
var p: machine;

if (resp.vote == YES) {
yesVotes += (resp.source);

if (yesVotes == participants()) {
foreach (p in participants())
invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants();
invariant forall new (e: event) :: e is eCommit;
{
send p, eCommit;
}
goto Committed;
}

} else {
yesVotes += (resp.source);
if (yesVotes == participants()) {
foreach (p in participants())
invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants();
invariant forall new (e: event) :: e is eAbort;
invariant forall new (e: event) :: e is eCommit;
{
send p, eAbort;
send p, eCommit;
}
goto Aborted;
goto Committed;
}
}
on eNo do (resp: tVoteResp) {
var p: machine;
foreach (p in participants())
invariant forall new (e: event) :: forall (m: machine) :: e targets m ==> m in participants();
invariant forall new (e: event) :: e is eAbort;
{
send p, eAbort;
}
goto Aborted;
}
}

state Committed {ignore eVoteResp;}
state Aborted {ignore eVoteResp;}
state Committed {ignore eYes, eNo;}
state Aborted {ignore eYes, eNo;}
}

machine Participant {
start state Undecided {
on eVoteReq do {
send coordinator(), eVoteResp, (source = this, vote = preference(this));
if (preference(this)) {
send coordinator(), eYes, (source = this,);
} else {
send coordinator(), eNo, (source = this,);
}
}

on eCommit do {
Expand All @@ -78,35 +79,48 @@ machine Participant {
// using these to avoid initialization
pure participants(): set[machine];
pure coordinator(): machine;
pure preference(m: machine) : Vote;
pure preference(m: machine) : bool;

// assumptions about how the system is setup and the pure functions above
init forall (m: machine) :: m == coordinator() == m is Coordinator;
init forall (m: machine) :: m in participants() == m is Participant;

// making sure that our assumptions about pure functions are not pulled out from underneath us
invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator;
invariant participant_set: forall (m: machine) :: m in participants() == m is Participant;

// set all the fields to their default values
init forall (c: Coordinator) :: c.yesVotes == default(set[machine]);

// make sure we never get a message that we're not expecting
invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e;
invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e;
invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e;
invariant never_resp_to_participant: forall (e: event, p: Participant) :: e is eVoteResp && e targets p ==> !inflight e;
invariant never_resp_to_init: forall (e: event, c: Coordinator) :: e is eVoteResp && e targets c && c is Init ==> !inflight e;
invariant req_implies_not_init: forall (e: event, c: Coordinator) :: e is eVoteReq && c is Init ==> !inflight e;
// making sure that our assumptions about pure functions are not pulled out from underneath us
Lemma system_config {
invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator;
invariant participant_set: forall (m: machine) :: m in participants() == m is Participant;
invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e;
invariant never_abort_to_coordinator: forall (e: event) :: e is eAbort && e targets coordinator() ==> !inflight e;
invariant never_req_to_coordinator: forall (e: event) :: e is eVoteReq && e targets coordinator() ==> !inflight e;
invariant never_yes_to_participant: forall (e: event, p: Participant) :: e is eYes && e targets p ==> !inflight e;
invariant never_yes_to_init: forall (e: event, c: Coordinator) :: e is eYes && e targets c && c is Init ==> !inflight e;
invariant never_no_to_participant: forall (e: event, p: Participant) :: e is eNo && e targets p ==> !inflight e;
invariant never_no_to_init: forall (e: event, c: Coordinator) :: e is eNo && e targets c && c is Init ==> !inflight e;
invariant req_implies_not_init: forall (e: event, c: Coordinator) :: e is eVoteReq && c is Init ==> !inflight e;
}

// the main invariant we care about
invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2) == YES);
invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2));

// supporting invariants, based on the Kondo paper
invariant a1: forall (e: eVoteResp) :: inflight e ==> e.source in participants();
invariant a2: forall (e: eVoteResp) :: inflight e ==> e.vote == preference(e.source);
invariant a3b: forall (e: eAbort) :: inflight e ==> coordinator() is Aborted;
invariant a3a: forall (e: eCommit) :: inflight e ==> coordinator() is Committed;
invariant a4: forall (p: Participant) :: p is Accepted ==> coordinator() is Committed;
invariant a5: forall (p: Participant, c: Coordinator) :: p in c.yesVotes ==> preference(p) == YES;
invariant a6: coordinator() is Committed ==> (forall (p: Participant) :: p in participants() ==> preference(p) == YES);
Lemma kondo {
invariant a1a: forall (e: eYes) :: inflight e ==> e.source in participants();
invariant a1b: forall (e: eNo) :: inflight e ==> e.source in participants();
invariant a2a: forall (e: eYes) :: inflight e ==> preference(e.source);
invariant a2b: forall (e: eNo) :: inflight e ==> !preference(e.source);
invariant a3b: forall (e: eAbort) :: inflight e ==> coordinator() is Aborted;
invariant a3a: forall (e: eCommit) :: inflight e ==> coordinator() is Committed;
invariant a4: forall (p: Participant) :: p is Accepted ==> coordinator() is Committed;
invariant a5: forall (p: Participant, c: Coordinator) :: p in c.yesVotes ==> preference(p);
invariant a6: coordinator() is Committed ==> (forall (p: Participant) :: p in participants() ==> preference(p));
}

Proof {
prove system_config;
prove kondo using system_config;
prove safety using kondo;
prove default using system_config;
}
125 changes: 0 additions & 125 deletions Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p
View file

This file was deleted.

8 changes: 0 additions & 8 deletions Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/TwoPhaseCommitVerification.pproj
View file

This file was deleted.

0 comments on commit 45f5269

Please sign in to comment.