diff --git a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs index c4d8da17ba..982a2a3674 100644 --- a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs @@ -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(""); @@ -1357,7 +1357,7 @@ private void GenerateEntryHandler(State s, List goals, List 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) @@ -1739,7 +1739,7 @@ private void GenerateStmt(IPStmt stmt, Machine specMachine, List 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) @@ -1788,7 +1788,7 @@ private void GenerateStmt(IPStmt stmt, Machine specMachine, List 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();"); diff --git a/Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p index a6322795d3..d4e73c7d26 100644 --- a/Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p +++ b/Tutorial/6_TwoPhaseCommitVerification/Single/PSrc/System.p @@ -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; @@ -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 { @@ -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); \ No newline at end of file +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; +} \ No newline at end of file diff --git a/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p deleted file mode 100644 index ed63ebfe63..0000000000 --- a/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/PSrc/System.p +++ /dev/null @@ -1,125 +0,0 @@ -enum Vote {YES, NO} -type tVoteResp = (source: machine, vote: Vote); - -event eVoteReq; -event eVoteResp: tVoteResp; -event eAbort; -event eCommit; - -machine Coordinator -{ - var yesVotes: set[machine]; - - start state Init { - entry { - 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 eVoteReq; - { - send p, eVoteReq; - } - goto WaitForResponses; - } - } - - state WaitForResponses { - on eVoteResp 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 { - 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;} -} - -machine Participant { - start state Undecided { - on eVoteReq do { - send coordinator(), eVoteResp, (source = this, vote = preference(this)); - } - - on eCommit do { - goto Accepted; - } - - on eAbort do { - goto Rejected; - } - } - - state Accepted {ignore eVoteReq, eCommit, eAbort;} - state Rejected {ignore eVoteReq, eCommit, eAbort;} -} - -// using these to avoid initialization -pure participants(): set[machine]; -pure coordinator(): machine; -pure preference(m: machine) : Vote; - -// 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 -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; -} - -// 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 -Lemma no_unexpected_messages { - 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; -} - -// the main invariant we care about -invariant safety: forall (p1: Participant) :: p1 is Accepted ==> (forall (p2: Participant) :: preference(p2) == YES); - -// supporting invariants, based on the Kondo paper -Lemma kondo { - 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); -} - -Proof { - prove safety using kondo; - prove no_unexpected_messages, system_config; - prove kondo using no_unexpected_messages, system_config; - prove default using no_unexpected_messages, system_config; -} \ No newline at end of file diff --git a/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/TwoPhaseCommitVerification.pproj b/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/TwoPhaseCommitVerification.pproj deleted file mode 100644 index d60d0d2f7d..0000000000 --- a/Tutorial/6_TwoPhaseCommitVerification/Single_Incremental/TwoPhaseCommitVerification.pproj +++ /dev/null @@ -1,8 +0,0 @@ - -TwoPhaseCommitVerification - - ./PSrc/ - -./PGenerated/ -UCLID5 -