diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs index f5048d997..928693a2f 100644 --- a/Source/Concurrency/CivlCoreTypes.cs +++ b/Source/Concurrency/CivlCoreTypes.cs @@ -1,7 +1,6 @@ using System.Collections.Generic; using System.Diagnostics; using System.Linq; -using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie { @@ -171,7 +170,7 @@ private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeCh { if (ActionDecl.Asserts.Count == 0) { - Gate = HoistAsserts(Impl, civlTypeChecker.Options); + Gate = Wlp.HoistAsserts(Impl, civlTypeChecker.Options); return; } @@ -199,7 +198,7 @@ private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeCh proc.OutParams, proc.IsPure, requires, proc.Modifies, new List()); gateSufficiencyCheckerDecls.AddRange(new Declaration[] { checkerImpl.Proc, checkerImpl }); - HoistAsserts(Impl, civlTypeChecker.Options); + Wlp.HoistAsserts(Impl, civlTypeChecker.Options); Gate = ActionDecl.Asserts.Select( assertCmd => new AssertCmd(assertCmd.tok, Substituter.Apply(gateSubst, assertCmd.Expr), @@ -367,103 +366,7 @@ private void DesugarSetChoice(CivlTypeChecker civlTypeChecker, Implementation im block.Cmds = newCmds; }); } - - /* - * HoistAsserts computes the weakest liberal precondition (wlp) of the body - * of impl as a collection of AssertCmd's. As a side effect, all AssertCmd's - * in any block of impl are removed. - * - * HoistAsserts assumes that the body of impl does not contain any loops or - * calls. The blocks in impl are sorted from entry to exit and processed in - * reverse order, thus ensuring that a block is processed only once the wlp - * of all its successors has been computed. - */ - private List HoistAsserts(Implementation impl, ConcurrencyOptions options) - { - Dictionary> wlps = new Dictionary>(); - Graph dag = Program.GraphFromBlocks(impl.Blocks, false); - foreach (var block in dag.TopologicalSort()) - { - if (block.TransferCmd is ReturnCmd) - { - var wlp = HoistAsserts(block.Cmds, new List(), options); - wlps.Add(block, wlp); - } - else if (block.TransferCmd is GotoCmd gotoCmd) - { - var wlp = - HoistAsserts(block.Cmds, gotoCmd.LabelTargets.SelectMany(b => wlps[b]).ToList(), options); - wlps.Add(block, wlp); - } - else - { - throw new Cce.UnreachableException(); - } - } - return wlps[impl.Blocks[0]].Select(assertCmd => Forall(impl.LocVars.Union(impl.OutParams), assertCmd)).ToList(); - } - - private List HoistAsserts(List cmds, List postconditions, ConcurrencyOptions options) - { - for (int i = cmds.Count - 1; i >= 0; i--) - { - var cmd = cmds[i]; - if (cmd is AssertCmd assertCmd) - { - postconditions.Add(assertCmd); - } - else if (cmd is AssumeCmd assumeCmd) - { - postconditions = postconditions - .Select(assertCmd => new AssertCmd(assertCmd.tok, Expr.Imp(assumeCmd.Expr, assertCmd.Expr))).ToList(); - } - else if (cmd is AssignCmd assignCmd) - { - var varToExpr = new Dictionary(); - var simpleAssignCmd = assignCmd.AsSimpleAssignCmd; - for (var j = 0; j < simpleAssignCmd.Lhss.Count; j++) - { - var lhs = simpleAssignCmd.Lhss[j]; - var rhs = simpleAssignCmd.Rhss[j]; - varToExpr.Add(lhs.DeepAssignedVariable, rhs); - } - postconditions = postconditions.Select(assertCmd => - new AssertCmd(assertCmd.tok, SubstitutionHelper.Apply(varToExpr, assertCmd.Expr))).ToList(); - } - else if (cmd is HavocCmd havocCmd) - { - postconditions = postconditions.Select(assertCmd => Forall(havocCmd.Vars.Select(ie => ie.Decl), assertCmd)) - .ToList(); - } - else if (cmd is UnpackCmd unpackCmd) - { - var desugaredCmd = (StateCmd) unpackCmd.GetDesugaring(options); - postconditions = HoistAsserts(desugaredCmd.Cmds, postconditions, options); // removes precondition assert from desugaredCmd.Cmds - } - else - { - throw new Cce.UnreachableException(); - } - } - cmds.RemoveAll(cmd => cmd is AssertCmd); - return postconditions; - } - - private static AssertCmd Forall(IEnumerable vars, AssertCmd assertCmd) - { - var freeObjects = new GSet(); - assertCmd.Expr.ComputeFreeVariables(freeObjects); - var quantifiedVars = freeObjects.OfType().Intersect(vars); - if (quantifiedVars.Count() == 0) - { - return assertCmd; - } - var varMapping = quantifiedVars.ToDictionary(v => v, - v => (Variable) VarHelper.BoundVariable(v.Name, v.TypedIdent.Type)); - return new AssertCmd(assertCmd.tok, - ExprHelper.ForallExpr(varMapping.Values.ToList(), SubstitutionHelper.Apply(varMapping, assertCmd.Expr))); - } - + private void DeclareTriggerFunctions() { TriggerFunctions = new Dictionary(); diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs index e4c4355f2..726cbe0f3 100644 --- a/Source/Concurrency/CivlUtil.cs +++ b/Source/Concurrency/CivlUtil.cs @@ -344,9 +344,9 @@ public static LocalVariable LocalVariable(string name, Type type) return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, name, type)); } - public static BoundVariable BoundVariable(string name, Type type) + public static BoundVariable BoundVariable(string name, Type type, QKeyValue kv = null) { - return new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, name, type)); + return new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, name, type), kv); } public static Formal Formal(string name, Type type, bool incoming) @@ -430,6 +430,14 @@ public static IEnumerable Apply(Dictionary map, IEnumer } } + public static class RequiresHelper + { + public static Requires Requires(Expr expr, QKeyValue kv = null) + { + return new Requires(Token.NoToken, false, expr, null, kv); + } + } + public static class LinqExtensions { public static IEnumerable> CartesianProduct(this IEnumerable> sequences) diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs index 31b6bf386..dc23de2b0 100644 --- a/Source/Concurrency/InductiveSequentialization.cs +++ b/Source/Concurrency/InductiveSequentialization.cs @@ -5,30 +5,6 @@ namespace Microsoft.Boogie { - public class LinearityCheck - { - public LinearDomain domain; - public Expr assume; - public Expr assert; - public string message; - public string checkName; - - public LinearityCheck(LinearDomain domain, Expr assume, Expr assert, string message, string checkName) - { - this.domain = domain; - this.assume = assume; - this.assert = assert; - this.message = message; - this.checkName = checkName; - } - } - - public enum InductiveSequentializationRule - { - ISL, - ISR - } - public abstract class Sequentialization { protected CivlTypeChecker civlTypeChecker; @@ -47,7 +23,7 @@ protected Sequentialization(CivlTypeChecker civlTypeChecker, Action targetAction public IEnumerable EliminatedActions => eliminatedActions; public int Layer => targetAction.LayerRange.UpperLayer; - public Action TargetAction => targetAction; + protected virtual List GenerateCheckers() { return new List(); @@ -100,98 +76,6 @@ protected AssertCmd GetCheck(IToken tok, Expr expr, string msg) expr.Typecheck(new TypecheckingContext(null, civlTypeChecker.Options)); return CmdHelper.AssertCmd(tok, expr, msg); } - - protected List GeneratePartitionChecker(Action action) - { - var inputDisjointnessExpr = civlTypeChecker.linearTypeChecker.DisjointnessExprForEachDomain( - action.Impl.InParams.Union(action.ModifiedGlobalVars) - .Where(x => LinearTypeChecker.InKinds.Contains(LinearTypeChecker.FindLinearKind(x)))); - - var requires = action.Gate.Select(a => new Requires(false, a.Expr)) - .Concat(inputDisjointnessExpr.Select(expr => new Requires(false, expr))) - .ToList(); - - var eliminatedActionDecls = EliminatedActionDecls.ToHashSet(); - var lhsExprs = new List(); - var rhsExprs = new List(); - foreach (var pendingAsync in action.PendingAsyncs) - { - var pendingAsyncExpr = Expr.Ident(action.PAs(pendingAsync.PendingAsyncType)); - var emptyExpr = ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0)); - if (eliminatedActionDecls.Contains(pendingAsync)) - { - lhsExprs.Add(Expr.Neq(pendingAsyncExpr, emptyExpr)); - } - else - { - rhsExprs.Add(Expr.Eq(pendingAsyncExpr, emptyExpr)); - } - } - var cmds = new List() { - CmdHelper.CallCmd(action.Impl.Proc, action.Impl.InParams, action.Impl.OutParams), - GetCheck(action.tok, Expr.Imp(Expr.Or(lhsExprs), Expr.And(rhsExprs)), "Partition checker failed") - }; - - List checkerBlocks = new List(); - var locals = new List(); - foreach (var pendingAsync in action.PendingAsyncs.Intersect(eliminatedActionDecls)) - { - var pendingAsyncType = pendingAsync.PendingAsyncType; - var pendingAsyncCtor = pendingAsync.PendingAsyncCtor; - var pendingAsyncVar = action.PAs(pendingAsyncType); - var pendingAsyncExpr = Expr.Ident(pendingAsyncVar); - var pendingAsyncAction = civlTypeChecker.Action(pendingAsync); - - var paLocal = civlTypeChecker.LocalVariable($"local_{pendingAsyncVar.Name}", pendingAsyncType); - locals.Add(paLocal); - - List blockCmds = new List - { - CmdHelper.AssumeCmd(Expr.Ge(Expr.Select(pendingAsyncExpr, Expr.Ident(paLocal)), Expr.Literal(1))) - }; - - var substMap = new Dictionary(); - for (int i = 0; i < pendingAsyncAction.Impl.InParams.Count; i++) - { - substMap[pendingAsyncAction.Impl.InParams[i]] = ExprHelper.FieldAccess(Expr.Ident(paLocal), pendingAsyncCtor.InParams[i].Name); - } - blockCmds.AddRange(pendingAsyncAction.GetGateAsserts( - Substituter.SubstitutionFromDictionary(substMap), - $"Gate of {pendingAsyncAction.Name} in partition checker failed")); - - var block = BlockHelper.Block($"label_{pendingAsyncVar.Name}", blockCmds); - checkerBlocks.Add(block); - } - - string checkerName = civlTypeChecker.AddNamePrefix($"PartitionChecker_{action.Name}"); - var blocks = new List(checkerBlocks.Count + 1); - if (checkerBlocks.Count != 0) - { - blocks.Add(BlockHelper.Block(checkerName, cmds, checkerBlocks)); - blocks.AddRange(checkerBlocks); - } - else - { - blocks.Add(BlockHelper.Block(checkerName, cmds)); - } - CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, blocks, ResolutionContext.State.Two); - - Procedure proc = DeclHelper.Procedure( - checkerName, - action.Impl.InParams, - action.Impl.OutParams, - requires, - action.ModifiedGlobalVars.Select(Expr.Ident).ToList(), - new List()); - Implementation impl = DeclHelper.Implementation( - proc, - proc.InParams, - proc.OutParams, - locals, - blocks); - - return new List(new Declaration[] { proc, impl }); - } } public class InlineSequentialization : Sequentialization diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index a20e2ebf7..e6f422d6d 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -18,12 +18,12 @@ private class MoverCheckContext HashSet> commutativityCheckerCache; HashSet> gatePreservationCheckerCache; HashSet> failurePreservationCheckerCache; - HashSet cooperationCheckerCache; + HashSet nonblockingCheckerCache; Dictionary>> perLayerCommutativityCheckerCache; Dictionary>> perLayerGatePreservationCheckerCache; Dictionary>> perLayerFailurePreservationCheckerCache; - Dictionary> perLayerCooperationCheckerCache; + Dictionary> perLayerNonblockingCheckerCache; private MoverCheck(CivlTypeChecker civlTypeChecker, List decls) { @@ -32,11 +32,11 @@ private MoverCheck(CivlTypeChecker civlTypeChecker, List decls) this.commutativityCheckerCache = new HashSet>(); this.gatePreservationCheckerCache = new HashSet>(); this.failurePreservationCheckerCache = new HashSet>(); - this.cooperationCheckerCache = new HashSet(); + this.nonblockingCheckerCache = new HashSet(); this.perLayerCommutativityCheckerCache = new Dictionary>>(); this.perLayerGatePreservationCheckerCache = new Dictionary>>(); this.perLayerFailurePreservationCheckerCache = new Dictionary>>(); - this.perLayerCooperationCheckerCache = new Dictionary>(); + this.perLayerNonblockingCheckerCache = new Dictionary>(); } private ConcurrencyOptions Options => civlTypeChecker.Options; @@ -45,8 +45,6 @@ public static void AddCheckers(CivlTypeChecker civlTypeChecker, List a.IsLeftMover)) { - moverChecking.CreateCooperationChecker(action); + moverChecking.CreateNonblockingChecker(action); } /* @@ -110,7 +108,7 @@ where first.IsRightMover || second.IsLeftMover layer = sequentialization.Layer, extraAssumptions = sequentialization.Preconditions(leftMover, subst).Select(assertCmd => assertCmd.Expr) }; - moverChecking.CreateCooperationChecker(leftMover, moverCheckContext); + moverChecking.CreateNonblockingChecker(leftMover, moverCheckContext); } } } @@ -121,7 +119,7 @@ private IEnumerable DisjointnessAndWellFormedRequires(IEnumerable new Requires(false, expr)); + .Select(expr => RequiresHelper.Requires(expr)); } private void AddChecker(string checkerName, List inputs, List outputs, List locals, @@ -199,16 +197,11 @@ private void CreateCommutativityChecker(Action first, Action second, MoverCheckC DisjointnessAndWellFormedRequires( first.FirstImpl.InParams.Union(second.SecondImpl.InParams) .Where(v => LinearTypeChecker.FindLinearKind(v) != LinearKind.LINEAR_OUT), frame).ToList(); - foreach (AssertCmd assertCmd in first.FirstGate.Union(second.SecondGate)) - { - requires.Add(new Requires(false, assertCmd.Expr)); - } + requires.AddRange(first.FirstGate.Union(second.SecondGate).Select(assertCmd => RequiresHelper.Requires(assertCmd.Expr, assertCmd.Attributes))); if (moverCheckContext != null) { checkerName = $"CommutativityChecker_{first.Name}_{second.Name}_{moverCheckContext.layer}"; - moverCheckContext.extraAssumptions.ForEach(extraAssumption => { - requires.Add(new Requires(false, extraAssumption)); - }); + requires.AddRange(moverCheckContext.extraAssumptions.Select(expr => RequiresHelper.Requires(expr))); } var transitionRelation = TransitionRelationComputation.Commutativity(civlTypeChecker, second, first, frame); @@ -218,11 +211,10 @@ private void CreateCommutativityChecker(Action first, Action second, MoverCheckC IEnumerable linearityAssumes = linearTypeChecker.DisjointnessExprForEachDomain(first.FirstImpl.OutParams.Union(secondInParamsFiltered) .Union(frame)).Union(linearTypeChecker.DisjointnessExprForEachDomain(first.FirstImpl.OutParams.Union(second.SecondImpl.OutParams) .Union(frame))); - // TODO: add further disjointness expressions? - AssertCmd commutativityCheck = CmdHelper.AssertCmd( + var commutativityCheck = CmdHelper.AssertCmd( first.tok, Expr.Imp(Expr.And(linearityAssumes), transitionRelation), - $"Commutativity check between {first.Name} and {second.Name} failed"); + $"Commutativity check between {first.Name} @ {Location(first.ActionDecl.tok)} and {second.Name} @ {Location(second.ActionDecl.tok)} failed"); List cmds = new List { @@ -276,16 +268,11 @@ private void CreateGatePreservationChecker(Action first, Action second, MoverChe DisjointnessAndWellFormedRequires( first.FirstImpl.InParams.Union(second.SecondImpl.InParams) .Where(v => LinearTypeChecker.FindLinearKind(v) != LinearKind.LINEAR_OUT), frame).ToList(); - foreach (AssertCmd assertCmd in first.FirstGate.Union(second.SecondGate)) - { - requires.Add(new Requires(false, assertCmd.Expr)); - } + requires.AddRange(first.FirstGate.Union(second.SecondGate).Select(assertCmd => RequiresHelper.Requires(assertCmd.Expr, assertCmd.Attributes))); if (moverCheckContext != null) { checkerName = $"GatePreservationChecker_{first.Name}_{second.Name}_{moverCheckContext.layer}"; - moverCheckContext.extraAssumptions.ForEach(extraAssumption => { - requires.Add(new Requires(false, extraAssumption)); - }); + requires.AddRange(moverCheckContext.extraAssumptions.Select(expr => RequiresHelper.Requires(expr))); } List inputs = first.FirstImpl.InParams.Union(second.SecondImpl.InParams).ToList(); @@ -296,16 +283,9 @@ private void CreateGatePreservationChecker(Action first, Action second, MoverChe IEnumerable linearityAssumes = linearTypeChecker.DisjointnessExprForEachDomain(first.FirstImpl.InParams.Union(second.SecondImpl.OutParams) .Union(frame)); - foreach (AssertCmd assertCmd in first.FirstGate) - { - cmds.Add( - CmdHelper.AssertCmd( - assertCmd.tok, - Expr.Imp(Expr.And(linearityAssumes), assertCmd.Expr), - $"Gate of {first.Name} not preserved by {second.Name}" - ) - ); - } + cmds.AddRange(first.FirstGate.Select(assertCmd => + CmdHelper.AssertCmd(assertCmd.tok, Expr.Imp(Expr.And(linearityAssumes), assertCmd.Expr), + $"Gate of {first.Name} @ {Location(first.ActionDecl.tok)} not preserved by {second.Name} @ {Location(second.ActionDecl.tok)}"))); AddChecker(checkerName, inputs, outputs, new List(), requires, cmds); } @@ -347,52 +327,42 @@ private void CreateFailurePreservationChecker(Action first, Action second, Mover var linearTypeChecker = civlTypeChecker.linearTypeChecker; List requires = DisjointnessAndWellFormedRequires( - first.FirstImpl.InParams.Union(second.SecondImpl.InParams) - .Where(v => LinearTypeChecker.FindLinearKind(v) != LinearKind.LINEAR_OUT), frame).ToList(); - Expr firstNegatedGate = Expr.Not(Expr.And(first.FirstGate.Select(a => a.Expr))); - firstNegatedGate.Type = Type.Bool; // necessary? - requires.Add(new Requires(false, firstNegatedGate)); - foreach (AssertCmd assertCmd in second.SecondGate) - { - requires.Add(new Requires(false, assertCmd.Expr)); - } + first.FirstImpl.InParams.Union(second.SecondImpl.InParams).Where(v => LinearTypeChecker.FindLinearKind(v) != LinearKind.LINEAR_OUT), frame).ToList(); + var wpreAssertCmds = Wlp.HoistAsserts(second.SecondImpl, first.FirstGate, Options); + requires.AddRange(wpreAssertCmds.Select(assertCmd => RequiresHelper.Requires(assertCmd.Expr, assertCmd.Attributes))); + requires.AddRange(second.SecondGate.Select(assertCmd => RequiresHelper.Requires(assertCmd.Expr, assertCmd.Attributes))); + if (moverCheckContext != null) { checkerName = $"FailurePreservationChecker_{first.Name}_{second.Name}_{moverCheckContext.layer}"; - moverCheckContext.extraAssumptions.ForEach(extraAssumption => { - requires.Add(new Requires(false, extraAssumption)); - }); + requires.AddRange(moverCheckContext.extraAssumptions.Select(expr => RequiresHelper.Requires(expr))); } + var cmds = new List(); IEnumerable linearityAssumes = - linearTypeChecker.DisjointnessExprForEachDomain(first.FirstImpl.InParams.Union(second.SecondImpl.OutParams) - .Union(frame)); - AssertCmd gateFailureCheck = CmdHelper.AssertCmd( - first.tok, - Expr.Imp(Expr.And(linearityAssumes), firstNegatedGate), - $"Gate failure of {first.Name} not preserved by {second.Name}"); + linearTypeChecker.DisjointnessExprForEachDomain(first.FirstImpl.InParams.Union(second.SecondImpl.OutParams).Union(frame)); + cmds.AddRange(linearityAssumes.Select(expr => new AssumeCmd(Token.NoToken, expr))); List inputs = first.FirstImpl.InParams.Union(second.SecondImpl.InParams).ToList(); List outputs = first.FirstImpl.OutParams.Union(second.SecondImpl.OutParams).ToList(); - var cmds = new List - { - ActionCallCmd(second, second.SecondImpl), - gateFailureCheck - }; + cmds.AddRange(first.FirstGate.Select(assertCmd => + CmdHelper.AssertCmd(assertCmd.tok, assertCmd.Expr, + $"Gate failure of {first.Name} @ {Location(first.ActionDecl.tok)} not preserved by {second.Name} @ {Location(second.ActionDecl.tok)}") + )); AddChecker(checkerName, inputs, outputs, new List(), requires, cmds); } - private void CreateCooperationChecker(Action action) => CreateCooperationChecker(action, null); + private void CreateNonblockingChecker(Action action) => CreateNonblockingChecker(action, null); - private void CreateCooperationChecker(Action action, MoverCheckContext moverCheckContext) + private void CreateNonblockingChecker(Action action, MoverCheckContext moverCheckContext) { if (!action.HasAssumeCmd) { return; } - if (!cooperationCheckerCache.Add(action)) + if (!nonblockingCheckerCache.Add(action)) { return; } @@ -400,17 +370,17 @@ private void CreateCooperationChecker(Action action, MoverCheckContext moverChec if (moverCheckContext != null) { var layer = moverCheckContext.layer; - if (!perLayerCooperationCheckerCache.ContainsKey(layer)) + if (!perLayerNonblockingCheckerCache.ContainsKey(layer)) { - perLayerCooperationCheckerCache[layer] = new HashSet(); + perLayerNonblockingCheckerCache[layer] = new HashSet(); } - if (!perLayerCooperationCheckerCache[layer].Add(action)) + if (!perLayerNonblockingCheckerCache[layer].Add(action)) { return; } } - string checkerName = $"CooperationChecker_{action.Name}"; + string checkerName = $"NonblockingChecker_{action.Name}"; Implementation impl = action.Impl; HashSet frame = new HashSet(); @@ -420,20 +390,22 @@ private void CreateCooperationChecker(Action action, MoverCheckContext moverChec List requires = DisjointnessAndWellFormedRequires(impl.InParams.Where(v => LinearTypeChecker.FindLinearKind(v) != LinearKind.LINEAR_OUT), frame).ToList(); - requires.AddRange(action.Gate.Select(assertCmd => new Requires(Token.NoToken, false, assertCmd.Expr, null, assertCmd.Attributes))); + requires.AddRange(action.Gate.Select(assertCmd => RequiresHelper.Requires(assertCmd.Expr, assertCmd.Attributes))); if (moverCheckContext != null) { - checkerName = $"CooperationChecker_{action.Name}_{moverCheckContext.layer}"; - requires.AddRange(moverCheckContext.extraAssumptions.Select(expr => new Requires(false, expr))); + checkerName = $"NonblockingChecker_{action.Name}_{moverCheckContext.layer}"; + requires.AddRange(moverCheckContext.extraAssumptions.Select(expr => RequiresHelper.Requires(expr))); } - AssertCmd cooperationCheck = CmdHelper.AssertCmd( + AssertCmd nonblockingCheck = CmdHelper.AssertCmd( action.tok, - TransitionRelationComputation.Cooperation(civlTypeChecker, action, frame), - $"Cooperation check for {action.Name} failed"); + TransitionRelationComputation.Nonblocking(civlTypeChecker, action, frame), + $"Nonblocking check for {action.Name} failed"); AddChecker(checkerName, new List(impl.InParams), new List(impl.OutParams), - new List(), requires, new List { cooperationCheck }); + new List(), requires, new List { nonblockingCheck }); } + + private static string Location(IToken tok) => string.Format("{0}({1},{2})", tok.filename, tok.line, tok.col); } } \ No newline at end of file diff --git a/Source/Concurrency/TransitionRelationComputation.cs b/Source/Concurrency/TransitionRelationComputation.cs index 9e7381ab4..f94c6d1aa 100644 --- a/Source/Concurrency/TransitionRelationComputation.cs +++ b/Source/Concurrency/TransitionRelationComputation.cs @@ -99,13 +99,13 @@ public static Expr Refinement(CivlTypeChecker civlTypeChecker, Implementation im $"Transition relation of {impl.Name}"); } - public static Expr Cooperation(CivlTypeChecker civlTypeChecker, Action action, HashSet frame) + public static Expr Nonblocking(CivlTypeChecker civlTypeChecker, Action action, HashSet frame) { return ComputeTransitionRelation( civlTypeChecker, action.Impl, null, frame, null, true, - $"Cooperation expression of {action.Name}"); + $"Nonblocking expression of {action.Name}"); } private void EnumeratePaths() diff --git a/Source/Concurrency/Wlp.cs b/Source/Concurrency/Wlp.cs new file mode 100644 index 000000000..df4fdab77 --- /dev/null +++ b/Source/Concurrency/Wlp.cs @@ -0,0 +1,165 @@ +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie.GraphUtil; + +namespace Microsoft.Boogie +{ + public class Wlp + { + /* + * HoistAsserts computes the weakest liberal precondition (wlp) of the body + * of impl as a collection of AssertCmd's. As a side effect, all AssertCmd's + * in any block of impl are removed. + * + * HoistAsserts assumes that the body of impl does not contain any loops or + * calls. The blocks in impl are sorted from entry to exit and processed in + * reverse order, thus ensuring that a block is processed only once the wlp + * of all its successors has been computed. + */ + + public static List HoistAsserts(Implementation impl, ConcurrencyOptions options) + { + return HoistAsserts(impl, new List(), options); + } + + public static List HoistAsserts(Implementation impl, List postconditions, ConcurrencyOptions options) + { + Dictionary> wlps = new Dictionary>(); + Graph dag = Program.GraphFromBlocks(impl.Blocks, false); + foreach (var block in dag.TopologicalSort()) + { + if (block.TransferCmd is ReturnCmd) + { + var wlp = HoistAsserts(block.Cmds, postconditions, options); + wlps.Add(block, wlp); + } + else if (block.TransferCmd is GotoCmd gotoCmd) + { + var wlp = + HoistAsserts(block.Cmds, gotoCmd.LabelTargets.SelectMany(b => wlps[b]).ToList(), options); + wlps.Add(block, wlp); + } + else + { + throw new Cce.UnreachableException(); + } + } + return wlps[impl.Blocks[0]].Select(assertCmd => Forall(impl.LocVars.Union(impl.OutParams), assertCmd)).ToList(); + } + + private static List HoistAsserts(List cmds, List postconditions, ConcurrencyOptions options) + { + for (int i = cmds.Count - 1; i >= 0; i--) + { + var cmd = cmds[i]; + if (cmd is AssertCmd assertCmd) + { + postconditions.Add(assertCmd); + } + else if (cmd is AssumeCmd assumeCmd) + { + QKeyValue Append(QKeyValue assumeAttributes, QKeyValue assertAttributes) + { + if (assumeAttributes == null) + { + return assertAttributes; + } + return new QKeyValue(assumeAttributes.tok, assumeAttributes.Key, assumeAttributes.Params, Append(assumeAttributes.Next, assertAttributes)); + } + postconditions = postconditions + .Select(assertCmd => new AssertCmd(assertCmd.tok, Expr.Imp(assumeCmd.Expr, assertCmd.Expr), Append(assumeCmd.Attributes, assertCmd.Attributes))) + .ToList(); + } + else if (cmd is AssignCmd assignCmd) + { + var varToExpr = new Dictionary(); + var simpleAssignCmd = assignCmd.AsSimpleAssignCmd; + for (var j = 0; j < simpleAssignCmd.Lhss.Count; j++) + { + var lhs = simpleAssignCmd.Lhss[j]; + var rhs = simpleAssignCmd.Rhss[j]; + varToExpr.Add(lhs.DeepAssignedVariable, rhs); + } + postconditions = postconditions.Select(assertCmd => + new AssertCmd(assertCmd.tok, SubstitutionHelper.Apply(varToExpr, assertCmd.Expr), Substitute(assertCmd.Attributes, varToExpr))).ToList(); + } + else if (cmd is HavocCmd havocCmd) + { + postconditions = postconditions.Select(assertCmd => Forall(havocCmd.Vars.Select(ie => ie.Decl), assertCmd)).ToList(); + } + else if (cmd is UnpackCmd unpackCmd) + { + var desugaredCmd = (StateCmd) unpackCmd.GetDesugaring(options); + postconditions = HoistAsserts(desugaredCmd.Cmds, postconditions, options); // removes precondition assert from desugaredCmd.Cmds + } + else + { + throw new Cce.UnreachableException(); + } + } + cmds.RemoveAll(cmd => cmd is AssertCmd); + return postconditions; + } + + private static QKeyValue Substitute(QKeyValue kv, Dictionary always) + { + if (kv == null) + { + return null; + } + var newKv = Substitute(kv.Next, always); + if (kv.Key != "add_to_pool") + { + return new QKeyValue(kv.tok, kv.Key, kv.Params, newKv); + } + return new QKeyValue( + kv.tok, + kv.Key, + kv.Params.Select(param => param is Expr expr ? SubstitutionHelper.Apply(always, expr) : param).ToList(), + newKv); + } + + private static AssertCmd Forall(IEnumerable vars, AssertCmd assertCmd) + { + var freeObjects = new GSet(); + assertCmd.Expr.ComputeFreeVariables(freeObjects); + var quantifiedVars = freeObjects.OfType().Intersect(vars); + if (quantifiedVars.Count() == 0) + { + return assertCmd; + } + + bool KeepExpr(Expr expr) + { + var freeObjects = new GSet(); + expr.ComputeFreeVariables(freeObjects); + return freeObjects.OfType().Intersect(vars).Count() == 0; + } + + QKeyValue Filter(QKeyValue kv) + { + if (kv == null) + { + return null; + } + var newKv = Filter(kv.Next); + if (kv.Key != "add_to_pool") + { + return new QKeyValue(kv.tok, kv.Key, kv.Params, newKv); + } + return new QKeyValue( + kv.tok, + kv.Key, + kv.Params.Where(param => param is not Expr expr || KeepExpr(expr)).ToList(), + newKv); + } + + var varMapping = quantifiedVars.ToDictionary(v => v, + v => (Variable) VarHelper.BoundVariable(v.Name, v.TypedIdent.Type, v.Attributes)); + return new AssertCmd( + assertCmd.tok, + ExprHelper.ForallExpr(varMapping.Values.ToList(), SubstitutionHelper.Apply(varMapping, assertCmd.Expr)), + Filter(assertCmd.Attributes)); + } + } +} \ No newline at end of file diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs index 4a8fb09ee..702c5c768 100644 --- a/Source/Core/AST/Implementation.cs +++ b/Source/Core/AST/Implementation.cs @@ -552,13 +552,23 @@ public override void Resolve(ResolutionContext rc) (this as ICarriesAttributes).ResolveAttributes(rc); rc.Proc = Proc; - rc.StateMode = Proc.IsPure ? ResolutionContext.State.StateLess : ResolutionContext.State.Two; + if (Proc.IsPure) + { + rc.StateMode = ResolutionContext.State.StateLess; + } + else if (Proc is not ActionDecl) + { + rc.StateMode = ResolutionContext.State.Two; + } foreach (Block b in Blocks) { b.Resolve(rc); } rc.Proc = null; - rc.StateMode = ResolutionContext.State.Single; + if (Proc.IsPure || Proc is not ActionDecl) + { + rc.StateMode = ResolutionContext.State.Single; + } rc.PopProcedureContext(); rc.PopVarContext(); diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs index 82991c1b4..eb67c8024 100644 --- a/Source/VCExpr/QuantifierInstantiationEngine.cs +++ b/Source/VCExpr/QuantifierInstantiationEngine.cs @@ -275,7 +275,7 @@ private VCExpr Execute(Implementation impl, VCExpr vcExpr) * quantifierBinding may be modified in each iteration of the following loop. * Therefore, take a snapshot of quantifierBinding.Keys to start the loop. */ - foreach (var v in quantifierBinding.Keys) + foreach (var v in quantifierBinding.Keys.ToList()) { if (visitedQuantifierBindings.Contains(v)) { diff --git a/Test/civl/async/2pc.bpl b/Test/civl/async/2pc.bpl index f47ca4511..ae3a0b63e 100644 --- a/Test/civl/async/2pc.bpl +++ b/Test/civl/async/2pc.bpl @@ -228,12 +228,12 @@ preserves call YieldConsistent_10(); left action {:layer 10} atomic_Participant_VoteReq (xid: Xid, mid: Mid, {:linear_in} pair: One Pair) modifies state; { - var {:pool "A"} x: XState; + var {:pool "A"} next_state_xid: XState; assert Set_IsDisjoint(perm(xid), UnallocatedXids); assert pair(xid, mid, pair->val); - assert xConsistent(state[xid]); - state[xid] := x; - assume xConsistentExtension(old(state)[xid], state[xid]); + assert {:add_to_pool "A", state[xid]} xConsistent(state[xid]); + assume {:add_to_pool "A", next_state_xid} xConsistentExtension(state[xid], next_state_xid); + state[xid] := next_state_xid; } yield procedure {:layer 9} @@ -258,15 +258,15 @@ requires call YieldInv_9(xid); left action {:layer 9} atomic_Coordinator_VoteYes (xid: Xid, mid: Mid, {:linear_in} pair: One Pair) modifies state, B; { - var {:pool "A"} x: XState; + var {:pool "A"} next_state_xid: XState; assert Set_IsDisjoint(perm(xid), UnallocatedXids); assert pair(xid, mid, pair->val); assert xConsistent(state[xid]); call One_Put(B, pair); if (*) { - state[xid] := x; + assume {:add_to_pool "A", next_state_xid} xConsistentExtension(state[xid], next_state_xid); + state[xid] := next_state_xid; assume xAllParticipantsInB(xid, B); - assume xConsistentExtension(old(state)[xid], state[xid]); } } @@ -307,13 +307,13 @@ requires call YieldUndecidedOrCommitted_8(xid, mid, pair); left action {:layer 9} atomic_Coordinator_VoteNo (xid: Xid, mid: Mid, {:linear_in} pair: One Pair) modifies state; { - var {:pool "A"} x: XState; + var {:pool "A"} next_state_xid: XState; assert Set_IsDisjoint(perm(xid), UnallocatedXids); assert pair(xid, mid, pair->val); - assert xUndecidedOrAborted(state[xid]); - state[xid] := x; + assert {:add_to_pool "A", state[xid]} xUndecidedOrAborted(state[xid]); + assume {:add_to_pool "A", next_state_xid} xConsistentExtension(state[xid], next_state_xid); + state[xid] := next_state_xid; assume xUndecidedOrAborted(state[xid]); - assume xConsistentExtension(old(state)[xid], state[xid]); } yield procedure {:layer 8} diff --git a/Test/civl/async/tds.bpl b/Test/civl/async/tds.bpl index 0f71deee9..745cef751 100644 --- a/Test/civl/async/tds.bpl +++ b/Test/civl/async/tds.bpl @@ -89,7 +89,7 @@ refines atomic_server; left action {:layer 3} atomic_server2({:linear} i: One int) modifies status; { - assert status[i->val] == DEFAULT; + assert {:add_to_pool "A", i->val} status[i->val] == DEFAULT; status[i->val] := CREATED; } yield procedure {:layer 2} server2({:linear} i: One int); @@ -119,8 +119,8 @@ refines atomic_master; atomic action {:layer 3} atomic_master2() modifies status; { - assert (forall i: int :: 0 <= i && i < n ==> status[i] == PROCESSED); - status := (lambda j: int :: if (0 <= j && j < n) then FINISHED else status[j]); + assert (forall {:pool "A"} i: int :: {:add_to_pool "A", i} 0 <= i && i < n ==> status[i] == PROCESSED); + status := (lambda {:pool "A"} j: int :: if (0 <= j && j < n) then FINISHED else status[j]); } yield procedure {:layer 2} master2(); refines atomic_master2; diff --git a/Test/civl/inductive-sequentialization/2PC.bpl b/Test/civl/inductive-sequentialization/2PC.bpl deleted file mode 100644 index 99509bc77..000000000 --- a/Test/civl/inductive-sequentialization/2PC.bpl +++ /dev/null @@ -1,465 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type {:linear "pid"} Pid = int; - -// A type for vote messages of participants -datatype vote { YES(), NO() } - -// A type for decision message of the coordinator -datatype decision { COMMIT(), ABORT(), NONE() } - -// Number of participants -const n:int; -axiom n > 0; - -// Participants have IDs from 1 to n, and the coordinator has ID 0. -function {:inline} pid (pid:int) : bool { 1 <= pid && pid <= n } -function {:inline} pidLe (pid:int, k:int) : bool { 1 <= pid && pid <= k } -function {:inline} pidGt (pid:int, k:int) : bool { k < pid && pid <= n } - -// Channel of the participants for request messages from the coordinator -var {:layer 0,6} RequestChannel:[int]int; -// Channel of the participants for decision messages from the coordinator -var {:layer 0,6} DecisionChannel:[int][decision]int; -// Channel of the coordinator for vote messages from the participants -var {:layer 0,6} VoteChannel:[vote]int; -// Participant votes -var {:layer 0,6} votes:[int]vote; -// Coordinator and participant decisions -var {:layer 0,6} decisions:[int]decision; - -//////////////////////////////////////////////////////////////////////////////// - -function {:inline} Init(pids:[int]bool, RequestChannel:[int]int, VoteChannel:[vote]int, - DecisionChannel:[int][decision]int, decisions:[int]decision) : bool -{ - pids == MapConst(true) && - RequestChannel == (lambda i:int :: 0) && - VoteChannel == (lambda v:vote :: 0) && - DecisionChannel == (lambda i:int :: (lambda d:decision :: 0)) && - decisions == (lambda i:int :: NONE()) -} - -//////////////////////////////////////////////////////////////////////////////// - -atomic action {:layer 6} -MAIN5 ({:linear_in} pids: Set int) -modifies RequestChannel, VoteChannel, votes, decisions; -{ - var dec:decision; - assert Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - havoc RequestChannel, VoteChannel, votes, decisions; - if (*) { dec := COMMIT(); } else { dec := ABORT(); } - assume dec == COMMIT() ==> (forall i:int :: pid(i) ==> votes[i] == YES()); - assume (forall i:int :: (i == 0 || pid(i)) ==> decisions[i] == dec); -} - -action {:layer 5} INV4 ({:linear_in} pids: Set int) -creates PARTICIPANT2; -modifies RequestChannel, VoteChannel, DecisionChannel, votes, decisions; -{ - var {:pool "INV4"} k: int; - var {:linear} pids': Set int; - var {:linear} participantPids: Set int; - - assert Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - - assume - {:add_to_pool "INV4", k, k+1} - {:add_to_pool "PARTICIPANT2", PARTICIPANT2(One(n))} - 0 <= k && k <= n; - havoc RequestChannel, VoteChannel, votes, decisions; - assume - (decisions[0] == COMMIT() || decisions[0] == ABORT()) && - (decisions[0] == COMMIT() ==> (forall i:int :: pid(i) ==> votes[i] == YES())) && - (forall i:int :: pidLe(i,k) ==> decisions[i] == decisions[0]); - DecisionChannel := (lambda i:int :: (lambda d:decision :: if pidGt(i, k) && d == decisions[0] then 1 else 0)); - - pids' := pids; - call participantPids := Set_Get(pids', (lambda i:int :: k < i && i <= n)); - call {:linear participantPids} create_asyncs((lambda {:pool "PARTICIPANT2"} pa:PARTICIPANT2 :: pidGt(pa->pid->val, k))); - call set_choice(PARTICIPANT2(One(k+1))); -} - -yield invariant {:layer 5} YieldParticipant ({:linear} pid: One int); -invariant DecisionChannel[pid->val][COMMIT()] > 0 || DecisionChannel[pid->val][ABORT()] > 0; - -//////////////////////////////////////////////////////////////////////////////// - -atomic action {:layer 5} MAIN4 ({:linear_in} pids: Set int) -refines MAIN5 using INV4; -creates PARTICIPANT2; -modifies RequestChannel, VoteChannel, DecisionChannel, votes, decisions; -{ - var dec:decision; - var {:linear} pids': Set int; - var {:linear} participantPids: Set int; - - assert Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - - assume {:add_to_pool "INV4", 0} true; - havoc RequestChannel, VoteChannel, votes; - if (*) { dec := COMMIT(); } else { dec := ABORT(); } - assume dec == COMMIT() ==> (forall i:int :: pid(i) ==> votes[i] == YES()); - decisions[0] := dec; - DecisionChannel := (lambda i:int :: (lambda d:decision :: if pid(i) && d == dec then 1 else 0)); - pids' := pids; - call participantPids := Set_Get(pids', (lambda i:int :: pid(i))); - call {:linear participantPids} create_asyncs((lambda pa:PARTICIPANT2 :: pid(pa->pid->val))); -} - -//////////////////////////////////////////////////////////////////////////////// - -atomic action {:layer 4} MAIN3 ({:linear_in} pids: Set int) -refines MAIN4; -creates COORDINATOR2, PARTICIPANT2; -modifies RequestChannel, VoteChannel, votes; -{ - var {:linear} pids': Set int; - var {:linear} pid: One int; - var {:linear} participantPids: Set int; - - assert Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - - havoc RequestChannel, VoteChannel, votes; - assume VoteChannel[YES()] >= 0 && VoteChannel[NO()] >= 0; - assume VoteChannel[YES()] + VoteChannel[NO()] <= n; - assume VoteChannel[YES()] == n ==> (forall i:int :: pid(i) ==> votes[i] == YES()); - pids' := pids; - call pid := One_Get(pids', 0); - async call COORDINATOR2(pid); - call participantPids := Set_Get(pids', (lambda i:int :: pid(i))); - call {:linear participantPids} create_asyncs((lambda pa:PARTICIPANT2 :: pid(pa->pid->val))); -} - -action {:layer 3} -INV2 ({:linear_in} pids: Set int) -creates COORDINATOR2, PARTICIPANT1, PARTICIPANT2; -modifies RequestChannel, VoteChannel, votes; -{ - var {:linear} pids': Set int; - var {:linear} pid: One int; - var {:linear} participantPids: Set int; - var {:pool "INV2"} k: int; - - assert Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - - havoc RequestChannel, VoteChannel, votes; - assume - {:add_to_pool "INV2", k, k+1} - {:add_to_pool "PARTICIPANT1", PARTICIPANT1(One(n))} - 0 <= k && k <= n; - assume (forall i:int :: pidGt(i,k) ==> RequestChannel[i] == 1) && - VoteChannel[YES()] >= 0 && VoteChannel[NO()] >= 0 && - VoteChannel[YES()] + VoteChannel[NO()] <= k && - (VoteChannel[YES()] == k ==> (forall i:int :: pidLe(i,k) ==> votes[i] == YES())); - pids' := pids; - call pid := One_Get(pids', 0); - async call COORDINATOR2(pid); - call participantPids := Set_Get(pids', (lambda i:int :: 1 <= i && i <= k)); - call {:linear participantPids} create_asyncs((lambda pa:PARTICIPANT2 :: pidLe(pa->pid->val, k))); - call participantPids := Set_Get(pids', (lambda i:int :: k < i && i <= n)); - call {:linear participantPids} create_asyncs((lambda {:pool "PARTICIPANT1"} pa:PARTICIPANT1 :: pidGt(pa->pid->val, k))); - call set_choice(PARTICIPANT1(One(k+1))); -} - -//////////////////////////////////////////////////////////////////////////////// - -atomic action {:layer 3} MAIN2 ({:linear_in} pids: Set int) -refines MAIN3 using INV2; -creates COORDINATOR2, PARTICIPANT1; -modifies RequestChannel; -{ - var {:linear} pids': Set int; - var {:linear} pid: One int; - var {:linear} participantPids: Set int; - - assert Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - - assume {:add_to_pool "INV2", 0} true; - RequestChannel := (lambda i:int :: if pid(i) then 1 else 0); - pids' := pids; - call pid := One_Get(pids', 0); - async call COORDINATOR2(pid); - call participantPids := Set_Get(pids', (lambda i:int :: pid(i))); - call {:linear participantPids} create_asyncs((lambda pa:PARTICIPANT1 :: pid(pa->pid->val))); -} - -//////////////////////////////////////////////////////////////////////////////// - -atomic action {:layer 2} MAIN1 ({:linear_in} pids: Set int) -refines MAIN2; -creates COORDINATOR1, PARTICIPANT1; -{ - var {:linear} pids': Set int; - var {:linear} pid: One int; - var {:linear} participantPids: Set int; - - assert Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - - pids' := pids; - call pid := One_Get(pids', 0); - async call COORDINATOR1(pid); - call participantPids := Set_Get(pids', (lambda i:int :: pid(i))); - call {:linear participantPids} create_asyncs((lambda pa:PARTICIPANT1 :: pid(pa->pid->val))); -} - -async atomic action {:layer 2,3} PARTICIPANT1 ({:linear_in} pid: One int) -creates PARTICIPANT2; -modifies RequestChannel, VoteChannel, votes; -{ - var v:vote; - assert pid(pid->val); - - if (*) - { - assume RequestChannel[pid->val] > 0; - RequestChannel[pid->val] := RequestChannel[pid->val] - 1; - if (*) { v := YES(); } else { v := NO(); } - votes[pid->val] := v; - VoteChannel[v] := VoteChannel[v] + 1; - } - - async call PARTICIPANT2(pid); -} - -async atomic action {:layer 2,5} PARTICIPANT2 ({:linear_in} pid: One int) -modifies DecisionChannel, decisions; -requires call YieldParticipant(pid); -{ - var d:decision; - assert pid(pid->val); - assert DecisionChannel[pid->val][NONE()] == 0; - if (*) { d := COMMIT(); } else { d := ABORT(); } - assume DecisionChannel[pid->val][d] > 0; - DecisionChannel[pid->val][d] := DecisionChannel[pid->val][d] - 1; - decisions[pid->val] := d; -} - -async left action {:layer 2} COORDINATOR1 ({:linear_in} pid: One int) -creates COORDINATOR2; -modifies RequestChannel; -{ - assert pid->val == 0; - RequestChannel := (lambda i:int :: if pid(i) then RequestChannel[i] + 1 else RequestChannel[i]); - async call COORDINATOR2(pid); -} - -async atomic action {:layer 2,4} COORDINATOR2 ({:linear_in} pid: One int) -modifies VoteChannel, DecisionChannel, decisions; -{ - var dec:decision; - assert pid->val == 0; - - if (*) - { - assume VoteChannel[YES()] >= n; - dec := COMMIT(); - } - else - { - dec := ABORT(); - } - - decisions[pid->val] := dec; - havoc VoteChannel; - DecisionChannel := (lambda i:int :: (lambda d:decision :: if pid(i) && d == dec then DecisionChannel[i][d] + 1 else DecisionChannel[i][d])); -} - -//////////////////////////////////////////////////////////////////////////////// - -yield invariant {:layer 1} YieldInit({:linear} pids: Set int); -invariant Init(pids->val, RequestChannel, VoteChannel, DecisionChannel, decisions); - -yield procedure {:layer 1} main ({:linear_in} pids: Set int) -refines MAIN1; -requires call YieldInit(pids); -{ - var i:int; - var {:pending_async}{:layer 1} Coordinator1_PAs:[COORDINATOR1]int; - var {:pending_async}{:layer 1} Participant1_PAs:[PARTICIPANT1]int; - var {:linear} pid: One int; - var {:linear} pids': Set int; - - pids' := pids; - call pid := One_Get(pids', 0); - async call coordinator1(pid); - i := 1; - while (i <= n) - invariant {:layer 1} 1 <= i && i <= n+1; - invariant {:layer 1} (forall ii:int :: pid(ii) && ii >= i ==> pids'->val[ii]); - invariant {:layer 1} Coordinator1_PAs == MapConst(0)[COORDINATOR1(One(0)) := 1]; - invariant {:layer 1} Participant1_PAs == (lambda pa:PARTICIPANT1 :: if pid(pa->pid->val) && pa->pid->val < i then 1 else 0); - { - call pid := One_Get(pids', i); - async call participant1(pid); - i := i + 1; - } -} - -yield procedure {:layer 1} participant1 ({:linear_in} pid: One int) -refines PARTICIPANT1; -requires {:layer 1} pid(pid->val); -{ - var v:vote; - - if (*) - { - call receive_req(pid->val); - havoc v; - call set_vote(pid, v); - call send_vote(v); - } - async call participant2(pid); -} - -yield procedure {:layer 1} participant2 ({:linear_in} pid: One int) -refines PARTICIPANT2; -requires {:layer 1} pid(pid->val); -{ - var d:decision; - - call d := receive_decision(pid->val); - call set_decision(pid, d); -} - -yield invariant {:layer 1} YieldCoordinator(); -invariant (forall vv:vote :: VoteChannel[vv] >= 0); - -yield procedure {:layer 1} coordinator1 ({:linear_in} pid: One int) -refines COORDINATOR1; -requires {:layer 1} pid->val == 0; -requires call YieldCoordinator(); -{ - var i:int; - var {:layer 1} old_RequestChannel:[int]int; - - call {:layer 1} old_RequestChannel := Copy(RequestChannel); - i := 1; - while (i <= n) - invariant {:layer 1} 1 <= i && i <= n+1; - invariant {:layer 1} RequestChannel == (lambda ii:int :: if pid(ii) && ii < i then old_RequestChannel[ii] + 1 else old_RequestChannel[ii]); - { - call send_request(i); - i := i + 1; - } - async call coordinator2(pid); -} - -yield procedure {:layer 1} coordinator2 ({:linear_in} pid: One int) -refines COORDINATOR2; -requires {:layer 1} pid->val == 0; -requires call YieldCoordinator(); -{ - var d:decision; - var v:vote; - var i:int; - var {:layer 1} old_VoteChannel:[vote]int; - var {:layer 1} old_DecisionChannel:[int][decision]int; - - call {:layer 1} old_VoteChannel := Copy(VoteChannel); - call {:layer 1} old_DecisionChannel := Copy(DecisionChannel); - i := 0; - d := COMMIT(); - while (i < n) - invariant {:layer 1} 0 <= i && i <= n; - invariant {:layer 1} VoteChannel[YES()] == old_VoteChannel[YES()] - i; - invariant {:layer 1} old_VoteChannel[YES()] - i >= 0; - invariant {:layer 1} VoteChannel[NO()] == old_VoteChannel[NO()]; - { - call v := receive_vote(); - if (v == NO()) - { - d := ABORT(); - break; - } - i := i + 1; - } - call set_decision(pid, d); - i := 1; - while (i <= n) - invariant {:layer 1} 1 <= i && i <= n+1; - invariant {:layer 1} DecisionChannel == (lambda ii:int :: (lambda dd:decision :: if pid(ii) && ii < i && dd == d then old_DecisionChannel[ii][dd] + 1 else old_DecisionChannel[ii][dd])); - { - call send_decision(i, d); - i := i + 1; - } -} - -//////////////////////////////////////////////////////////////////////////////// - -both action {:layer 1} SET_VOTE({:linear} pid: One int, v:vote) -modifies votes; -{ - votes[pid->val] := v; -} - -both action {:layer 1} SET_DECISION({:linear} pid: One int, d:decision) -modifies decisions; -{ - decisions[pid->val] := d; -} - -left action {:layer 1} SEND_REQUEST(pid:int) -modifies RequestChannel; -{ - RequestChannel[pid] := RequestChannel[pid] + 1; -} - -right action {:layer 1} RECEIVE_REQ(pid:int) -modifies RequestChannel; -{ - assume RequestChannel[pid] > 0; - RequestChannel[pid] := RequestChannel[pid] - 1; -} - -left action {:layer 1} SEND_VOTE(v:vote) -modifies VoteChannel; -{ - VoteChannel[v] := VoteChannel[v] + 1; -} - -right action {:layer 1} RECEIVE_VOTE() returns (v:vote) -modifies VoteChannel; -{ - assume VoteChannel[v] > 0; - VoteChannel[v] := VoteChannel[v] - 1; -} - -left action {:layer 1} SEND_DECISION(pid:int, d:decision) -modifies DecisionChannel; -{ - DecisionChannel[pid][d] := DecisionChannel[pid][d] + 1; -} - -right action {:layer 1} RECEIVE_DECISION(pid:int) returns (d:decision) -modifies DecisionChannel; -{ - assume DecisionChannel[pid][d] > 0; - DecisionChannel[pid][d] := DecisionChannel[pid][d] - 1; -} - -yield procedure {:layer 0} set_vote({:linear} pid: One int, v:vote); -refines SET_VOTE; - -yield procedure {:layer 0} set_decision({:linear} pid: One int, d:decision); -refines SET_DECISION; - -yield procedure {:layer 0} send_request(pid:int); -refines SEND_REQUEST; - -yield procedure {:layer 0} receive_req(pid:int); -refines RECEIVE_REQ; - -yield procedure {:layer 0} send_vote(v:vote); -refines SEND_VOTE; - -yield procedure {:layer 0} receive_vote() returns (v:vote); -refines RECEIVE_VOTE; - -yield procedure {:layer 0} send_decision(pid:int, d:decision); -refines SEND_DECISION; - -yield procedure {:layer 0} receive_decision(pid:int) returns (d:decision); -refines RECEIVE_DECISION; diff --git a/Test/civl/inductive-sequentialization/2PC.bpl.expect b/Test/civl/inductive-sequentialization/2PC.bpl.expect deleted file mode 100644 index 309f0e6f6..000000000 --- a/Test/civl/inductive-sequentialization/2PC.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 55 verified, 0 errors diff --git a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl index 35981057d..794d1cc6a 100644 --- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl +++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl @@ -75,7 +75,7 @@ modifies CH, decision; CH := (lambda v:val :: value_card(v, value, 1, n)); assume card(CH) == n; assume MultisetSubsetEq(MultisetEmpty, CH); - decision := (lambda i:pid :: if pid(i) then max(CH) else old(decision)[i]); + decision := (lambda i:pid :: if pid(i) then max(CH) else decision[i]); } action {:layer 3} diff --git a/Test/civl/large-samples/GC.bpl b/Test/civl/large-samples/GC.bpl index e620aba05..16082b1e4 100644 --- a/Test/civl/large-samples/GC.bpl +++ b/Test/civl/large-samples/GC.bpl @@ -556,9 +556,11 @@ preserves call Yield_Lock(); atomic action {:layer 100} AtomicCanMarkStop({:linear} tid:Tid) returns (canStop: bool) modifies Color; { + var old_Color: [int]int; assert tid == GcTid; + old_Color := Color; havoc Color; - assume (forall u: int :: if memAddr(u) && White(old(Color)[u]) && (exists k: int :: rootAddr(k) && root[k] == u) then Color[u] == GRAY() else Color[u] == old(Color)[u]); + assume (forall u: int :: if memAddr(u) && White(old_Color[u]) && (exists k: int :: rootAddr(k) && root[k] == u) then Color[u] == GRAY() else Color[u] == old_Color[u]); canStop := (forall v: int :: memAddr(v) ==> !Gray(Color[v])); } diff --git a/Test/civl/large-samples/cache-coherence.bpl b/Test/civl/large-samples/cache-coherence.bpl index 822f42b53..cc12ef290 100644 --- a/Test/civl/large-samples/cache-coherence.bpl +++ b/Test/civl/large-samples/cache-coherence.bpl @@ -235,7 +235,7 @@ refines atomic action {:layer 2} _ { result := Ok(); ca := Hash(ma); line := cache[i][ca]; - assume line->state != Invalid() && line->state != Shared() && line->ma == ma && Set_Contains(cachePermissions, CachePermission(i, ca)); + assume {:add_to_pool "X", i} line->state != Invalid() && line->state != Shared() && line->ma == ma && Set_Contains(cachePermissions, CachePermission(i, ca)); cache[i][ca]->value := v; cache[i][ca]->state := Modified(); absMem[ma] := v; @@ -401,7 +401,7 @@ refines left action {:layer 2} _ { assert Set_Contains(dp, DirPermission(i, ma)); assume {:add_to_pool "DirPermission", DirPermission(i, ma)} true; ca := Hash(ma); - assert (forall j: CacheId :: (var line := cache[j][ca]; line->ma == ma ==> line->state == Invalid() || line->state == Shared())); + assert (forall {:pool "X"} j: CacheId :: {:add_to_pool "X", j} (var line := cache[j][ca]; line->ma == ma ==> line->state == Invalid() || line->state == Shared())); // this assertion accompanies the relaxation in cache_read#1 to allow cache_invalidate_shd#1 to commute to the left of cache_read#1 assert cache[i][ca]->value == absMem[ma]; call primitive_cache_invalidate_shd(i, ma, s); diff --git a/Test/civl/large-samples/verified-ft.bpl b/Test/civl/large-samples/verified-ft.bpl index 5c6f4faea..84ef9d3b3 100644 --- a/Test/civl/large-samples/verified-ft.bpl +++ b/Test/civl/large-samples/verified-ft.bpl @@ -391,10 +391,10 @@ modifies shadow.VC; assert VCRepOk(shadow.VC[v2]); assert VCRepOk(shadow.VC[v1]); if (*) { + assume VCRepOk(vc); + assume VCArrayLen(vc) == max(VCArrayLen(shadow.VC[v1]),VCArrayLen(shadow.VC[v2])); + assume (forall j: int :: 0 <= j ==> VCArrayGet(vc, j) == VCArrayGet(shadow.VC[v2], j)); shadow.VC[v1] := vc; - assume VCRepOk(shadow.VC[v1]); - assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); - assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == VCArrayGet(old(shadow.VC)[v2], j)); } else { shadow.VC[v1] := shadow.VC[v2]; } @@ -451,10 +451,10 @@ modifies shadow.VC; assert !(v1 is ShadowableVar); assert !(v2 is ShadowableVar); assert VCRepOk(shadow.VC[v2]); + assume VCRepOk(vc); + assume VCArrayLen(vc) == max(VCArrayLen(shadow.VC[v1]),VCArrayLen(shadow.VC[v2])); + assume (forall j: int :: 0 <= j ==> VCArrayGet(vc, j) == EpochMax(VCArrayGet(shadow.VC[v1], j), VCArrayGet(shadow.VC[v2], j))); shadow.VC[v1] := vc; - assume VCRepOk(shadow.VC[v1]); - assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); - assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == EpochMax(VCArrayGet(old(shadow.VC)[v1], j), VCArrayGet(old(shadow.VC)[v2], j))); } yield procedure {:layer 10} @@ -557,17 +557,17 @@ modifies shadow.VC; v1 := ShadowableTid(uid); v2 := ShadowableTid(tid->val); - shadow.VC[v1] := vc1; - shadow.VC[v2] := vc2; + assume VCArrayLen(vc1) == max(VCArrayLen(shadow.VC[v1]),VCArrayLen(shadow.VC[v2])); + assume VCRepOk(vc1); + assume (forall j: int :: 0 <= j ==> VCArrayGet(vc1, j) == EpochMax(VCArrayGet(shadow.VC[v1], j), VCArrayGet(shadow.VC[v2], j))); - assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); - assume VCRepOk(shadow.VC[v1]); - assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == EpochMax(VCArrayGet(old(shadow.VC)[v1], j), VCArrayGet(old(shadow.VC)[v2], j))); + assume VCRepOk(vc2); + assume VCArrayLen(vc2) == max(VCArrayLen(vc2), tid->val + 1); + assume (forall j: int :: 0 <= j && j != tid->val ==> VCArrayGet(vc2, j) == VCArrayGet(shadow.VC[v2], j)); + assume VCArrayGet(vc2, tid->val) == EpochInc(VCArrayGet(shadow.VC[v2], tid->val)); - assume VCRepOk(shadow.VC[v2]); - assume VCArrayLen(shadow.VC[v2]) == max(VCArrayLen(shadow.VC[v2]), tid->val + 1); - assume (forall j: int :: 0 <= j && j != tid->val ==> VCArrayGet(shadow.VC[v2], j) == VCArrayGet(old(shadow.VC)[v2], j)); - assume VCArrayGet(shadow.VC[v2], tid->val) == EpochInc(VCArrayGet(old(shadow.VC)[v2], tid->val)); + shadow.VC[v1] := vc1; + shadow.VC[v2] := vc2; } yield procedure {:layer 20} Fork({:linear} tid: One Tid, uid : Tid) @@ -599,12 +599,12 @@ modifies shadow.VC; v1 := ShadowableTid(uid); v2 := ShadowableTid(tid->val); - shadow.VC[v2] := vc; - assume VCArrayLen(shadow.VC[v2]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); - assume VCRepOk(shadow.VC[v2]); + assume VCArrayLen(vc) == max(VCArrayLen(shadow.VC[v1]),VCArrayLen(shadow.VC[v2])); + assume VCRepOk(vc); assume (forall j: int :: 0 <= j ==> - VCArrayGet(shadow.VC[v2], j) == - EpochMax(VCArrayGet(old(shadow.VC)[v2], j), VCArrayGet(old(shadow.VC)[v1], j))); + VCArrayGet(vc, j) == + EpochMax(VCArrayGet(shadow.VC[v2], j), VCArrayGet(shadow.VC[v1], j))); + shadow.VC[v2] := vc; } yield procedure {:layer 20} @@ -633,12 +633,12 @@ modifies shadow.VC; v1 := ShadowableTid(tid->val); v2 := ShadowableLock(l); - shadow.VC[v1] := vc; - assume VCRepOk(shadow.VC[v1]); - assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); + assume VCRepOk(vc); + assume VCArrayLen(vc) == max(VCArrayLen(shadow.VC[v1]),VCArrayLen(shadow.VC[v2])); assume (forall j: int :: 0 <= j ==> - VCArrayGet(shadow.VC[v1], j) == - EpochMax(VCArrayGet(old(shadow.VC)[v1], j), VCArrayGet(old(shadow.VC)[v2], j))); + VCArrayGet(vc, j) == + EpochMax(VCArrayGet(shadow.VC[v1], j), VCArrayGet(shadow.VC[v2], j))); + shadow.VC[v1] := vc; } yield procedure {:layer 20} Acquire({:linear} tid: One Tid, l: Lock) @@ -666,22 +666,22 @@ modifies shadow.VC; v1 := ShadowableLock(l); v2 := ShadowableTid(tid->val); - shadow.VC[v1] := vc1; - shadow.VC[v2] := vc2; - // Use the same strategy as in Copy's atomic spec. if (*) { - assume VCRepOk(shadow.VC[v1]); - assume VCArrayLen(shadow.VC[v1]) == max(VCArrayLen(old(shadow.VC)[v1]),VCArrayLen(old(shadow.VC)[v2])); - assume (forall j: int :: 0 <= j ==> VCArrayGet(shadow.VC[v1], j) == VCArrayGet(old(shadow.VC)[v2], j)); + assume VCRepOk(vc1); + assume VCArrayLen(vc1) == max(VCArrayLen(shadow.VC[v1]),VCArrayLen(shadow.VC[v2])); + assume (forall j: int :: 0 <= j ==> VCArrayGet(vc1, j) == VCArrayGet(shadow.VC[v2], j)); } else { - assume shadow.VC[v1] == old(shadow.VC)[v2]; + assume vc1 == shadow.VC[v2]; } - assume VCRepOk(shadow.VC[v2]); - assume VCArrayLen(shadow.VC[v2]) == max(VCArrayLen(shadow.VC[v2]), tid->val + 1); - assume (forall j: int :: 0 <= j && j != tid->val ==> VCArrayGet(shadow.VC[v2], j) == VCArrayGet(old(shadow.VC)[v2], j)); - assume VCArrayGet(shadow.VC[v2], tid->val) == EpochInc(VCArrayGet(old(shadow.VC)[v2], tid->val)); + assume VCRepOk(vc2); + assume VCArrayLen(vc2) == max(VCArrayLen(vc2), tid->val + 1); + assume (forall j: int :: 0 <= j && j != tid->val ==> VCArrayGet(vc2, j) == VCArrayGet(shadow.VC[v2], j)); + assume VCArrayGet(vc2, tid->val) == EpochInc(VCArrayGet(shadow.VC[v2], tid->val)); + + shadow.VC[v1] := vc1; + shadow.VC[v2] := vc2; } yield procedure {:layer 20} Release({:linear} tid: One Tid, l: Lock) diff --git a/Test/civl/regression-tests/chris2.bpl.expect b/Test/civl/regression-tests/chris2.bpl.expect index c25bf49cc..9b5764068 100644 --- a/Test/civl/regression-tests/chris2.bpl.expect +++ b/Test/civl/regression-tests/chris2.bpl.expect @@ -1,22 +1,18 @@ -chris2.bpl(23,3): Error: Gate of atomic_p_gt2 not preserved by atomic_p_gt1_lower +chris2.bpl(23,3): Error: Gate of atomic_p_gt2 @ chris2.bpl(22,28) not preserved by atomic_p_gt1_lower @ chris2.bpl(5,28) Execution trace: chris2.bpl(5,28): inline$atomic_p_gt1_lower$0$Entry chris2.bpl(7,5): inline$atomic_p_gt1_lower$0$anon0 chris2.bpl(5,28): inline$atomic_p_gt1_lower$0$Return -chris2.bpl(23,3): Error: Gate of atomic_p_gt2 not preserved by atomic_p_gt1 +chris2.bpl(23,3): Error: Gate of atomic_p_gt2 @ chris2.bpl(22,28) not preserved by atomic_p_gt1 @ chris2.bpl(12,28) Execution trace: chris2.bpl(12,28): inline$atomic_p_gt1$0$Entry chris2.bpl(14,5): inline$atomic_p_gt1$0$anon0 chris2.bpl(12,28): inline$atomic_p_gt1$0$Return -chris2.bpl(22,28): Error: Gate failure of atomic_p_gt2 not preserved by atomic_p_gt1_lower +chris2.bpl(23,3): Error: Gate failure of atomic_p_gt2 @ chris2.bpl(22,28) not preserved by atomic_p_gt1_lower @ chris2.bpl(5,28) Execution trace: - chris2.bpl(5,28): inline$atomic_p_gt1_lower$0$Entry - chris2.bpl(7,5): inline$atomic_p_gt1_lower$0$anon0 - chris2.bpl(5,28): inline$atomic_p_gt1_lower$0$Return -chris2.bpl(22,28): Error: Gate failure of atomic_p_gt2 not preserved by atomic_p_gt1 + (0,0): init +chris2.bpl(23,3): Error: Gate failure of atomic_p_gt2 @ chris2.bpl(22,28) not preserved by atomic_p_gt1 @ chris2.bpl(12,28) Execution trace: - chris2.bpl(12,28): inline$atomic_p_gt1$0$Entry - chris2.bpl(14,5): inline$atomic_p_gt1$0$anon0 - chris2.bpl(12,28): inline$atomic_p_gt1$0$Return + (0,0): init Boogie program verifier finished with 1 verified, 4 errors diff --git a/Test/civl/regression-tests/cyclic-concur.bpl b/Test/civl/regression-tests/cyclic-concur.bpl index b19407551..5899b0c4e 100644 --- a/Test/civl/regression-tests/cyclic-concur.bpl +++ b/Test/civl/regression-tests/cyclic-concur.bpl @@ -5,8 +5,10 @@ var {:layer 0,2} x : int; atomic action {:layer 2} MAIN () modifies x; { - havoc x; - assume x > old(x) && (x - old(x)) mod 6 == 0; + var next_x: int; + + assume next_x > x && (next_x - x) mod 6 == 0; + x := next_x; } diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect index 1a747e1d9..8a32f0857 100644 --- a/Test/civl/regression-tests/intro-nonblocking.bpl.expect +++ b/Test/civl/regression-tests/intro-nonblocking.bpl.expect @@ -1,4 +1,4 @@ -intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed +intro-nonblocking.bpl(4,13): Error: Nonblocking check for intro failed Execution trace: (0,0): init diff --git a/Test/civl/regression-tests/left-mover.bpl.expect b/Test/civl/regression-tests/left-mover.bpl.expect index 44ada71cb..10c5729da 100644 --- a/Test/civl/regression-tests/left-mover.bpl.expect +++ b/Test/civl/regression-tests/left-mover.bpl.expect @@ -1,14 +1,12 @@ -left-mover.bpl(11,26): Error: Gate failure of ass_eq_1 not preserved by inc +left-mover.bpl(12,3): Error: Gate failure of ass_eq_1 @ left-mover.bpl(11,26) not preserved by inc @ left-mover.bpl(6,24) Execution trace: - left-mover.bpl(6,24): inline$inc$0$Entry - left-mover.bpl(8,5): inline$inc$0$anon0 - left-mover.bpl(6,24): inline$inc$0$Return -left-mover.bpl(19,26): Error: Commutativity check between init and inc failed + (0,0): init +left-mover.bpl(19,26): Error: Commutativity check between init @ left-mover.bpl(19,26) and inc @ left-mover.bpl(6,24) failed Execution trace: left-mover.bpl(19,26): inline$init$0$Entry left-mover.bpl(8,5): inline$inc$0$anon0 left-mover.bpl(6,24): inline$inc$0$Return -left-mover.bpl(26,24): Error: Cooperation check for block failed +left-mover.bpl(26,24): Error: Nonblocking check for block failed Execution trace: (0,0): init diff --git a/Test/civl/regression-tests/linearity-bug-1.bpl.expect b/Test/civl/regression-tests/linearity-bug-1.bpl.expect index 392d9f2fe..9af9ab81e 100644 --- a/Test/civl/regression-tests/linearity-bug-1.bpl.expect +++ b/Test/civl/regression-tests/linearity-bug-1.bpl.expect @@ -1,4 +1,4 @@ -linearity-bug-1.bpl(20,25): Error: Commutativity check between atomic_read_n and atomic_inc_n failed +linearity-bug-1.bpl(20,25): Error: Commutativity check between atomic_read_n @ linearity-bug-1.bpl(20,25) and atomic_inc_n @ linearity-bug-1.bpl(13,26) failed Execution trace: linearity-bug-1.bpl(20,25): inline$atomic_read_n$0$Entry linearity-bug-1.bpl(15,3): inline$atomic_inc_n$0$anon0 diff --git a/Test/civl/samples/array-insert.bpl b/Test/civl/samples/array-insert.bpl index 490827f6c..0fb21c791 100644 --- a/Test/civl/samples/array-insert.bpl +++ b/Test/civl/samples/array-insert.bpl @@ -17,6 +17,7 @@ atomic action {:layer 2} INSERT ({:linear} tid: One Tid, v:int) modifies A, count; { var idx:int; // index at which v is written + var old_A: [int]int; assert count >= 0; assert sorted(A, count); @@ -25,11 +26,12 @@ modifies A, count; assume (forall i:int :: 0 <= i && i < idx ==> A[i] < v); assume (forall i:int :: idx <= i && i < count ==> A[i] >= v); + old_A := A; havoc A; - assume (forall i:int :: i < idx ==> A[i] == old(A)[i]); - assume (forall i:int :: idx < i && i < count ==> A[i+1] == old(A)[i]); - assume (forall i:int :: count < i ==> A[i] == old(A)[i]); + assume (forall i:int :: i < idx ==> A[i] == old_A[i]); + assume (forall i:int :: idx < i && i < count ==> A[i+1] == old_A[i]); + assume (forall i:int :: count < i ==> A[i] == old_A[i]); assume A[idx] == v; count := count + 1;