diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs index 68ba9aa91..a5585fd27 100644 --- a/Source/Concurrency/InductiveSequentialization.cs +++ b/Source/Concurrency/InductiveSequentialization.cs @@ -182,7 +182,6 @@ private Cmd Transform(Dictionary eliminatedPendingAsyn public class InductiveSequentialization : Sequentialization { private Action invariantAction; - private HashSet frame; private IdentifierExpr choice; private Dictionary newPAs; @@ -193,7 +192,6 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target // - the modified set of each of each eliminated and abstract action associated with this invariant. // - the target and refined action of every application of inductive sequentialization that refers to this invariant. this.invariantAction = invariantAction; - frame = new HashSet(invariantAction.ModifiedGlobalVars); choice = Expr.Ident(invariantAction.ImplWithChoice.OutParams.Last()); newPAs = invariantAction.PendingAsyncs.ToDictionary(decl => decl.PendingAsyncType, decl => (Variable)civlTypeChecker.LocalVariable($"newPAs_{decl.Name}", decl.PendingAsyncMultisetType)); @@ -202,7 +200,7 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target private List GenerateBaseCaseChecker() { var requires = invariantAction.Gate.Select(g => new Requires(false, g.Expr)).ToList(); - + var subst = targetAction.GetSubstitution(invariantAction); var cmds = targetAction.GetGateAsserts(subst, $"Gate of {targetAction.Name} fails in IS base check against invariant {invariantAction.Name}").ToList(); @@ -215,7 +213,7 @@ private List GenerateBaseCaseChecker() outputVars.AddRange(targetAction.PendingAsyncs.Select(action => invariantAction.Impl.OutParams[pendingAsyncTypeToOutputParamIndex[action.PendingAsyncType]])); cmds.Add(CmdHelper.CallCmd(targetAction.Impl.Proc, invariantAction.Impl.InParams, outputVars)); - + // Assign empty multiset to the rest var remainderPendingAsyncs = invariantAction.PendingAsyncs.Except(targetAction.PendingAsyncs); if (remainderPendingAsyncs.Any()) @@ -228,6 +226,7 @@ private List GenerateBaseCaseChecker() cmds.Add(CmdHelper.AssignCmd(lhss, rhss)); } + var frame = new HashSet(invariantAction.ModifiedGlobalVars); cmds.Add(GetCheck(targetAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame), $"IS base of {targetAction.Name} failed")); @@ -246,6 +245,7 @@ private List GenerateConclusionChecker() cmds.Add(CmdHelper.CallCmd(invariantAction.Impl.Proc, invariantAction.Impl.InParams, invariantAction.Impl.OutParams)); cmds.Add(CmdHelper.AssumeCmd(NoPendingAsyncs)); + var frame = new HashSet(refinedAction.ModifiedGlobalVars); cmds.Add(GetCheck(targetAction.tok, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)), $"IS conclusion of {targetAction.Name} failed")); @@ -300,6 +300,7 @@ private List GenerateStepChecker(Action pendingAsync) cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); } + var frame = new HashSet(invariantAction.ModifiedGlobalVars); cmds.Add(GetCheck(invariantAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame), $"IS step of {invariantAction.Name} with {abs.Name} failed")); @@ -315,7 +316,7 @@ private List GenerateStepChecker(Action pendingAsync) * A key concept used in the generation of this extra assumption is the input-output transition relation of an action. * This relation is obtained by taking the conjunction of the gate and transition relation of the action and * existentially quantifying globals in the pre and the post state. - * + * * There are two parts to the assumption, one for leftMover and the other for action. * Both parts are stated in the context of the input-output relation of the invariant action. * - The invocation of leftMover is identical to the choice made by the invariant. @@ -427,7 +428,7 @@ private List GetCheckerTuple(string checkerName, List req inParams, outParams, requires, - frame.Select(Expr.Ident).ToList(), + invariantAction.ModifiedGlobalVars.Select(Expr.Ident).ToList(), new List()); var impl = DeclHelper.Implementation( proc, @@ -457,7 +458,7 @@ private Expr ChoiceTest(CtorType pendingAsyncType) { return ExprHelper.IsConstructor(choice, invariantAction.ChoiceConstructor(pendingAsyncType).Name); } - + private Expr NoPendingAsyncs { get @@ -468,7 +469,7 @@ private Expr NoPendingAsyncs return expr; } } - + private AssignCmd RemoveChoice(CtorType pendingAsyncType) { var rhs = Expr.Sub(Expr.Select(PAs(pendingAsyncType), Choice(pendingAsyncType)), Expr.Literal(1)); diff --git a/Test/civl/inductive-sequentialization/paxos/Paxos.bpl b/Test/civl/inductive-sequentialization/paxos/Paxos.bpl index b5feeac3d..43cb52d39 100644 --- a/Test/civl/inductive-sequentialization/paxos/Paxos.bpl +++ b/Test/civl/inductive-sequentialization/paxos/Paxos.bpl @@ -90,8 +90,8 @@ function {:inline} VotePAs(r: Round, v: Value) : [A_Vote]bool //////////////////////////////////////////////////////////////////////////////// //// Global variables // Abstract -var {:layer 1,3} joinedNodes: [Round]NodeSet; -var {:layer 1,3} voteInfo: [Round]Option VoteInfo; +var {:layer 1,2} joinedNodes: [Round]NodeSet; +var {:layer 1,2} voteInfo: [Round]Option VoteInfo; var {:layer 1,3} decision: [Round]Option Value; // spec // Concrete @@ -106,9 +106,10 @@ var {:layer 1,1} {:linear "perm"} permVoteChannel: VoteResponseChannel; //////////////////////////////////////////////////////////////////////////////// function {:inline} Init ( - rs: [Round]bool) : bool + rs: [Round]bool, decision: [Round]Option Value) : bool { - rs == (lambda r: Round :: true) + rs == (lambda r: Round :: true) && + decision == (lambda r: Round :: None()) } function {:inline} InitLow ( diff --git a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl index 664592ab8..2fded11eb 100644 --- a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl +++ b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl @@ -56,7 +56,7 @@ function InvChannels (joinChannel: [Round][JoinResponse]int, permJoinChannel: Jo } yield invariant {:layer 1} YieldInit({:linear "perm"} rs: [Round]bool); -invariant Init(rs); +invariant Init(rs, decision); invariant InitLow(acceptorState, joinChannel, voteChannel, permJoinChannel, permVoteChannel); yield invariant {:layer 1} YieldInv(); diff --git a/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl b/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl index a290e358e..acbed721c 100644 --- a/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl +++ b/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl @@ -4,22 +4,21 @@ refines A_Paxos' using INV; creates A_StartRound; { var {:pool "NumRounds"} numRounds: int; - assert Init(rs); + assert Init(rs, decision); assume {:add_to_pool "Round", 0, numRounds} {:add_to_pool "NumRounds", numRounds} 0 <= numRounds; joinedNodes := (lambda r: Round:: NoNodes()); voteInfo := (lambda r: Round:: None()); - decision := (lambda r: Round:: None()); call create_asyncs((lambda pa: A_StartRound :: pa->r == pa->r_lin && Round(pa->r) && pa->r <= numRounds)); } atomic action {:layer 3} A_Paxos'({:linear_in "perm"} rs: [Round]bool) -modifies joinedNodes, voteInfo, decision; +modifies decision; { - assert Init(rs); - havoc joinedNodes, voteInfo, decision; + assert Init(rs, decision); + havoc decision; assume (forall r1: Round, r2: Round :: decision[r1] is Some && decision[r2] is Some ==> decision[r1] == decision[r2]); } @@ -32,7 +31,7 @@ modifies joinedNodes, voteInfo, decision; var {:pool "Round"} k: int; var {:pool "Node"} m: Node; - assert Init(rs); + assert Init(rs, decision); havoc joinedNodes, voteInfo, decision; diff --git a/Test/civl/inductive-sequentialization/paxos/is.sh.expect b/Test/civl/inductive-sequentialization/paxos/is.sh.expect index 65d6dd918..773f14960 100644 --- a/Test/civl/inductive-sequentialization/paxos/is.sh.expect +++ b/Test/civl/inductive-sequentialization/paxos/is.sh.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 72 verified, 0 errors +Boogie program verifier finished with 73 verified, 0 errors