[Civl] Added explicit gates to atomic actions (#911)

This PR allows gates of atomic actions to be explicitly specified. The
convention is as follows:

var {:layer 0,1} x: int;

yield invariant YieldInv();
invariant ...

atomic action Foo()
requires x > 0; // gate (must be sufficient to prove absence of failures
in atomic action)
requires call YieldInv(); // precondition used only in special
circumstances
{
   assert x != 0;
}

---------

Co-authored-by: Shaz Qadeer <[email protected]>

Source/Concurrency/CivlCoreTypes.cs

@@ -52,10 +52,12 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
         DropSetChoice(civlTypeChecker, Impl);
       }
 
-      Gate = HoistAsserts(Impl, civlTypeChecker.Options);
+      ModifiedGlobalVars = new HashSet<Variable>(Impl.Proc.Modifies.Select(x => x.Decl));
+
+      AddGateSufficiencyCheckerAndHoistAsserts(civlTypeChecker);
+
       UsedGlobalVarsInGate = new HashSet<Variable>(VariableCollector.Collect(Gate).Where(x => x is GlobalVariable));
       UsedGlobalVarsInAction = new HashSet<Variable>(VariableCollector.Collect(Impl).Where(x => x is GlobalVariable));
-      ModifiedGlobalVars = new HashSet<Variable>(Impl.Proc.Modifies.Select(x => x.Decl));
 
       InputOutputRelation = ComputeInputOutputRelation(civlTypeChecker, Impl);
       if (ImplWithChoice != null)
@@ -159,6 +161,38 @@ public static Implementation CreateDuplicateImplementation(Implementation impl,
       return duplicateImpl;
     }
 
+    public static void AddGateSufficiencyCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
+    {
+      decls.AddRange(gateSufficiencyCheckerDecls);
+    }
+
+    private static List<Declaration> gateSufficiencyCheckerDecls = new List<Declaration>();
+
+    private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeChecker)
+    {
+      if (ActionDecl.Requires.Count == 0)
+      {
+        Gate = HoistAsserts(Impl, civlTypeChecker.Options);
+        return;
+      }
+
+      var checkerName = $"{Name}_GateSufficiencyChecker";
+      var checkerImpl = new Duplicator().VisitImplementation(Impl);
+      checkerImpl.Name = checkerName;
+      checkerImpl.Attributes = null;
+      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);
+      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))).ToList();
+    }
+
     private Function ComputeInputOutputRelation(CivlTypeChecker civlTypeChecker, Implementation impl)
     {
       var alwaysMap = new Dictionary<Variable, Expr>();

Source/Concurrency/CivlRewriter.cs

@@ -21,8 +21,12 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
       var originalDecls = origActionDecls.Union<Declaration>(origActionImpls).Union(origYieldProcs)
         .Union(origYieldImpls).Union(origYieldInvariants).ToHashSet();
 
-      // Commutativity checks
       var decls = new List<Declaration>();
+
+      // Gate sufficiency checks
+      Action.AddGateSufficiencyCheckers(civlTypeChecker, decls);
+
+      // Commutativity checks
       civlTypeChecker.AtomicActions.ForEach(x =>
       {
         decls.AddRange(new Declaration[] { x.Impl, x.Impl.Proc, x.InputOutputRelation });

Source/Core/AST/Absy.cs

@@ -2481,17 +2481,9 @@ public override void Resolve(ResolutionContext rc)
       }
       if (rc.Proc is ActionDecl actionDecl)
       {
-        if (Layers.Count == 0)
-        {
-          rc.Error(this, "expected layers");
-        }
-        else
+        if (Layers.Count > 0)
         {
-          var assertLayerRange = new LayerRange(Layers[0], Layers[^1]);
-          if (!assertLayerRange.Subset(actionDecl.LayerRange))
-          {
-            rc.Error(this, $"each layer must be in the range {actionDecl.LayerRange}");
-          }
+          rc.Error(this, "did not expect layers");
         }
       }
     }
@@ -3013,9 +3005,7 @@ public override void Typecheck(TypecheckingContext tc)
     {
       var oldProc = tc.Proc;
       tc.Proc = this;
-      tc.GlobalAccessOnlyInOld = true;
       base.Typecheck(tc);
-      tc.GlobalAccessOnlyInOld = false;
       YieldRequires.ForEach(callCmd => callCmd.Typecheck(tc));
       Contract.Assert(tc.Proc == this);
       tc.Proc = oldProc;

Test/civl/inductive-sequentialization/ChangRoberts.bpl

@@ -76,8 +76,7 @@ modifies leader;
     assume (forall {:pool "ORDER"} x: int :: {:add_to_pool "ORDER", x} Pos(pid) < x && x <= Prev(Pos(self)) ==> Below(Pid(x), pid));
     // create prefix
     call create_asyncs(
-      (lambda {:pool "P_INV2"} pa: P :: {:add_to_pool "P_MAIN2", pa} {:add_to_pool "P_INV2", pa}
-        ValidPid(pa->pid) && Pos(pa->pid) < Pos(pid) && pa->self == Next(pa->pid)));
+      (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);
     call set_choice(choice);
@@ -94,9 +93,7 @@ creates P;
   assert Init(pids->val, leader);
   assume {:add_to_pool "INV2", P(ExpectedLeader, Prev(ExpectedLeader))} true;
   call create_asyncs(
-    (lambda {:pool "P_MAIN2"} pa: P :: 
-      {:add_to_pool "P_INV2", pa} 
-      ValidPid(pa->pid) && pa->self == Next(pa->pid)));
+    (lambda pa: P :: ValidPid(pa->pid) && pa->self == Next(pa->pid)));
 }
 
 action {:layer 2} INV1({:linear_in} pids: Set int)

