From 1b8d9637600e5e0c6fd59e5a760f323c5380ed13 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 22 Jul 2024 09:59:07 -0700 Subject: [PATCH] [Civl] Eliminated linearity checks in favor of local checks (#914) --- Source/Concurrency/CivlCoreTypes.cs | 45 ++-- Source/Concurrency/CivlRewriter.cs | 3 - Source/Concurrency/CivlTypeChecker.cs | 4 +- .../Concurrency/InductiveSequentialization.cs | 28 ++- Source/Concurrency/LinearRewriter.cs | 96 ++++++++ Source/Concurrency/LinearTypeChecker.cs | 96 ++++++++ Source/Concurrency/LinearityChecker.cs | 232 ------------------ Source/Core/AST/CallCmd.cs | 25 +- Source/Core/CivlAttributes.cs | 2 +- Source/Core/Inline.cs | 3 +- Test/civl/async/async3.bpl | 2 +- Test/civl/async/lock-service.bpl | 2 +- Test/civl/async/lock-service.bpl.expect | 2 +- Test/civl/inductive-sequentialization/2PC.bpl | 66 ++++- .../2PC.bpl.expect | 2 +- .../BroadcastConsensus.bpl | 52 ++-- .../BroadcastConsensus.bpl.expect | 2 +- .../ChangRoberts.bpl | 6 +- .../inductive-sequentialization/NoChoice.bpl | 4 +- .../inductive-sequentialization/PingPong.bpl | 37 ++- .../PingPong.bpl.expect | 2 +- .../ProducerConsumer.bpl | 37 ++- .../ProducerConsumer.bpl.expect | 2 +- .../snapshot-IS2-part.bpl | 74 ------ .../snapshot-IS2-part.bpl.expect | 2 - .../snapshot-scatter-gather.bpl | 201 --------------- .../snapshot-scatter-gather.bpl.expect | 2 - Test/civl/paxos/Paxos.bpl | 5 + Test/civl/paxos/PaxosActions.bpl | 27 +- Test/civl/paxos/PaxosSeq.bpl | 43 ++-- .../regression-tests/hide-params-pa-2.bpl | 2 +- Test/civl/regression-tests/is2-attributes.bpl | 12 +- .../regression-tests/only-async-call-ISR.bpl | 4 +- .../pa-noninterference-check.bpl | 2 +- .../civl/regression-tests/pending-async-1.bpl | 6 +- .../pending-async-1.bpl.expect | 6 +- .../civl/regression-tests/pending-async-2.bpl | 4 +- .../pending-async-2.bpl.expect | 2 +- .../pending-async-linearity.bpl | 70 ------ .../pending-async-linearity.bpl.expect | 27 -- .../pending-async-noninterference-fail.bpl | 2 +- .../pending-async-noninterference-linear.bpl | 2 +- ...ng-async-noninterference-linear.bpl.expect | 2 +- .../pending-async-noninterference-ok.bpl | 2 +- Test/civl/regression-tests/rec-IS1.bpl | 6 +- Test/civl/regression-tests/rec-IS1.bpl.expect | 2 +- 46 files changed, 497 insertions(+), 758 deletions(-) delete mode 100644 Source/Concurrency/LinearityChecker.cs delete mode 100644 Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl delete mode 100644 Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl.expect delete mode 100644 Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl delete mode 100644 Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl.expect delete mode 100644 Test/civl/regression-tests/pending-async-linearity.bpl delete mode 100644 Test/civl/regression-tests/pending-async-linearity.bpl.expect diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs index 977983670..b4b9d26b4 100644 --- a/Source/Concurrency/CivlCoreTypes.cs +++ b/Source/Concurrency/CivlCoreTypes.cs @@ -49,7 +49,7 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl); DesugarSetChoice(civlTypeChecker, ImplWithChoice); } - DropSetChoice(civlTypeChecker, Impl); + DropSetChoice(Impl); } ModifiedGlobalVars = new HashSet(Impl.Proc.Modifies.Select(x => x.Decl)); @@ -176,19 +176,24 @@ private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeCh return; } + var gateSubst = Substituter.SubstitutionFromDictionary(ActionDecl.InParams + .Zip(Impl.InParams) + .ToDictionary(x => x.Item1, x => (Expr)Expr.Ident(x.Item2))); + var checkerName = $"{Name}_GateSufficiencyChecker"; - var checkerImpl = new Duplicator().VisitImplementation(ActionDecl.Impl); + var checkerImpl = new Duplicator().VisitImplementation(Impl); checkerImpl.Name = checkerName; checkerImpl.Attributes = null; + var requires = ActionDecl.Requires.Select( + requires => new Requires(requires.tok, requires.Free, Substituter.Apply(gateSubst, requires.Condition), + null, CivlAttributes.ApplySubstitutionToPoolHints(gateSubst, requires.Attributes))).ToList(); var proc = checkerImpl.Proc; checkerImpl.Proc = new Procedure(proc.tok, checkerName, proc.TypeParameters, proc.InParams, - proc.OutParams, proc.IsPure, proc.Requires, proc.Modifies, proc.Ensures); + proc.OutParams, proc.IsPure, requires, proc.Modifies, new List()); gateSufficiencyCheckerDecls.AddRange(new Declaration[] { checkerImpl.Proc, checkerImpl }); HoistAsserts(Impl, civlTypeChecker.Options); - var gateSubst = Substituter.SubstitutionFromDictionary(ActionDecl.InParams - .Zip(Impl.InParams) - .ToDictionary(x => x.Item1, x => (Expr)Expr.Ident(x.Item2))); + Gate = ActionDecl.Requires.Select( requires => new AssertCmd(requires.tok, Substituter.Apply(gateSubst, requires.Condition), CivlAttributes.ApplySubstitutionToPoolHints(gateSubst, requires.Attributes))).ToList(); @@ -256,15 +261,28 @@ public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implemen if (cmd is CallCmd callCmd) { var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(callCmd.Proc); - if (originalProc.Name == "create_async" || originalProc.Name == "create_asyncs" || originalProc.Name == "create_multi_asyncs") + if (callCmd.IsAsync) + { + var actionDecl = (ActionDecl)callCmd.Proc; + var pendingAsyncMultiset = + Expr.Store( + ExprHelper.FunctionCall(actionDecl.PendingAsyncConst, Expr.Literal(0)), + ExprHelper.FunctionCall(actionDecl.PendingAsyncCtor, callCmd.Ins), + Expr.Literal(1)); + var pendingAsyncMultisetType = TypeHelper.MapType(actionDecl.PendingAsyncType, Type.Int); + var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType)); + var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector, + ExprHelper.FunctionCall(actionDecl.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset)); + updateAssignCmd.Typecheck(tc); + newCmds.Add(updateAssignCmd); + continue; + } + else if (originalProc.Name == "create_asyncs" || originalProc.Name == "create_multi_asyncs") { var pendingAsyncType = (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; var pendingAsync = pendingAsyncTypeToActionDecl[pendingAsyncType]; - var pendingAsyncMultiset = originalProc.Name == "create_async" - ? Expr.Store(ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0)), callCmd.Ins[0], - Expr.Literal(1)) - : originalProc.Name == "create_asyncs" + var pendingAsyncMultiset = originalProc.Name == "create_asyncs" ? ExprHelper.FunctionCall(pendingAsync.PendingAsyncIte, callCmd.Ins[0], ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(1)), ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0))) @@ -272,8 +290,7 @@ public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implemen var pendingAsyncMultisetType = TypeHelper.MapType(pendingAsyncType, Type.Int); var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType)); var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector, - ExprHelper.FunctionCall(pendingAsync.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), - pendingAsyncMultiset)); + ExprHelper.FunctionCall(pendingAsync.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset)); updateAssignCmd.Typecheck(tc); newCmds.Add(updateAssignCmd); continue; @@ -285,7 +302,7 @@ public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implemen }); } - private void DropSetChoice(CivlTypeChecker civlTypeChecker, Implementation impl) + private void DropSetChoice(Implementation impl) { impl.Blocks.ForEach(block => { diff --git a/Source/Concurrency/CivlRewriter.cs b/Source/Concurrency/CivlRewriter.cs index d7a787bb4..dcf9bfa35 100644 --- a/Source/Concurrency/CivlRewriter.cs +++ b/Source/Concurrency/CivlRewriter.cs @@ -45,9 +45,6 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp // Desugaring of yielding procedures YieldingProcChecker.AddCheckers(civlTypeChecker, decls); - // Linear type checks - LinearityChecker.AddCheckers(civlTypeChecker, decls); - if (!options.TrustSequentialization) { Sequentialization.AddCheckers(civlTypeChecker, decls); diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 59394cee8..97ccab95f 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -132,7 +132,7 @@ private HashSet TypeCheckActions() { foreach (var block in actionDecl.Impl.Blocks) { - foreach (var callCmd in block.Cmds.OfType()) + foreach (var callCmd in block.Cmds.OfType().Where(callCmd => !callCmd.IsAsync)) { callGraph.AddEdge(actionDecl, callCmd.Proc); } @@ -220,7 +220,7 @@ private void CheckAsyncToSyncSafety(ActionDecl actionDecl, HashSet refin for (int i = block.Cmds.Count - 1; 0 <= i; i--) { var cmd = block.Cmds[i]; - if (modifiedGlobals && cmd is CallCmd callCmd && callCmd.Proc.OriginalDeclWithFormals is { Name: "create_async" }) + if (modifiedGlobals && cmd is CallCmd callCmd && callCmd.IsAsync) { var pendingAsyncType = (CtorType)program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; if (!refinedActionCreateNames.Contains(pendingAsyncType.Decl.Name)) diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs index 8ed8857d2..dcad2b88d 100644 --- a/Source/Concurrency/InductiveSequentialization.cs +++ b/Source/Concurrency/InductiveSequentialization.cs @@ -5,6 +5,24 @@ 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, @@ -292,16 +310,14 @@ private Implementation CreateInlinedImplementation() private Cmd Transform(Dictionary eliminatedPendingAsyncs, Cmd cmd, HashSet modifies) { - if (cmd is CallCmd callCmd && callCmd.Proc.OriginalDeclWithFormals is { Name: "create_async" }) + if (cmd is CallCmd callCmd && callCmd.IsAsync) { - var pendingAsyncType = (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; - var datatypeTypeCtorDecl = (DatatypeTypeCtorDecl)pendingAsyncType.Decl; + var actionDecl = (ActionDecl)callCmd.Proc; + var pendingAsyncType = actionDecl.PendingAsyncType; if (eliminatedPendingAsyncs.ContainsKey(pendingAsyncType)) { var newCallee = eliminatedPendingAsyncs[pendingAsyncType].Proc; - var newIns = datatypeTypeCtorDecl.Constructors[0].InParams - .Select(x => (Expr)ExprHelper.FieldAccess(callCmd.Ins[0], x.Name)).ToList(); - var newCallCmd = new CallCmd(callCmd.tok, newCallee.Name, newIns, new List()) + var newCallCmd = new CallCmd(callCmd.tok, newCallee.Name, callCmd.Ins, new List()) { Proc = newCallee }; diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index da6fbd404..c1aac53c6 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Boogie; @@ -41,6 +42,11 @@ private List RewriteCmdSeq(List cmdSeq) { newCmdSeq.AddRange(RewriteCallCmd(callCmd)); } + else if (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name == "create_asyncs") + { + newCmdSeq.AddRange(PreconditionsForCreateAsyncs(callCmd)); + newCmdSeq.Add(cmd); + } else { newCmdSeq.Add(cmd); @@ -54,6 +60,91 @@ private List RewriteCmdSeq(List cmdSeq) return newCmdSeq; } + private List PreconditionsForCreateAsyncs(CallCmd callCmd) + { + var cmds = new List(); + var attr = QKeyValue.FindAttribute(callCmd.Attributes, x => x.Key == "linear"); + if (attr == null) + { + return cmds; + } + + var sources = attr.Params.OfType(); + var pendingAsyncType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; + var actionDecl = civlTypeChecker.linearTypeChecker.GetActionDeclFromCreateAsyncs(callCmd); + var iter = Enumerable.Range(0, actionDecl.InParams.Count).Where(i => { + var inParam = actionDecl.InParams[i]; + if (LinearTypeChecker.FindLinearKind(inParam) == LinearKind.ORDINARY) + { + return false; + } + if (inParam.TypedIdent.Type is not CtorType ctorType) + { + return false; + } + var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); + return originalTypeCtorDecl.Name == "One" || originalTypeCtorDecl.Name == "Set"; + }); + var datatypeTypeCtorDecl = (DatatypeTypeCtorDecl) actionDecl.PendingAsyncType.Decl; + var constructor = datatypeTypeCtorDecl.Constructors[0]; + + var paVar = civlTypeChecker.BoundVariable("pa", actionDecl.PendingAsyncType); + var containsExpr = NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar)); + var containsCheckExprs = iter.Zip(sources).Select(kv => { + var i = kv.First; + var sourceExpr = kv.Second; + var inParam = actionDecl.InParams[i]; + var ctorType = (CtorType)inParam.TypedIdent.Type; + var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); + var instanceType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl)[0]; + var fieldAccess = ExprHelper.FieldAccess(Expr.Ident(paVar), constructor.InParams[i].Name); + if (originalTypeCtorDecl.Name == "One") + { + fieldAccess = ExprHelper.FieldAccess(fieldAccess, "val"); + return ExprHelper.FunctionCall(SetContains(instanceType), sourceExpr, fieldAccess); + } + else + { + return ExprHelper.FunctionCall(SetIsSubset(instanceType), fieldAccess, sourceExpr); + } + }); + var containsCheckExpr = ExprHelper.ForallExpr( + new List(){ paVar }, + Expr.Imp(containsExpr, Expr.And(containsCheckExprs))); + cmds.Add(CmdHelper.AssertCmd(callCmd.tok, containsCheckExpr, "Contains check failed")); + + var paVar1 = civlTypeChecker.BoundVariable("pa1", actionDecl.PendingAsyncType); + var paVar2 = civlTypeChecker.BoundVariable("pa2", actionDecl.PendingAsyncType); + var guardExprs = new List() { + NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar1)), + NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar2)), + Expr.Neq(Expr.Ident(paVar1), Expr.Ident(paVar2)) + }; + var distinctCheckExprs = iter.Select(i => { + var inParam = actionDecl.InParams[i]; + var ctorType = (CtorType)inParam.TypedIdent.Type; + var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); + var instanceType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl)[0]; + var fieldAccess1 = ExprHelper.FieldAccess(Expr.Ident(paVar1), constructor.InParams[i].Name); + var fieldAccess2 = ExprHelper.FieldAccess(Expr.Ident(paVar2), constructor.InParams[i].Name); + if (originalTypeCtorDecl.Name == "One") + { + return Expr.Neq(fieldAccess1, fieldAccess2); + } + else + { + return ExprHelper.FunctionCall(SetIsDisjoint(instanceType), fieldAccess1, fieldAccess2); + } + }); + var distinctCheckExpr = ExprHelper.ForallExpr( + new List(){ paVar1, paVar2 }, + Expr.Imp(Expr.And(guardExprs), Expr.And(distinctCheckExprs))); + cmds.Add(CmdHelper.AssertCmd(callCmd.tok, distinctCheckExpr, "Distinct check failed")); + + ResolveAndTypecheck(options, cmds); + return cmds; + } + public List RewriteCallCmd(CallCmd callCmd) { switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) @@ -122,6 +213,11 @@ private Function SetIsSubset(Type type) return monomorphizer.InstantiateFunction("Set_IsSubset", new Dictionary() { { "T", type } }); } + private Function SetIsDisjoint(Type type) + { + return monomorphizer.InstantiateFunction("Set_IsDisjoint",new Dictionary() { { "T", type } }); + } + private Function SetAdd(Type type) { return monomorphizer.InstantiateFunction("Set_Add",new Dictionary() { { "T", type } }); diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index d5fb1e2e9..112758517 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -11,6 +11,7 @@ public class LinearTypeChecker : ReadOnlyVisitor public Program program; private CheckingContext checkingContext; private CivlTypeChecker civlTypeChecker; + private Dictionary pendingAsyncTypeToActionDecl; private Dictionary permissionTypeToLinearDomain; private Dictionary> collectors; private Dictionary> availableLinearVars; @@ -20,6 +21,11 @@ public LinearTypeChecker(CivlTypeChecker civlTypeChecker) this.civlTypeChecker = civlTypeChecker; this.program = civlTypeChecker.program; this.checkingContext = civlTypeChecker.checkingContext; + this.pendingAsyncTypeToActionDecl = new (); + foreach (var actionDecl in program.TopLevelDeclarations.OfType().Where(actionDecl => actionDecl.MaybePendingAsync)) + { + pendingAsyncTypeToActionDecl[actionDecl.PendingAsyncType] = actionDecl; + } // other fields are initialized in the TypeCheck method } @@ -220,6 +226,24 @@ private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) Error(ie, $"unavailable source {ie} for linear parameter at position {i}"); } } + var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(callCmd.Proc); + if (originalProc.Name == "create_asyncs") + { + var attr = QKeyValue.FindAttribute(callCmd.Attributes, x => x.Key == "linear"); + if (attr != null) + { + attr.Params.OfType().ForEach(ie => { + if (start.Contains(ie.Decl)) + { + start.Remove(ie.Decl); + } + else + { + Error(ie, $"unavailable linear source"); + } + }); + } + } AddAvailableVars(callCmd, start); availableLinearVars[callCmd] = new HashSet(start); } @@ -593,6 +617,72 @@ enclosingProc is not YieldProcedureDecl && } } } + + var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(node.Proc); + if (originalProc.Name == "create_multi_asyncs" || originalProc.Name == "create_asyncs") + { + var actionDecl = GetActionDeclFromCreateAsyncs(node); + if (originalProc.Name == "create_multi_asyncs") + { + foreach (var inParam in actionDecl.InParams.Where(inParam => FindLinearKind(inParam) != LinearKind.ORDINARY)) + { + Error(node, $"linear parameters not allowed on pending async"); + } + } + else if (originalProc.Name == "create_asyncs") + { + var linearArgumentTypes = new List(); + foreach (var inParam in actionDecl.InParams.Where(inParam => FindLinearKind(inParam) != LinearKind.ORDINARY)) + { + if (inParam.TypedIdent.Type is CtorType ctorType) + { + var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); + if (originalTypeCtorDecl.Name == "One") + { + var typeInstantiation = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl); + var setType = TypeHelper.CtorType(civlTypeChecker.program.monomorphizer.InstantiateTypeCtorDecl("Set", typeInstantiation)); + linearArgumentTypes.Add(setType); + continue; + } + else if (originalTypeCtorDecl.Name == "Set") + { + linearArgumentTypes.Add(ctorType); + continue; + } + } + Error(node, $"linear parameter must be of type One or Set"); + } + var attr = QKeyValue.FindAttribute(node.Attributes, x => x.Key == "linear"); + var attrParams = attr == null ? new List() : attr.Params; + var identifierExprs = attrParams.OfType().ToList(); + if (identifierExprs.Count != attrParams.Count()) + { + Error(node, $"each linear source must be a variable"); + } + else if (identifierExprs.Count != linearArgumentTypes.Count) + { + Error(node, $"number of linear sources must match the number of linear parameters"); + } + else + { + foreach (var (ie, type) in identifierExprs.Zip(linearArgumentTypes)) + { + if (ie.Decl is LocalVariable || ie.Decl is Formal) + { + if (!ie.Decl.TypedIdent.Type.Equals(type)) + { + Error(ie, $"expected type {type}"); + } + } + else + { + Error(ie, $"expected local or formal variable"); + } + } + } + } + } + return base.VisitCallCmd(node); } @@ -901,6 +991,12 @@ private Function MapWellFormedFunction(Monomorphizer monomorphizer, TypeCtorDecl return monomorphizer.InstantiateFunction("Map_WellFormed", typeParamInstantiationMap); } + public ActionDecl GetActionDeclFromCreateAsyncs(CallCmd callCmd) + { + var pendingAsyncType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; + return pendingAsyncTypeToActionDecl[pendingAsyncType]; + } + #endregion #region Annotation Eraser diff --git a/Source/Concurrency/LinearityChecker.cs b/Source/Concurrency/LinearityChecker.cs deleted file mode 100644 index 664265f71..000000000 --- a/Source/Concurrency/LinearityChecker.cs +++ /dev/null @@ -1,232 +0,0 @@ -using System.Collections.Generic; -using System.Linq; - -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; - } -} - -class LinearityChecker -{ - private CivlTypeChecker civlTypeChecker; - private LinearTypeChecker linearTypeChecker => civlTypeChecker.linearTypeChecker; - - private LinearityChecker(CivlTypeChecker civlTypeChecker) - { - this.civlTypeChecker = civlTypeChecker; - } - - public static void AddCheckers(CivlTypeChecker civlTypeChecker, List decls) - { - var linearityChecker = new LinearityChecker(civlTypeChecker); - foreach (var action in civlTypeChecker.MoverActions) - { - linearityChecker.AddChecker(action, decls); - } - } - - private IdentifierExpr PAs(Action action, int pendingAsyncIndex) - { - return Expr.Ident(action.Impl.OutParams[action.PendingAsyncStartIndex + pendingAsyncIndex]); - } - - private void AddChecker(Action action, List decls) - { - if (action is not Action { HasPendingAsyncs: true } atomicAction) - { - return; - } - var pendingAsyncs = new List(atomicAction.PendingAsyncs); - // Note: The implementation should be used as the variables in the - // gate are bound to implementation and not to the procedure. - Implementation impl = action.Impl; - List inputs = impl.InParams; - List outputs = impl.OutParams; - - var locals = new List(); - var ctorTypeToFirstPA = new Dictionary(); - var ctorTypeToSecondPA = new Dictionary(); - pendingAsyncs.ForEach(y => - { - var paLocal1 = civlTypeChecker.LocalVariable($"pa1_{y.PendingAsyncType.Decl.Name}", y.PendingAsyncType); - var paLocal2 = civlTypeChecker.LocalVariable($"pa2_{y.PendingAsyncType.Decl.Name}", y.PendingAsyncType); - locals.Add(paLocal1); - locals.Add(paLocal2); - ctorTypeToFirstPA[y.PendingAsyncType] = Expr.Ident(paLocal1); - ctorTypeToSecondPA[y.PendingAsyncType] = Expr.Ident(paLocal2); - }); - - // Linear in vars - var inVars = inputs.Union(action.ModifiedGlobalVars) - .Where(x => LinearTypeChecker.InKinds.Contains(LinearTypeChecker.FindLinearKind(x))) - .Select(Expr.Ident).ToList(); - // Linear out vars - var outVars = inputs.Union(outputs).Union(action.ModifiedGlobalVars) - .Where(x => LinearTypeChecker.OutKinds.Contains(LinearTypeChecker.FindLinearKind(x))) - .Select(Expr.Ident).ToList(); - - var inputDisjointnessExprs = linearTypeChecker.DisjointnessExprForEachDomain( - inputs.Union(action.ModifiedGlobalVars) - .Where(x => LinearTypeChecker.InKinds.Contains(LinearTypeChecker.FindLinearKind(x)))); - List requires = action.Gate.Select(a => new Requires(false, a.Expr)) - .Concat(inputDisjointnessExprs.Select(expr => new Requires(false, expr))) - .ToList(); - - List linearityChecks = new List(); - foreach (var domain in linearTypeChecker.LinearDomains) - { - for (int i = 0; i < pendingAsyncs.Count; i++) - { - var pendingAsync = pendingAsyncs[i]; - var pa1 = ctorTypeToFirstPA[pendingAsync.PendingAsyncType]; - var pa2 = ctorTypeToSecondPA[pendingAsync.PendingAsyncType]; - var pendingAsyncLinearParams = PendingAsyncLinearParams(pendingAsync, pa1); - - if (pendingAsyncLinearParams.Count == 0) - { - continue; - } - - // First kind - // Input permission of a pending async is a subset of permissions in input variables. - var existingExpr = Expr.And( - ExprHelper.IsConstructor(pa1, pendingAsync.PendingAsyncCtor.Name), - Expr.Ge(Expr.Select(PAs(atomicAction, i), pa1), Expr.Literal(1))); - var outSubsetInExpr = OutPermsSubsetInPerms(domain, inVars, pendingAsyncLinearParams); - linearityChecks.Add(new LinearityCheck( - domain, - existingExpr, - outSubsetInExpr, - $"Out-of-thin-air permissions of type {domain.permissionType} in pending async of {pendingAsync.Name}", - $"out_of_thin_air_{pendingAsync.Name}")); - - // Second kind - // Input permission of a pending async is disjoint from permissions in output variables. - var noDuplicationExpr = DisjointPerms(domain, outVars, pendingAsyncLinearParams); - linearityChecks.Add(new LinearityCheck( - domain, - existingExpr, - noDuplicationExpr, - $"Duplication of permissions of type {domain.permissionType} in calling context (globals, linear outputs, or linear/linear_out inputs) and pending async of {pendingAsync.Name}", - $"duplication_{pendingAsync.Name}")); - } - - for (int i = 0; i < pendingAsyncs.Count; i++) - { - var pendingAsync1 = pendingAsyncs[i]; - var pa1 = ctorTypeToFirstPA[pendingAsync1.PendingAsyncType]; - for (int j = i; j < pendingAsyncs.Count; j++) - { - var pendingAsync2 = pendingAsyncs[j]; - var pa2 = ctorTypeToSecondPA[pendingAsync2.PendingAsyncType]; - var pendingAsyncLinearParams1 = PendingAsyncLinearParams(pendingAsync1, pa1); - var pendingAsyncLinearParams2 = PendingAsyncLinearParams(pendingAsync2, pa2); - - if (pendingAsyncLinearParams1.Count == 0 || pendingAsyncLinearParams2.Count == 0) - { - continue; - } - - // Third kind - // Input permissions of two pending asyncs (possibly of the same action) are disjoint. - var membershipExpr = Expr.And( - i == j ? Expr.Neq(pa1, pa2) : Expr.True, - Expr.And( - ExprHelper.IsConstructor(pa1, pendingAsync1.PendingAsyncCtor.Name), - ExprHelper.IsConstructor(pa2, pendingAsync2.PendingAsyncCtor.Name))); - - var existingExpr = Expr.And( - Expr.Ge(Expr.Select(PAs(atomicAction, i), pa1), Expr.Literal(1)), - Expr.Ge(Expr.Select(PAs(atomicAction, j), pa2), Expr.Literal(1))); - - var noDuplicationExpr = DisjointPerms(domain, pendingAsyncLinearParams1, pendingAsyncLinearParams2); - - linearityChecks.Add(new LinearityCheck( - domain, - Expr.And(membershipExpr, existingExpr), - noDuplicationExpr, - $"Duplication of permissions of type {domain.permissionType} in pending asyncs of {pendingAsync1.Name} and {pendingAsync2.Name}", - $"duplication_{pendingAsync1.Name}_{pendingAsync2.Name}")); - } - } - } - - if (linearityChecks.Count == 0) - { - return; - } - - // Create checker blocks - List checkerBlocks = new List(linearityChecks.Count); - foreach (var lc in linearityChecks) - { - List cmds = new List(2); - if (lc.assume != null) - { - cmds.Add(CmdHelper.AssumeCmd(lc.assume)); - } - cmds.Add(CmdHelper.AssertCmd(action.tok, lc.assert, lc.message)); - var block = BlockHelper.Block($"{lc.domain.permissionType}_{lc.checkName}", cmds); - CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, block, ResolutionContext.State.Two); - checkerBlocks.Add(block); - } - - // Create init blocks - List blocks = new List(linearityChecks.Count + 1); - blocks.Add( - BlockHelper.Block( - "init", - new List() { CmdHelper.CallCmd(action.Impl.Proc, inputs, outputs) }, - checkerBlocks)); - blocks.AddRange(checkerBlocks); - - // Create the whole check procedure - string checkerName = civlTypeChecker.AddNamePrefix($"LinearityChecker_{action.Name}"); - Procedure linCheckerProc = DeclHelper.Procedure(checkerName, - inputs, outputs, requires, action.Impl.Proc.Modifies, new List()); - Implementation linCheckImpl = DeclHelper.Implementation(linCheckerProc, - inputs, outputs, locals, blocks); - decls.Add(linCheckImpl); - decls.Add(linCheckerProc); - } - - private List PendingAsyncLinearParams(ActionDecl pendingAsync, IdentifierExpr pa) - { - var pendingAsyncLinearParams = pendingAsync.InParams - .Where(v => LinearTypeChecker.InKinds.Contains(LinearTypeChecker.FindLinearKind(v))) - .Select(v => ExprHelper.FieldAccess(pa, v.Name)).ToList(); - // These expressions must be typechecked since the types are needed later in PermissionMultiset. - CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, pendingAsyncLinearParams); - return pendingAsyncLinearParams; - } - - private Expr OutPermsSubsetInPerms(LinearDomain domain, IEnumerable ins, IEnumerable outs) - { - var inPermissionSet = ExprHelper.Old(linearTypeChecker.UnionExprForPermissions(domain, linearTypeChecker.PermissionExprs(domain, ins))); - var outPermissionSet = linearTypeChecker.UnionExprForPermissions(domain, linearTypeChecker.PermissionExprs(domain, outs)); - return linearTypeChecker.SubsetExprForPermissions(domain, outPermissionSet, inPermissionSet); - } - - private Expr DisjointPerms(LinearDomain domain, IEnumerable set1, IEnumerable set2) { - var expr1 = linearTypeChecker.UnionExprForPermissions(domain, linearTypeChecker.PermissionExprs(domain, set1)); - var expr2 = linearTypeChecker.UnionExprForPermissions(domain, linearTypeChecker.PermissionExprs(domain, set2)); - return Expr.Eq( - ExprHelper.FunctionCall(domain.mapAnd, expr1, expr2), - ExprHelper.FunctionCall(domain.mapConstBool, Expr.False)); - } -} \ No newline at end of file diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs index 7f9d377e1..1fd4cab7a 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/CallCmd.cs @@ -254,13 +254,23 @@ public override void Resolve(ResolutionContext rc) } if (IsAsync) { - if (rc.Proc is not YieldProcedureDecl) + if (rc.Proc is ActionDecl) { - rc.Error(this, "calling procedure of an async call must yield"); + if (Proc is not ActionDecl) + { + rc.Error(this, "target of async call must be an action"); + } } - if (Proc is not YieldProcedureDecl) + else if (rc.Proc is YieldProcedureDecl) { - rc.Error(this, "target procedure of an async call must yield"); + if (Proc is not YieldProcedureDecl) + { + rc.Error(this, "target of async call must be a yield procedure"); + } + } + else + { + rc.Error(this, "async call allowed only from a yield procedure or an action"); } } // checking calls from atomic actions need type information, hence postponed to type checking @@ -470,6 +480,13 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc) { // ok } + else if (IsAsync) + { + if (callerActionDecl.Creates.All(x => x.ActionName != Proc.Name)) + { + tc.Error(this, "pending async must be in the creates clause of caller"); + } + } else if (CivlPrimitives.Async.Contains(Proc.Name)) { var type = TypeProxy.FollowProxy(TypeParameters[Proc.TypeParameters[0]].Expanded); diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index ed3b51888..5c86ee686 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -257,7 +257,7 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) public static HashSet Async = new() { - "create_async", "create_asyncs", "create_multi_asyncs", "set_choice" + "create_asyncs", "create_multi_asyncs", "set_choice" }; } } diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 2c4361d8d..e649a3c3f 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -372,9 +372,8 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis { Cmd cmd = cmds[i]; - if (cmd is CallCmd) + if (cmd is CallCmd callCmd && !callCmd.IsAsync) { - CallCmd callCmd = (CallCmd) cmd; Implementation impl = FindProcImpl(program, callCmd.Proc); if (impl == null) { diff --git a/Test/civl/async/async3.bpl b/Test/civl/async/async3.bpl index 1a89e8fd9..23410343a 100644 --- a/Test/civl/async/async3.bpl +++ b/Test/civl/async/async3.bpl @@ -13,7 +13,7 @@ atomic action {:layer 1} A_Service() refines A_Inc; creates A_Inc; { - call create_async(A_Inc()); + async call A_Inc(); } yield procedure {:layer 0} Service () refines A_Service; diff --git a/Test/civl/async/lock-service.bpl b/Test/civl/async/lock-service.bpl index bef8be763..d3bce276e 100644 --- a/Test/civl/async/lock-service.bpl +++ b/Test/civl/async/lock-service.bpl @@ -77,7 +77,7 @@ modifies l; assert tid->val != nil; assume l == nil; l := tid->val; - call create_async(A_Callback(tid)); + async call A_Callback(tid); } yield procedure {:layer 2} GetLockAndCallback ({:linear_in} tid: One Tid) refines A_GetLockAndCallback; diff --git a/Test/civl/async/lock-service.bpl.expect b/Test/civl/async/lock-service.bpl.expect index b76b1aea8..fdd1a2438 100644 --- a/Test/civl/async/lock-service.bpl.expect +++ b/Test/civl/async/lock-service.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 34 verified, 0 errors +Boogie program verifier finished with 33 verified, 0 errors diff --git a/Test/civl/inductive-sequentialization/2PC.bpl b/Test/civl/inductive-sequentialization/2PC.bpl index 6bbb82feb..99509bc77 100644 --- a/Test/civl/inductive-sequentialization/2PC.bpl +++ b/Test/civl/inductive-sequentialization/2PC.bpl @@ -60,6 +60,8 @@ 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); @@ -73,7 +75,10 @@ modifies RequestChannel, VoteChannel, DecisionChannel, votes, decisions; (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)); - call create_asyncs((lambda {:pool "PARTICIPANT2"} pa:PARTICIPANT2 :: pidGt(pa->pid->val, k))); + + 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))); } @@ -88,6 +93,9 @@ 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; @@ -96,7 +104,9 @@ modifies RequestChannel, VoteChannel, DecisionChannel, votes, decisions; 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)); - call create_asyncs((lambda pa:PARTICIPANT2 :: pid(pa->pid->val))); + pids' := pids; + call participantPids := Set_Get(pids', (lambda i:int :: pid(i))); + call {:linear participantPids} create_asyncs((lambda pa:PARTICIPANT2 :: pid(pa->pid->val))); } //////////////////////////////////////////////////////////////////////////////// @@ -106,13 +116,21 @@ 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()); - call create_async(COORDINATOR2(One(0))); - call create_asyncs((lambda pa:PARTICIPANT2 :: pid(pa->pid->val))); + 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} @@ -120,6 +138,9 @@ 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); @@ -133,9 +154,13 @@ modifies RequestChannel, VoteChannel, votes; VoteChannel[YES()] >= 0 && VoteChannel[NO()] >= 0 && VoteChannel[YES()] + VoteChannel[NO()] <= k && (VoteChannel[YES()] == k ==> (forall i:int :: pidLe(i,k) ==> votes[i] == YES())); - call create_async(COORDINATOR2(One(0))); - call create_asyncs((lambda pa:PARTICIPANT2 :: pidLe(pa->pid->val, k))); - call create_asyncs((lambda {:pool "PARTICIPANT1"} pa:PARTICIPANT1 :: pidGt(pa->pid->val, k))); + 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))); } @@ -146,12 +171,19 @@ 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); - call create_async(COORDINATOR2(One(0))); - call create_asyncs((lambda pa:PARTICIPANT1 :: pid(pa->pid->val))); + 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))); } //////////////////////////////////////////////////////////////////////////////// @@ -160,9 +192,17 @@ 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); - call create_async(COORDINATOR1(One(0))); - call create_asyncs((lambda pa:PARTICIPANT1 :: pid(pa->pid->val))); + + 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) @@ -181,7 +221,7 @@ modifies RequestChannel, VoteChannel, votes; VoteChannel[v] := VoteChannel[v] + 1; } - call create_async(PARTICIPANT2(pid)); + async call PARTICIPANT2(pid); } async atomic action {:layer 2,5} PARTICIPANT2 ({:linear_in} pid: One int) @@ -203,7 +243,7 @@ modifies RequestChannel; { assert pid->val == 0; RequestChannel := (lambda i:int :: if pid(i) then RequestChannel[i] + 1 else RequestChannel[i]); - call create_async(COORDINATOR2(One(0))); + async call COORDINATOR2(pid); } async atomic action {:layer 2,4} COORDINATOR2 ({:linear_in} pid: One int) diff --git a/Test/civl/inductive-sequentialization/2PC.bpl.expect b/Test/civl/inductive-sequentialization/2PC.bpl.expect index 2ce761c65..309f0e6f6 100644 --- a/Test/civl/inductive-sequentialization/2PC.bpl.expect +++ b/Test/civl/inductive-sequentialization/2PC.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 61 verified, 0 errors +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 e2df7b23e..2d65d6b64 100644 --- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl +++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl @@ -82,22 +82,24 @@ action {:layer 3} INV_COLLECT_ELIM({:linear_in} ps: Set perm) creates COLLECT; modifies CH, decision; +requires ps->val == (lambda p:perm :: pid(p->i)); +requires CH == MultisetEmpty; { + var {:linear} ps': Set perm; + var {:linear} remainingCollects: Set perm; var {:pool "INV_COLLECT"} k: int; - assert ps->val == (lambda p:perm :: pid(p->i)); - assert CH == MultisetEmpty; - CH := (lambda v:val :: value_card(v, value, 1, n)); assume card(CH) == n; assume MultisetSubsetEq(MultisetEmpty, CH); - assume {:add_to_pool "INV_COLLECT", k, k+1} {:add_to_pool "Collect", COLLECT(One(Collect(n)), n)} 0 <= k && k <= n; decision := (lambda i:pid :: if 1 <= i && i <= k then max(CH) else decision[i]); - call create_asyncs(RemainingCollects(k)); + ps' := ps; + call remainingCollects := Set_Get(ps', (lambda p: perm :: p is Collect && k < p->i && p->i <= n)); + call {:linear remainingCollects} create_asyncs(RemainingCollects(k)); call set_choice(COLLECT(One(Collect(k+1)), k+1)); } @@ -108,41 +110,52 @@ MAIN'({:linear_in} ps: Set perm) refines MAIN'' using INV_COLLECT_ELIM; creates COLLECT; modifies CH; +requires ps->val == (lambda p:perm :: pid(p->i)); +requires CH == MultisetEmpty; { - assert ps->val == (lambda p:perm :: pid(p->i)); - assert CH == MultisetEmpty; + var {:linear} ps': Set perm; + var {:linear} allCollects: Set perm; assume {:add_to_pool "INV_COLLECT", 0} true; CH := (lambda v:val :: value_card(v, value, 1, n)); assume card(CH) == n; assume MultisetSubsetEq(MultisetEmpty, CH); - call create_asyncs(AllCollects()); + ps' := ps; + call allCollects := Set_Get(ps', (lambda p: perm :: p is Collect && pid(p->i))); + call {:linear allCollects} create_asyncs(AllCollects()); } atomic action {:layer 2} MAIN({:linear_in} ps: Set perm) refines MAIN' using INV_BROADCAST_ELIM; creates BROADCAST, COLLECT; +requires ps->val == (lambda p:perm :: pid(p->i)); +requires CH == MultisetEmpty; { - assert ps->val == (lambda p:perm :: pid(p->i)); + var {:linear} ps': Set perm; + var {:linear} allBroadcasts: Set perm; + var {:linear} allCollects: Set perm; assume {:add_to_pool "INV_BROADCAST", 0} true; - assert CH == MultisetEmpty; - - call create_asyncs(AllBroadcasts()); - call create_asyncs(AllCollects()); + ps' := ps; + call allBroadcasts := Set_Get(ps', (lambda p: perm :: p is Broadcast && pid(p->i))); + call {:linear allBroadcasts} create_asyncs(AllBroadcasts()); + call allCollects := Set_Get(ps', (lambda p: perm :: p is Collect && pid(p->i))); + call {:linear allCollects} create_asyncs(AllCollects()); } action {:layer 2} INV_BROADCAST_ELIM({:linear_in} ps: Set perm) creates BROADCAST, COLLECT; modifies CH; +requires ps->val == (lambda p:perm :: pid(p->i)); +requires CH == MultisetEmpty; { + var {:linear} ps': Set perm; + var {:linear} remainingBroadcasts: Set perm; + var {:linear} allCollects: Set perm; var {:pool "INV_BROADCAST"} k: int; - assert ps->val == (lambda p:perm :: pid(p->i)); - assert CH == MultisetEmpty; - assume {:add_to_pool "INV_BROADCAST", k, k+1} {:add_to_pool "Broadcast", BROADCAST(One(Broadcast(n)), n)} @@ -150,8 +163,11 @@ modifies CH; CH := (lambda v:val :: value_card(v, value, 1, k)); assume card(CH) == k; assume MultisetSubsetEq(MultisetEmpty, CH); - call create_asyncs(RemainingBroadcasts(k)); - call create_asyncs(AllCollects()); + ps' := ps; + call remainingBroadcasts := Set_Get(ps', (lambda p: perm :: p is Broadcast && k < p->i && p->i <= n)); + call {:linear remainingBroadcasts} create_asyncs(RemainingBroadcasts(k)); + call allCollects := Set_Get(ps', (lambda p: perm :: p is Collect && pid(p->i))); + call {:linear allCollects} create_asyncs(AllCollects()); call set_choice(BROADCAST(One(Broadcast(k+1)), k+1)); } diff --git a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl.expect b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl.expect index dc45a0eee..6696bdbd1 100644 --- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl.expect +++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 24 verified, 0 errors +Boogie program verifier finished with 26 verified, 0 errors diff --git a/Test/civl/inductive-sequentialization/ChangRoberts.bpl b/Test/civl/inductive-sequentialization/ChangRoberts.bpl index 47079a3d8..0e1a0580b 100644 --- a/Test/civl/inductive-sequentialization/ChangRoberts.bpl +++ b/Test/civl/inductive-sequentialization/ChangRoberts.bpl @@ -77,7 +77,7 @@ modifies leader; call create_asyncs( (lambda pa: P :: ValidPid(pa->pid) && Pos(pa->pid) < Pos(pid) && pa->self == Next(pa->pid))); // create singleton and set the choice - call create_async(choice); + async call P(self, pid); call set_choice(choice); } else { leader[ExpectedLeader] := true; @@ -125,7 +125,7 @@ async left action {:layer 2} PInit(self: int) creates P; { assert ValidPid(self); - call create_async(P(Next(self), self)); + async call P(Next(self), self); } async atomic action {:layer 2, 3} P(self: int, pid: int) @@ -139,7 +139,7 @@ modifies leader; } else if (Below(self, pid)) { - call create_async(P(Next(self), pid)); + async call P(Next(self), pid); } } diff --git a/Test/civl/inductive-sequentialization/NoChoice.bpl b/Test/civl/inductive-sequentialization/NoChoice.bpl index 00c3620ae..a74e1b6c6 100644 --- a/Test/civl/inductive-sequentialization/NoChoice.bpl +++ b/Test/civl/inductive-sequentialization/NoChoice.bpl @@ -9,8 +9,8 @@ atomic action {:layer 1} MAIN () refines MAIN'; creates INC, DEC; { - call create_async(INC()); - call create_async(DEC()); + async call INC(); + async call DEC(); } atomic action {:layer 2} MAIN' () diff --git a/Test/civl/inductive-sequentialization/PingPong.bpl b/Test/civl/inductive-sequentialization/PingPong.bpl index 32b2c27c1..e16d0c03e 100644 --- a/Test/civl/inductive-sequentialization/PingPong.bpl +++ b/Test/civl/inductive-sequentialization/PingPong.bpl @@ -44,26 +44,32 @@ INV (cid: ChannelId, {:linear_in} handles: Set ChannelHandle) creates PING, PONG; modifies channel; { + var {:linear} handles': Set ChannelHandle; + var {:linear} left: One ChannelHandle; + var {:linear} right: One ChannelHandle; var {:pool "INV"} c: int; assert handles == BothHandles(cid); assert channel[cid] == ChannelPair(EmptyChannel(), EmptyChannel()); assume {:add_to_pool "INV", 0, c, c+1} 0 < c; + handles' := handles; + call left := One_Get(handles', Left(cid)); + call right := One_Get(handles', Right(cid)); if (*) { channel[cid] := ChannelPair(EmptyChannel(), EmptyChannel()[c := 1]); - call create_async(PONG(c, One(Right(cid)))); - call create_async(PING(c, One(Left(cid)))); - call set_choice(PONG(c, One(Right(cid)))); + async call PONG(c, right); + async call PING(c, left); + call set_choice(PONG(c, right)); } else if (*) { channel[cid] := ChannelPair(EmptyChannel(), EmptyChannel()[0 := 1]); - call create_async(PONG(c, One(Right(cid)))); - call set_choice(PONG(c, One(Right(cid)))); + async call PONG(c, right); + call set_choice(PONG(c, right)); } else if (*) { channel[cid] := ChannelPair(EmptyChannel()[c := 1], EmptyChannel()); - call create_async(PONG(c+1, One(Right(cid)))); - call create_async(PING(c, One(Left(cid)))); - call set_choice(PING(c, One(Left(cid)))); + async call PONG(c+1, right); + async call PING(c, left); + call set_choice(PING(c, left)); } else { channel[cid] := ChannelPair(EmptyChannel(), EmptyChannel()); } @@ -77,11 +83,18 @@ refines MAIN' using INV; creates PING, PONG; modifies channel; { + var {:linear} handles': Set ChannelHandle; + var {:linear} left: One ChannelHandle; + var {:linear} right: One ChannelHandle; + assert handles == BothHandles(cid); assert channel[cid] == ChannelPair(EmptyChannel(), EmptyChannel()); channel[cid] := ChannelPair(EmptyChannel(), EmptyChannel()[1 := 1]); - call create_async(PING(1, One(Left(cid)))); - call create_async(PONG(1, One(Right(cid)))); + handles' := handles; + call left := One_Get(handles', Left(cid)); + call right := One_Get(handles', Right(cid)); + async call PING(1, left); + async call PONG(1, right); } async atomic action {:layer 2} PING (x: int, {:linear_in} p: One ChannelHandle) @@ -106,7 +119,7 @@ requires call YieldPing(x, p); if (*) { right_channel[x+1] := right_channel[x+1] + 1; - call create_async(PING(x+1, p)); + async call PING(x+1, p); } else { @@ -136,7 +149,7 @@ requires call YieldPong(y, p); assume right_channel[y] > 0; right_channel[y] := right_channel[y] - 1; left_channel[y] := left_channel[y] + 1; - call create_async(PONG(y+1, p)); + async call PONG(y+1, p); } else { diff --git a/Test/civl/inductive-sequentialization/PingPong.bpl.expect b/Test/civl/inductive-sequentialization/PingPong.bpl.expect index bf98dae4d..fdd1a2438 100644 --- a/Test/civl/inductive-sequentialization/PingPong.bpl.expect +++ b/Test/civl/inductive-sequentialization/PingPong.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 36 verified, 0 errors +Boogie program verifier finished with 33 verified, 0 errors diff --git a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl index bc7b900a3..091ed1932 100644 --- a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl +++ b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl @@ -23,10 +23,17 @@ atomic action {:layer 2} MAIN (cid: ChannelId, {:linear_in} handles: Set Channel refines MAIN' using INV; creates PRODUCER, CONSUMER; { + var {:linear} handles': Set ChannelHandle; + var {:linear} send: One ChannelHandle; + var {:linear} receive: One ChannelHandle; + assert handles == BothHandles(cid); assert channels[cid]->head == channels[cid]->tail; - call create_async(PRODUCER(1, One(Send(cid)))); - call create_async(CONSUMER(1, One(Receive(cid)))); + handles' := handles; + call send := One_Get(handles', Send(cid)); + call receive := One_Get(handles', Receive(cid)); + async call PRODUCER(1, send); + async call CONSUMER(1, receive); } atomic action {:layer 3} MAIN' (cid: ChannelId, {:linear_in} handles: Set ChannelHandle) @@ -45,6 +52,9 @@ INV (cid: ChannelId, {:linear_in} handles: Set ChannelHandle) creates PRODUCER, CONSUMER; modifies channels; { + var {:linear} handles': Set ChannelHandle; + var {:linear} send: One ChannelHandle; + var {:linear} receive: One ChannelHandle; var {:pool "INV1"} c: int; var {:pool "INV2"} channel: Channel; var C: [int]int; @@ -57,20 +67,23 @@ modifies channels; head := channel->head; tail := channel->tail; assume {:add_to_pool "INV1", c, c+1} 0 < c; + handles' := handles; + call send := One_Get(handles', Send(cid)); + call receive := One_Get(handles', Receive(cid)); if (*) { assume head == tail; - call create_async(PRODUCER(c, One(Send(cid)))); - call create_async(CONSUMER(c, One(Receive(cid)))); - call set_choice(PRODUCER(c, One(Send(cid)))); + async call PRODUCER(c, send); + async call CONSUMER(c, receive); + call set_choice(PRODUCER(c, send)); } else if (*) { assume tail == head + 1 && C[head] == 0; - call create_async(CONSUMER(c, One(Receive(cid)))); - call set_choice(CONSUMER(c, One(Receive(cid)))); + async call CONSUMER(c, receive); + call set_choice(CONSUMER(c, receive)); } else if (*) { assume tail == head + 1 && C[head] == c; - call create_async(PRODUCER(c+1, One(Send(cid)))); - call create_async(CONSUMER(c, One(Receive(cid)))); - call set_choice(CONSUMER(c, One(Receive(cid)))); + async call PRODUCER(c+1, send); + async call CONSUMER(c, receive); + call set_choice(CONSUMER(c, receive)); } else { assume head == tail; } @@ -96,7 +109,7 @@ modifies channels; { C[tail] := x; tail := tail + 1; - call create_async(PRODUCER(x+1, send_handle)); + async call PRODUCER(x+1, send_handle); } else { @@ -129,7 +142,7 @@ requires call YieldConsumer(receive_handle); head := head + 1; if (x' != 0) { - call create_async(CONSUMER(x'+1, receive_handle)); + async call CONSUMER(x'+1, receive_handle); } channels[receive_handle->val->cid] := Channel(C, head, tail); assume {:add_to_pool "INV2", channels[receive_handle->val->cid]} true; diff --git a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl.expect b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl.expect index dc45a0eee..4bcb10714 100644 --- a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl.expect +++ b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 24 verified, 0 errors +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl b/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl deleted file mode 100644 index 76012c3f6..000000000 --- a/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl +++ /dev/null @@ -1,74 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type Value; - -type Tid; - -datatype StampedValue { - StampedValue(ts: int, value: Value) -} - -const n: int; -axiom n >= 1; - -var {:layer 0,2} mem: [int]StampedValue; -var {:layer 0,2} r1: [Tid][int]StampedValue; - -// M = main_f , \elim = read_f, I = Inv, M' = main_f' -action {:layer 1} main_f({:linear_in} tid: One Tid) -refines {:IS_right} main_f' using Inv; -creates read_f; -{ - assume {:add_to_pool "A", 0} true; - call create_async(read_f(tid, 1)); -} - -action {:layer 2} main_f'({:linear_in} tid: One Tid) -modifies r1; -{ - havoc r1; - assume (forall i:int :: ((1 <= i && i <= n) ==> (mem[i]->ts > r1[tid->val][i]->ts || r1[tid->val][i] == mem[i]))); -} - -async atomic action {:layer 1} read_f({:linear_in} tid: One Tid, i: int) -creates read_f; -modifies r1; -{ - var {:pool "K"} k:int; - var {:pool "V"} v:Value; - if (*) { - assume {:add_to_pool "K", mem[i]->ts, k} {:add_to_pool "V", mem[i]->value, v} true; - assume k < mem[i]->ts; - r1[tid->val][i] := StampedValue(k, v); - } else { - r1[tid->val][i] := mem[i]; - } - - if (i != n) { - call create_async(read_f(tid, i+1)); - } -} - -atomic action {: layer 1,2} write(i: int,v: Value) -modifies mem; -{ - var x: StampedValue; - x := mem[i]; - mem[i] := StampedValue(x->ts + 1, v); -} - -action {:layer 1} Inv({:linear_in} tid: One Tid) -modifies r1; -creates read_f; -{ - - var {:pool "A"} j: int; - assume {:add_to_pool "A", j+1} 0 <= j && j <= n; - havoc r1; - assume (forall i:int :: ((1 <= i && i <= j) ==> (mem[i]->ts > r1[tid->val][i]->ts || r1[tid->val][i] == mem[i]))); - if (j < n) { - call create_async(read_f(tid, j+1)); - call set_choice(read_f(tid, j+1)); - } -} \ No newline at end of file diff --git a/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl.expect b/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl.expect deleted file mode 100644 index 1aff37bfb..000000000 --- a/Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 15 verified, 0 errors \ No newline at end of file diff --git a/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl b/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl deleted file mode 100644 index b07d0ec5d..000000000 --- a/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl +++ /dev/null @@ -1,201 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type Value; - -type Tid; - -datatype StampedValue { - StampedValue(ts: int, value: Value) -} - -datatype Permission { - Permission(tid: Tid, mem_index: int) -} - -const n: int; -axiom n >= 1; - -var {:layer 0,2} mem: [int]StampedValue; -var {:linear} {:layer 0,2} pSet: Set Permission; -var {:layer 0,2} channels: [Tid](Option [int]StampedValue); -var {:layer 0,1} snapshots: [Tid][int]StampedValue; - -function {:inline} WholeTidPermission(tid: Tid): Set Permission { - Set((lambda {:pool "D"} x: Permission :: x->tid == tid && 1 <= x->mem_index && x->mem_index <= n)) -} - -async action {:layer 1} main_f(tid: Tid, {:linear_in} sps: Set Permission) -refines {:IS_right} main_f' using Inv_f; -modifies pSet; -creates read_f; -{ - assume {:add_to_pool "A", 0, n} true; - assert sps == WholeTidPermission(tid); - assert channels[tid] == None(); - call create_asyncs((lambda pa:read_f :: 1 <= pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid)); -} - -async action {:layer 2} main_f'(tid: Tid, {:linear_in} sps: Set Permission) -modifies pSet, channels; -{ - var snapshot: [int]StampedValue; - assume {:add_to_pool "A", 0, n} true; - assert sps == WholeTidPermission(tid); - assert channels[tid] == None(); - assume (forall i:int :: 1 <= i && i <= n ==> (snapshot[i]->ts < mem[i]->ts || snapshot[i]== mem[i])); - call Set_Put(pSet, sps); - call ChannelSend(tid, snapshot); -} - -async action {:layer 1} {:exit_condition Set_IsSubset(WholeTidPermission(perm->val->tid), Set_Add(pSet, perm->val))} read_f({:linear_in} perm: One Permission) -modifies snapshots, pSet, channels; -{ - var {:pool "K"} k:int; - var {:pool "V"} v:Value; - assert 1 <= perm->val->mem_index && perm->val->mem_index <=n; - assert channels[perm->val->tid] == None(); - assume {:add_to_pool "A", 0, n} true; - - if (*) { - assume {:add_to_pool "K", mem[perm->val->mem_index]->ts, k} {:add_to_pool "V", mem[perm->val->mem_index]->value, v} true; - assume k < mem[perm->val->mem_index]->ts; - snapshots[perm->val->tid][perm->val->mem_index]:= StampedValue(k, v); - } else { - snapshots[perm->val->tid][perm->val->mem_index]:= mem[perm->val->mem_index]; - } - call One_Put(pSet, perm); - - if (Set_IsSubset(WholeTidPermission(perm->val->tid), pSet)) { - call ChannelSend(perm->val->tid, snapshots[perm->val->tid]); - } -} - -atomic action {:layer 1,2} write(i: int,v: Value) -modifies mem; -{ - var x: StampedValue; - x := mem[i]; - mem[i] := StampedValue(x->ts + 1, v); -} - -action {:layer 1} Inv_f(tid: Tid, {:linear_in} sps: Set Permission) -modifies snapshots, pSet, channels; -creates read_f; -{ - var {:pool "A"} j: int; - var {:linear} sps': Set Permission; - var {:linear} done_set: Set Permission; - var choice: read_f; - assert sps == WholeTidPermission(tid); - assert channels[tid] == None(); - assume {:add_to_pool "A", 0, j+1, n} 0 <= j && j <= n; - havoc snapshots; - assume (forall i:int :: 1 <= i && i <= j ==> (snapshots[tid][i]->ts < mem[i]->ts || snapshots[tid][i]== mem[i])); - - assume {:add_to_pool "D", Permission(tid, n)} true; - sps' := sps; - call done_set := Set_Get(sps', (lambda {:pool "D" } x: Permission :: x->tid == tid && 1 <= x->mem_index && x->mem_index <= j)); - - call Set_Put(pSet, done_set); - if (j < n) { - choice := read_f(One(Permission(tid, j+1))); - assume {:add_to_pool "C", choice} true; - call create_asyncs((lambda {:pool "C" } pa:read_f :: j+1 <= pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid)); - call set_choice(choice); - } else { - call ChannelSend(tid, snapshots[tid]); - } -} - -action {:layer 1,2} ChannelSend(tid: Tid, snapshot: [int]StampedValue) -modifies channels; -{ - assert Set_IsSubset(WholeTidPermission(tid), pSet); - assert channels[tid] == None(); - channels[tid] := Some(snapshot); -} - -right action {:layer 1,2} ChannelReceive(tid: Tid) returns (snapshot: [int]StampedValue) -modifies channels; -{ - assume channels[tid] != None(); - snapshot := channels[tid]->t; - channels[tid] := None(); -} - -async action {:layer 1} main_s(tid: Tid, {:linear_in} sps: Set Permission) -refines {:IS_left} main_s' using Inv_s; -modifies pSet; -creates read_s; -{ - assume {:add_to_pool "A", 0, n} true; - assert sps == WholeTidPermission(tid); - assert channels[tid] == None(); - call create_asyncs((lambda pa:read_s :: 1 <= pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid)); -} - -async action {:layer 2} main_s'(tid: Tid, {:linear_in} sps: Set Permission) -modifies pSet, channels; -{ - var snapshot: [int]StampedValue; - assume {:add_to_pool "A", 0, n} true; - assert sps == WholeTidPermission(tid); - assert channels[tid] == None(); - assume (forall i:int :: 1 <= i && i <= n ==> (snapshot[i]->ts > mem[i]->ts || snapshot[i]== mem[i])); - call Set_Put(pSet, sps); - call ChannelSend(tid, snapshot); -} - -async left action {:layer 1} read_s({:linear_in} perm: One Permission) -modifies snapshots, pSet, channels; -{ - var {:pool "K"} k:int; - var {:pool "V"} v:Value; - assert 1 <= perm->val->mem_index && perm->val->mem_index <=n; - assert channels[perm->val->tid] == None(); - assume {:add_to_pool "A", 0, n} true; - - if (*) { - assume {:add_to_pool "K", mem[perm->val->mem_index]->ts, k} {:add_to_pool "V", mem[perm->val->mem_index]->value, v} true; - assume k > mem[perm->val->mem_index]->ts; - snapshots[perm->val->tid][perm->val->mem_index]:= StampedValue(k, v); - } else { - snapshots[perm->val->tid][perm->val->mem_index]:= mem[perm->val->mem_index]; - } - call One_Put(pSet, perm); - - if (Set_IsSubset(WholeTidPermission(perm->val->tid), pSet)) { - call ChannelSend(perm->val->tid, snapshots[perm->val->tid]); - } -} - -action {:layer 1} Inv_s(tid: Tid, {:linear_in} sps: Set Permission) -modifies snapshots, pSet, channels; -creates read_s; -{ - var {:pool "A"} j: int; - var {:linear} sps': Set Permission; - var {:linear} done_set: Set Permission; - var choice: read_s; - assert sps == WholeTidPermission(tid); - assert channels[tid] == None(); - assume {:add_to_pool "A", 0, j+1, n} 0 <= j && j <= n; - havoc snapshots; - assume (forall i:int :: 1 <= i && i <= j ==> (snapshots[tid][i]->ts > mem[i]->ts || snapshots[tid][i]== mem[i])); - - assume {:add_to_pool "D", Permission(tid, n)} true; - sps' := sps; - call done_set := Set_Get(sps', (lambda {:pool "D" } x: Permission :: x->tid == tid && 1 <= x->mem_index && x->mem_index <= j)); - - call Set_Put(pSet, done_set); - if (j < n) { - choice := read_s(One(Permission(tid, j+1))); - assume {:add_to_pool "C", choice} true; - call create_asyncs((lambda {:pool "C" } pa:read_s :: j+1 <= pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid)); - call set_choice(choice); - } else { - call ChannelSend(tid, snapshots[tid]); - } -} - diff --git a/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl.expect b/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl.expect deleted file mode 100644 index 753f9e1e3..000000000 --- a/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 57 verified, 0 errors \ No newline at end of file diff --git a/Test/civl/paxos/Paxos.bpl b/Test/civl/paxos/Paxos.bpl index 2fb600021..cac2ae040 100644 --- a/Test/civl/paxos/Paxos.bpl +++ b/Test/civl/paxos/Paxos.bpl @@ -72,6 +72,11 @@ function {:inline} JoinPermissions(r: Round) : Set Permission Set((lambda {:pool "Permission"} p:Permission :: {:add_to_pool "Permission", p} p is JoinPerm && p->r == r)) } +function {:inline} VotePermissions(r: Round) : Set Permission +{ + Set((lambda {:pool "Permission"} p:Permission :: {:add_to_pool "Permission", p} p is VotePerm && p->r == r)) +} + function {:inline} ProposePermissions(r: Round) : Set Permission { Set((lambda {:pool "Permission"} p:Permission :: {:add_to_pool "Permission", p} !(p is JoinPerm) && p->r == r)) diff --git a/Test/civl/paxos/PaxosActions.bpl b/Test/civl/paxos/PaxosActions.bpl index 007bfea35..0a6e74114 100644 --- a/Test/civl/paxos/PaxosActions.bpl +++ b/Test/civl/paxos/PaxosActions.bpl @@ -1,8 +1,10 @@ async atomic action {:layer 2} A_StartRound(r: Round, {:linear_in} r_lin: Set Permission) creates A_Join, A_Propose; +requires AllPermissions(r) == r_lin; +requires Round(r); { - assert AllPermissions(r) == r_lin; - assert Round(r); + var {:linear} r_lin': Set Permission; + var {:linear} joinPermissions: Set Permission; assume {:add_to_pool "Round", r-1} @@ -10,22 +12,25 @@ creates A_Join, A_Propose; {:add_to_pool "Permission", ConcludePerm(r)} true; - call create_asyncs(JoinPAs(r)); - call create_async(A_Propose(r, ProposePermissions(r))); + r_lin' := r_lin; + call joinPermissions := Set_Get(r_lin', JoinPermissions(r)->val); + call {:linear joinPermissions} create_asyncs(JoinPAs(r)); + async call A_Propose(r, r_lin'); } async atomic action {:layer 2} A_Propose(r: Round, {:linear_in} ps: Set Permission) creates A_Vote, A_Conclude; modifies voteInfo; +requires Round(r); +requires ps == ProposePermissions(r); +requires voteInfo[r] is None; { + var {:linear} ps': Set Permission; + var {:linear} concludePermission: One Permission; var {:pool "Round"} maxRound: int; var {:pool "MaxValue"} maxValue: Value; var {:pool "NodeSet"} ns: NodeSet; - assert Round(r); - assert ps == ProposePermissions(r); - assert voteInfo[r] is None; - assume {:add_to_pool "Round", r, r-1} {:add_to_pool "Node", 0} @@ -42,8 +47,10 @@ modifies voteInfo; maxValue := voteInfo[maxRound]->t->value; } voteInfo[r] := Some(VoteInfo(maxValue, NoNodes())); - call create_asyncs(VotePAs(r, maxValue)); - call create_async(A_Conclude(r, maxValue, One(ConcludePerm(r)))); + ps' := ps; + call concludePermission := One_Get(ps', ConcludePerm(r)); + async call A_Conclude(r, maxValue, concludePermission); + call {:linear ps'} create_asyncs(VotePAs(r, maxValue)); } } diff --git a/Test/civl/paxos/PaxosSeq.bpl b/Test/civl/paxos/PaxosSeq.bpl index bb7482199..acdb92518 100644 --- a/Test/civl/paxos/PaxosSeq.bpl +++ b/Test/civl/paxos/PaxosSeq.bpl @@ -11,7 +11,7 @@ creates A_StartRound; 0 <= numRounds; joinedNodes := (lambda r: Round:: NoNodes()); voteInfo := (lambda r: Round:: None()); - call create_asyncs((lambda pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && Round(pa->r) && pa->r <= numRounds)); + call {:linear ps} create_asyncs((lambda pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && Round(pa->r) && pa->r <= numRounds)); } atomic action {:layer 3} A_Paxos'({:linear_in} ps: Set Permission) @@ -26,13 +26,18 @@ action {:layer 2} INV({:linear_in} ps: Set Permission) creates A_StartRound, A_Propose, A_Conclude, A_Join, A_Vote; modifies joinedNodes, voteInfo, decision; +requires Init(ps, decision); { + var {:linear} ps': Set Permission; + var {:linear} proposePermissions: Set Permission; + var {:linear} joinPermissions: Set Permission; + var {:linear} votePermissions: Set Permission; + var {:linear} concludePermission: One Permission; var {:pool "NumRounds"} numRounds: int; var {:pool "Round"} k: int; var {:pool "Node"} m: Node; - assert Init(ps, decision); - + ps' := ps; havoc joinedNodes, voteInfo, decision; // This invariant is the "pending async skeleton" which states the possible @@ -53,7 +58,7 @@ modifies joinedNodes, voteInfo, decision; assume (forall r: Round :: r < 1 || r > k ==> voteInfo[r] is None) && (forall r: Round :: r < 1 || r > k ==> decision[r] is None); - call create_asyncs((lambda {:pool "A_StartRound"} pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && k < pa->r && pa->r <= numRounds)); + call {:linear ps'} create_asyncs((lambda {:pool "A_StartRound"} pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && k < pa->r && pa->r <= numRounds)); call set_choice(A_StartRound(k+1, AllPermissions(k+1))); } else if (*) { assume @@ -63,11 +68,16 @@ modifies joinedNodes, voteInfo, decision; {:add_to_pool "Node", m} {:add_to_pool "A_Join", A_Join(k+1, numNodes, One(JoinPerm(k+1, numNodes)))} 0 <= m && m <= numNodes; - call create_asyncs((lambda pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && k+1 < pa->r && pa->r <= numRounds)); - call create_async(A_Propose(k+1, ProposePermissions(k+1))); - call create_asyncs((lambda {:pool "A_Join"} pa: A_Join :: pa->r == k+1 && m < pa->n && pa->n <= numNodes && pa->p->val == JoinPerm(k+1, pa->n))); - if (m == numNodes) { call set_choice(A_Propose(k+1, ProposePermissions(k+1))); } - else { call set_choice(A_Join(k+1, m+1, One(JoinPerm(k+1, m+1)))); } + call proposePermissions := Set_Get(ps', ProposePermissions(k+1)->val); + async call A_Propose(k+1, proposePermissions); + call joinPermissions := Set_Get(ps', JoinPermissions(k+1)->val); + call {:linear joinPermissions} create_asyncs((lambda {:pool "A_Join"} pa: A_Join :: pa->r == k+1 && m < pa->n && pa->n <= numNodes && pa->p->val == JoinPerm(k+1, pa->n))); + call {:linear ps'} create_asyncs((lambda pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && k+1 < pa->r && pa->r <= numRounds)); + if (m == numNodes) { + call set_choice(A_Propose(k+1, ProposePermissions(k+1))); + } else { + call set_choice(A_Join(k+1, m+1, One(JoinPerm(k+1, m+1)))); + } } else { assume voteInfo[k+1] is Some && @@ -79,11 +89,16 @@ modifies joinedNodes, voteInfo, decision; {:add_to_pool "A_StartRound", A_StartRound(numRounds, AllPermissions(numRounds))} 0 <= m && m <= numNodes && (forall n: Node :: n < 1 || n > m ==> !voteInfo[k+1]->t->ns[n]); - call create_asyncs((lambda {:pool "A_StartRound"} pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && k+1 < pa->r && pa->r <= numRounds)); - call create_async(A_Conclude(k+1, voteInfo[k+1]->t->value, One(ConcludePerm(k+1)))); - call create_asyncs((lambda {:pool "A_Vote"} pa: A_Vote :: pa->r == k+1 && m < pa->n && pa->n <= numNodes && pa->v == voteInfo[k+1]->t->value && pa->p->val == VotePerm(k+1, pa->n))); - if (m == numNodes) { call set_choice(A_Conclude(k+1, voteInfo[k+1]->t->value, One(ConcludePerm(k+1)))); } - else { call set_choice(A_Vote(k+1, m+1, voteInfo[k+1]->t->value, One(VotePerm(k+1, m+1)))); } + call concludePermission := One_Get(ps', ConcludePerm(k+1)); + async call A_Conclude(k+1, voteInfo[k+1]->t->value, concludePermission); + call votePermissions := Set_Get(ps', VotePermissions(k+1)->val); + call {:linear votePermissions} create_asyncs((lambda {:pool "A_Vote"} pa: A_Vote :: pa->r == k+1 && m < pa->n && pa->n <= numNodes && pa->v == voteInfo[k+1]->t->value && pa->p->val == VotePerm(k+1, pa->n))); + call {:linear ps'} create_asyncs((lambda {:pool "A_StartRound"} pa: A_StartRound :: AllPermissions(pa->r) == pa->r_lin && k+1 < pa->r && pa->r <= numRounds)); + if (m == numNodes) { + call set_choice(A_Conclude(k+1, voteInfo[k+1]->t->value, One(ConcludePerm(k+1)))); + } else { + call set_choice(A_Vote(k+1, m+1, voteInfo[k+1]->t->value, One(VotePerm(k+1, m+1)))); + } } // If there was a decision for some value, then there must have been a diff --git a/Test/civl/regression-tests/hide-params-pa-2.bpl b/Test/civl/regression-tests/hide-params-pa-2.bpl index 8dc572003..31e369cbc 100644 --- a/Test/civl/regression-tests/hide-params-pa-2.bpl +++ b/Test/civl/regression-tests/hide-params-pa-2.bpl @@ -4,7 +4,7 @@ atomic action {:layer 1,2} SPEC () creates A; { - call create_async(A(1)); + async call A(1); } yield procedure {:layer 1} b () diff --git a/Test/civl/regression-tests/is2-attributes.bpl b/Test/civl/regression-tests/is2-attributes.bpl index 9c6dfebdf..0bab41652 100644 --- a/Test/civl/regression-tests/is2-attributes.bpl +++ b/Test/civl/regression-tests/is2-attributes.bpl @@ -9,10 +9,10 @@ async left action {:layer 1} main_f''() refines {:IS_right} final using Inv; creates main_f''; { - if(*){ + if (*) { } - else{ - call create_async(main_f''()); + else { + async call main_f''(); } } @@ -24,10 +24,10 @@ left action {:layer 2} final() action {:layer 1} Inv() creates main_f''; { - if(*){ + if (*) { } - else{ - call create_async(main_f''()); + else { + async call main_f''(); call set_choice(main_f''()); } } \ No newline at end of file diff --git a/Test/civl/regression-tests/only-async-call-ISR.bpl b/Test/civl/regression-tests/only-async-call-ISR.bpl index 858d34b7a..312e1fa56 100644 --- a/Test/civl/regression-tests/only-async-call-ISR.bpl +++ b/Test/civl/regression-tests/only-async-call-ISR.bpl @@ -17,7 +17,7 @@ creates main_f; if (*) { } else { - call create_async(main_f()); + async call main_f(); } } @@ -30,7 +30,7 @@ creates main_f; if (*) { } else { - call create_async(main_f()); + async call main_f(); call set_choice(main_f()); } } \ No newline at end of file diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl b/Test/civl/regression-tests/pa-noninterference-check.bpl index 3f6fca844..f6f8f1df7 100644 --- a/Test/civl/regression-tests/pa-noninterference-check.bpl +++ b/Test/civl/regression-tests/pa-noninterference-check.bpl @@ -4,7 +4,7 @@ atomic action {:layer 3} A_Foo() creates A_Incr; { - call create_async(A_Incr()); + async call A_Incr(); } yield procedure {:layer 2} Foo() diff --git a/Test/civl/regression-tests/pending-async-1.bpl b/Test/civl/regression-tests/pending-async-1.bpl index 0ab838d32..cb5d23783 100644 --- a/Test/civl/regression-tests/pending-async-1.bpl +++ b/Test/civl/regression-tests/pending-async-1.bpl @@ -8,14 +8,14 @@ async atomic action {:layer 1,2} A () {} left action {:layer 1} B () creates A; { - call create_async(A()); + async call A(); } left action {:layer 1} C (flag:bool) creates A; { if (flag) { - call create_async(A()); + async call A(); } } @@ -55,7 +55,7 @@ refines TEST2; atomic action {:layer 2} TEST2 () creates A; { - call create_async(A()); + async call A(); } //////////////////////////////////////////////////////////////////////////////// diff --git a/Test/civl/regression-tests/pending-async-1.bpl.expect b/Test/civl/regression-tests/pending-async-1.bpl.expect index ec6e90fd4..86c6fbf94 100644 --- a/Test/civl/regression-tests/pending-async-1.bpl.expect +++ b/Test/civl/regression-tests/pending-async-1.bpl.expect @@ -1,16 +1,16 @@ pending-async-1.bpl(48,28): Error: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: pending-async-1.bpl(51,3): anon0 - pending-async-1.bpl(11,3): inline$B$0$anon0 + pending-async-1.bpl(11,9): inline$B$0$anon0 pending-async-1.bpl(51,3): anon0$1 - pending-async-1.bpl(11,3): inline$B$1$anon0 + pending-async-1.bpl(11,9): inline$B$1$anon0 pending-async-1.bpl(51,3): anon0$2 (0,0): Civl_ReturnChecker pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized Execution trace: pending-async-1.bpl(67,3): anon0 pending-async-1.bpl(17,3): inline$C$0$anon0 - pending-async-1.bpl(18,5): inline$C$0$anon2_Then + pending-async-1.bpl(18,11): inline$C$0$anon2_Then pending-async-1.bpl(67,3): anon0$1 Boogie program verifier finished with 5 verified, 2 errors diff --git a/Test/civl/regression-tests/pending-async-2.bpl b/Test/civl/regression-tests/pending-async-2.bpl index 5407f2bec..d59c814c9 100644 --- a/Test/civl/regression-tests/pending-async-2.bpl +++ b/Test/civl/regression-tests/pending-async-2.bpl @@ -12,9 +12,9 @@ async atomic action {:layer 1} B () {} left action {:layer 1} C () creates A; { - call create_async(A()); + async call A(); // create undeclared pending async to B - call create_async(B()); + async call B(); } left action {:layer 1} D () diff --git a/Test/civl/regression-tests/pending-async-2.bpl.expect b/Test/civl/regression-tests/pending-async-2.bpl.expect index fbdac7ec6..e5c2e070d 100644 --- a/Test/civl/regression-tests/pending-async-2.bpl.expect +++ b/Test/civl/regression-tests/pending-async-2.bpl.expect @@ -1,2 +1,2 @@ -pending-async-2.bpl(17,2): Error: primitive call must be instantiated with a pending async type in the creates clause of caller +pending-async-2.bpl(17,8): Error: pending async must be in the creates clause of caller 1 type checking errors detected in pending-async-2.bpl diff --git a/Test/civl/regression-tests/pending-async-linearity.bpl b/Test/civl/regression-tests/pending-async-linearity.bpl deleted file mode 100644 index a8c7b6839..000000000 --- a/Test/civl/regression-tests/pending-async-linearity.bpl +++ /dev/null @@ -1,70 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -async atomic action {:layer 1} A ({:linear_in} pid: One int) -{} - -async atomic action {:layer 1} B ({:linear_in} pid: One int) -{} - -atomic action {:layer 1} M0 (pid:int) -creates A; -{ - call create_async(A(/* out of thin air */ One(pid))); -} - -atomic action {:layer 1} M1 ({:linear_in} pid: One int) -creates A; -{ - call create_async(A(pid)); -} - -atomic action {:layer 1} M2 ({:linear} pid: One int) -creates A; -{ - call create_async(A(/* duplication */ pid)); -} - -atomic action {:layer 1} M3 ({:linear_in} pid1: One int, {:linear_in} pid2: One int) -creates A, B; -{ - call create_async(A(pid1)); - call create_async(B(pid2)); -} - -atomic action {:layer 1} M4 ({:linear_in} pid1: One int, {:linear_in} pid2: One int) -creates A, B; -{ - call create_async(A(pid1)); - call create_async(B(/* duplication */ pid1)); -} - -atomic action {:layer 1} M5 ({:linear_in} pid: One int) returns ({:linear} pid_out: One int) -creates A; -{ - pid_out := pid; - call create_async(A(/* duplication */ pid)); -} - -atomic action {:layer 1} M6 ({:linear_in} pid1: One int, {:linear_in} pid2: One int, {:linear_in} pid3: One int) -returns ({:linear} pid_out: One int) -creates A, B; -{ - pid_out := pid3; - call create_async(A(pid1)); - call create_async(B(pid2)); -} - -atomic action {:layer 1} M7 ({:linear_in} pids: Set int) -creates A; -{ - assert pids->val == (lambda i:int :: 1 <= i && i <= 10); - call create_async(A(One(5))); -} - -atomic action {:layer 1} M8 ({:linear_in} pids: Set int) -creates A; -{ - assert pids->val == (lambda i:int :: 1 <= i && i <= 10); - call create_async(A(/* out of thin air */ One(0))); -} diff --git a/Test/civl/regression-tests/pending-async-linearity.bpl.expect b/Test/civl/regression-tests/pending-async-linearity.bpl.expect deleted file mode 100644 index ef39b8020..000000000 --- a/Test/civl/regression-tests/pending-async-linearity.bpl.expect +++ /dev/null @@ -1,27 +0,0 @@ -pending-async-linearity.bpl(10,26): Error: Out-of-thin-air permissions of type int in pending async of A -Execution trace: - pending-async-linearity.bpl(10,26): inline$M0$0$Entry - pending-async-linearity.bpl(13,3): inline$M0$0$anon0 - (0,0): int_out_of_thin_air_A -pending-async-linearity.bpl(22,26): Error: Duplication of permissions of type int in calling context (globals, linear outputs, or linear/linear_out inputs) and pending async of A -Execution trace: - pending-async-linearity.bpl(22,26): inline$M2$0$Entry - pending-async-linearity.bpl(25,3): inline$M2$0$anon0 - (0,0): int_duplication_A -pending-async-linearity.bpl(35,26): Error: Duplication of permissions of type int in pending asyncs of A and B -Execution trace: - pending-async-linearity.bpl(35,26): inline$M4$0$Entry - pending-async-linearity.bpl(38,3): inline$M4$0$anon0 - (0,0): int_duplication_A_B -pending-async-linearity.bpl(42,26): Error: Duplication of permissions of type int in calling context (globals, linear outputs, or linear/linear_out inputs) and pending async of A -Execution trace: - pending-async-linearity.bpl(42,26): inline$M5$0$Entry - pending-async-linearity.bpl(45,11): inline$M5$0$anon0 - (0,0): int_duplication_A -pending-async-linearity.bpl(65,26): Error: Out-of-thin-air permissions of type int in pending async of A -Execution trace: - pending-async-linearity.bpl(65,26): inline$M8$0$Entry - pending-async-linearity.bpl(68,3): inline$M8$0$anon0 - (0,0): int_out_of_thin_air_A - -Boogie program verifier finished with 4 verified, 5 errors diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl index 1ce957dea..d8b0f84db 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl +++ b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl @@ -15,7 +15,7 @@ modifies x; left action {:layer 1} ASYNC_A () creates A; { - call create_async(A()); + async call A(); } yield procedure {:layer 1} dummy () {} diff --git a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl b/Test/civl/regression-tests/pending-async-noninterference-linear.bpl index 9d5d9f88a..247b49eb0 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl +++ b/Test/civl/regression-tests/pending-async-noninterference-linear.bpl @@ -15,7 +15,7 @@ modifies x; left action {:layer 1} ASYNC_A ({:linear_in} tid: One int) creates A; { - call create_async(A(tid)); + async call A(tid); } yield procedure {:layer 1} dummy () {} diff --git a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-linear.bpl.expect index a9949f2e7..41374b000 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl.expect +++ b/Test/civl/regression-tests/pending-async-noninterference-linear.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/regression-tests/pending-async-noninterference-ok.bpl b/Test/civl/regression-tests/pending-async-noninterference-ok.bpl index f85cf6367..c71c9e680 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-ok.bpl +++ b/Test/civl/regression-tests/pending-async-noninterference-ok.bpl @@ -15,7 +15,7 @@ modifies x; left action {:layer 1} ASYNC_A () creates A; { - call create_async(A()); + async call A(); } yield procedure {:layer 1} dummy () {} diff --git a/Test/civl/regression-tests/rec-IS1.bpl b/Test/civl/regression-tests/rec-IS1.bpl index e8ed569ff..748499a9a 100644 --- a/Test/civl/regression-tests/rec-IS1.bpl +++ b/Test/civl/regression-tests/rec-IS1.bpl @@ -8,8 +8,8 @@ refines final using Inv; creates main_f''; { if (*) { - } else{ - call create_async(main_f''(l)); + } else { + async call main_f''(l); } } @@ -24,7 +24,7 @@ creates main_f''; assert l != g; if (*) { } else { - call create_async(main_f''(l)); + async call main_f''(l); call set_choice(main_f''(l)); } } \ No newline at end of file diff --git a/Test/civl/regression-tests/rec-IS1.bpl.expect b/Test/civl/regression-tests/rec-IS1.bpl.expect index 6d4df7dad..ac9f53623 100644 --- a/Test/civl/regression-tests/rec-IS1.bpl.expect +++ b/Test/civl/regression-tests/rec-IS1.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors \ No newline at end of file +Boogie program verifier finished with 4 verified, 0 errors \ No newline at end of file