Test/civl/regression-tests/assert-layers.bpl.expect

@@ -1,5 +1,4 @@
 assert-layers.bpl(5,0): Error: expected layers
 assert-layers.bpl(6,0): Error: expected layers
 assert-layers.bpl(8,2): Error: expected layers
-assert-layers.bpl(12,0): Error: expected layers
-4 name resolution errors detected in assert-layers.bpl
+3 name resolution errors detected in assert-layers.bpl

Test/civl/regression-tests/gate-sufficiency-checker.bpl

@@ -0,0 +1,10 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 0,1} x: int;
+
+atomic action {:layer 1} Foo()
+requires x > 0;
+{
+    assert x != 0;
+}

Test/civl/regression-tests/gate-sufficiency-checker.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors

Test/civl/regression-tests/yield-pre-post.bpl

@@ -9,5 +9,9 @@ ensures {:layer 1} g > 0;
 { }
 
 atomic action {:layer 1} A()
-requires {:layer 1} g > 0;
+requires g > 0;
+{}
+
+atomic action {:layer 2} B()
+requires g > 0;
 {}

Test/civl/regression-tests/yield-pre-post.bpl.expect

@@ -1,4 +1,4 @@
 yield-pre-post.bpl(7,20): Error: global variable must be accessed inside old expression: g
 yield-pre-post.bpl(8,19): Error: global variable must be accessed inside old expression: g
-yield-pre-post.bpl(12,20): Error: global variable must be accessed inside old expression: g
-3 type checking errors detected in yield-pre-post.bpl
+yield-pre-post.bpl(16,9): Error: global variable must be available across all layers ([2, 2]) of action B: g
+3 type checking errors detected in yield-pre-post.bpl

Test/civl/samples/treiber-stack.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie -lib:base -lib:node "%s" > "%t"
+// RUN: %parallel-boogie -lib:base -lib:node -vcsSplitOnEveryAssert "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype LocPiece { Left(), Right() }
@@ -162,6 +162,7 @@ preserves call StackDom();
 atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc (Treiber X), x: X)
   returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X))
 modifies ts;
+requires Map_Contains(ts, loc_t);
 {
   var {:linear} one_loc_t: One (Loc (Treiber X));
   var {:linear} treiber: Treiber X;

Test/civl/samples/treiber-stack.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 33 verified, 0 errors
+Boogie program verifier finished with 34 verified, 0 errors