[CIVL] renamed non-blocking -> cooperation, terminates -> cooperates (#…

…314)

* renamed non-blocking -> cooperation, terminates -> cooperates

* added more explanation

Source/Concurrency/CivlTypeChecker.cs

@@ -18,8 +18,8 @@ public class CivlTypeChecker
     private string namePrefix;
 
     public Dictionary<Block, YieldingLoop> yieldingLoops;
-    public Dictionary<Block, HashSet<int>> terminatingLoopHeaders;
-    public HashSet<Procedure> terminatingProcedures;
+    public Dictionary<Block, HashSet<int>> cooperatingLoopHeaders;
+    public HashSet<Procedure> cooperatingProcedures;
 
     public Dictionary<Procedure, AtomicAction> procToAtomicAction;
     public Dictionary<Procedure, AtomicAction> procToIsInvariant;
@@ -56,8 +56,8 @@ public CivlTypeChecker(Program program)
       this.globalVarToLayerRange = new Dictionary<Variable, LayerRange>();
       this.localVarToLayerRange = new Dictionary<Variable, LayerRange>();
       this.yieldingLoops = new Dictionary<Block, YieldingLoop>();
-      this.terminatingLoopHeaders = new Dictionary<Block, HashSet<int>>();
-      this.terminatingProcedures = new HashSet<Procedure>();
+      this.cooperatingLoopHeaders = new Dictionary<Block, HashSet<int>>();
+      this.cooperatingProcedures = new HashSet<Procedure>();
       this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
       this.procToAtomicAction = new Dictionary<Procedure, AtomicAction>();
       this.procToIsInvariant = new Dictionary<Procedure, AtomicAction>();
@@ -627,9 +627,9 @@ private void TypeCheckYieldingProcedureDecls()
 
         YieldingProcVisitor visitor = new YieldingProcVisitor(this, yieldRequires, yieldEnsures);
         visitor.VisitProcedure(proc);
-        if (proc.HasAttribute(CivlAttributes.TERMINATES))
+        if (proc.HasAttribute(CivlAttributes.COOPERATES))
         {
-          terminatingProcedures.Add(proc);
+          cooperatingProcedures.Add(proc);
         }
       }
 
@@ -664,23 +664,23 @@ private void TypeCheckLoopAnnotations()
         foreach (var header in graph.Headers)
         {
           var yieldingLayers = new HashSet<int>();
-          var terminatingLayers = new HashSet<int>();
+          var cooperatingLayers = new HashSet<int>();
           foreach (PredicateCmd predCmd in header.Cmds.TakeWhile(cmd => cmd is PredicateCmd))
           {
             if (predCmd.HasAttribute(CivlAttributes.YIELDS))
             {
               yieldingLayers.UnionWith(absyToLayerNums[predCmd]);
             }
 
-            if (predCmd.HasAttribute(CivlAttributes.TERMINATES))
+            if (predCmd.HasAttribute(CivlAttributes.COOPERATES))
             {
-              terminatingLayers.UnionWith(absyToLayerNums[predCmd]);
+              cooperatingLayers.UnionWith(absyToLayerNums[predCmd]);
             }
           }
 
-          if (yieldingLayers.Intersect(terminatingLayers).Count() != 0)
+          if (yieldingLayers.Intersect(cooperatingLayers).Count() != 0)
           {
-            Error(header, "Loop cannot be both yielding and terminating on the same layer.");
+            Error(header, "Loop cannot be both yielding and cooperating on the same layer.");
             continue;
           }
 
@@ -704,7 +704,7 @@ private void TypeCheckLoopAnnotations()
           }
 
           yieldingLoops[header] = new YieldingLoop(yieldingLayers, yieldInvariants);
-          terminatingLoopHeaders[header] = terminatingLayers;
+          cooperatingLoopHeaders[header] = cooperatingLayers;
         }
       }
     }
@@ -1168,19 +1168,19 @@ public bool IsYieldingLoopHeader(Block block, int layerNum)
       return yieldingLoops[block].layers.Contains(layerNum);
     }
 
-    public bool IsTerminatingLoopHeader(Block block, int layerNum)
+    public bool IsCooperatingLoopHeader(Block block, int layerNum)
     {
-      if (!terminatingLoopHeaders.ContainsKey(block))
+      if (!cooperatingLoopHeaders.ContainsKey(block))
       {
         return false;
       }
 
-      return terminatingLoopHeaders[block].Contains(layerNum);
+      return cooperatingLoopHeaders[block].Contains(layerNum);
     }
 
-    public bool IsTerminatingProcedure(Procedure proc)
+    public bool IsCooperatingProcedure(Procedure proc)
     {
-      return terminatingProcedures.Contains(proc);
+      return cooperatingProcedures.Contains(proc);
     }
 
     public LayerRange GlobalVariableLayerRange(Variable g)

Source/Concurrency/MoverCheck.cs

@@ -58,20 +58,20 @@ where action.layerRange.Contains(IS.inputAction.layerRange.upperLayerNum)
       // Here we include IS abstractions
       foreach (var atomicAction in civlTypeChecker.AllAtomicActions.Where(a => a.IsLeftMover))
       {
-        moverChecking.CreateNonBlockingChecker(atomicAction);
+        moverChecking.CreateCooperationChecker(atomicAction);
       }
 
       // IS abstractions are marked left movers, so here we select regular atomic actions
       // that are not marked left mover but used as abstraction in IS.
       foreach (var atomicAction in civlTypeChecker.inductiveSequentializations.SelectMany(IS => IS.elim.Values)
         .Where(a => !a.IsLeftMover).Distinct())
       {
-        moverChecking.CreateNonBlockingChecker(atomicAction);
+        moverChecking.CreateCooperationChecker(atomicAction);
       }
 
       foreach (var introductionAction in civlTypeChecker.procToIntroductionAction.Values)
       {
-        moverChecking.CreateNonBlockingChecker(introductionAction);
+        moverChecking.CreateCooperationChecker(introductionAction);
       }
     }
 
@@ -269,11 +269,11 @@ private void CreateFailurePreservationChecker(AtomicAction first, AtomicAction s
       AddChecker(checkerName, inputs, outputs, new List<Variable>(), requires, cmds);
     }
 
-    private void CreateNonBlockingChecker(Action action)
+    private void CreateCooperationChecker(Action action)
     {
       if (!action.HasAssumeCmd) return;
 
-      string checkerName = $"NonBlockingChecker_{action.proc.Name}";
+      string checkerName = $"CooperationChecker_{action.proc.Name}";
 
       Implementation impl = action.impl;
       HashSet<Variable> frame = new HashSet<Variable>();
@@ -290,13 +290,13 @@ private void CreateNonBlockingChecker(Action action)
         requires.Add(new Requires(false, assertCmd.Expr));
       }
 
-      AssertCmd nonBlockingCheck = CmdHelper.AssertCmd(
+      AssertCmd cooperationCheck = CmdHelper.AssertCmd(
         action.proc.tok,
-        TransitionRelationComputation.Nonblocking(civlTypeChecker, action, frame),
-        $"Non-blocking check for {action.proc.Name} failed");
+        TransitionRelationComputation.Cooperation(civlTypeChecker, action, frame),
+        $"Cooperation check for {action.proc.Name} failed");
 
       AddChecker(checkerName, new List<Variable>(impl.InParams), new List<Variable>(),
-        new List<Variable>(), requires, new List<Cmd> { nonBlockingCheck });
+        new List<Variable>(), requires, new List<Cmd> { cooperationCheck });
     }
   }
 }

Source/Concurrency/TransitionRelationComputation.cs

@@ -116,13 +116,13 @@ public static Expr Refinement(CivlTypeChecker civlTypeChecker, AtomicAction acti
         string.Format("Transition relation of {0}", action.proc.Name));
     }
 
-    public static Expr Nonblocking(CivlTypeChecker civlTypeChecker, Action action, HashSet<Variable> frame)
+    public static Expr Cooperation(CivlTypeChecker civlTypeChecker, Action action, HashSet<Variable> frame)
     {
       return ComputeTransitionRelation(
         civlTypeChecker,
         action.impl, null,
         frame, null, null, true,
-        string.Format("Nonblocking expression of {0}", action.proc.Name));
+        string.Format("Cooperation expression of {0}", action.proc.Name));
     }
 
     private void EnumeratePaths()

Source/Concurrency/YieldSufficiencyTypeChecker.cs

@@ -239,15 +239,15 @@ private void AtomicityCheck()
         foreach (Block header in implGraph.Headers)
         {
           if (civlTypeChecker.IsYieldingLoopHeader(header, currLayerNum) ||
-              civlTypeChecker.IsTerminatingLoopHeader(header, currLayerNum)) continue;
+              civlTypeChecker.IsCooperatingLoopHeader(header, currLayerNum)) continue;
           initialConstraints[header] = new HashSet<int> {RM};
         }
 
         if (IsMoverProcedure)
         {
           foreach (var call in impl.Blocks.SelectMany(b => b.cmds).OfType<CallCmd>())
           {
-            if (!IsTerminatingCall(call))
+            if (!IsCooperatingCall(call))
             {
               initialConstraints[call] = new HashSet<int> {RM};
             }
@@ -277,9 +277,9 @@ private bool IsMoverProcedure
         get { return yieldingProc is MoverProc && yieldingProc.upperLayer == currLayerNum; }
       }
 
-      private bool IsTerminatingCall(CallCmd call)
+      private bool IsCooperatingCall(CallCmd call)
       {
-        return !IsRecursiveMoverProcedureCall(call) || civlTypeChecker.IsTerminatingProcedure(call.Proc);
+        return !IsRecursiveMoverProcedureCall(call) || civlTypeChecker.IsCooperatingProcedure(call.Proc);
       }
 
       private bool CheckAtomicity(Dictionary<Absy, HashSet<int>> simulationRelation)

Source/Core/CivlAttributes.cs

@@ -26,7 +26,7 @@ public static class CivlAttributes
     public static string REFINES = "refines";
     public static string HIDE = "hide";
 
-    public const string TERMINATES = "terminates";
+    public const string COOPERATES = "cooperates";
 
     public const string LINEAR = "linear";
     public const string LINEAR_IN = "linear_in";
@@ -52,7 +52,7 @@ public static class CivlAttributes
       COMMUTATIVITY, LEMMA, WITNESS,
       PENDING_ASYNC, IS, IS_INVARIANT, IS_ABSTRACTION, ELIM, CHOICE,
       YIELD_REQUIRES, YIELD_ENSURES, YIELD_PRESERVES, YIELD_LOOP,
-      TERMINATES
+      COOPERATES
     };
 
     private static string[] LINEAR_ATTRIBUTES =

Source/Core/CommandLineOptions.cs

@@ -1934,8 +1934,8 @@ Invocation of yield invariant.
      {:refines ""action""}
        Refined atomic action of a yielding procedure.
 
-     {:terminates}
-       Terminating loop.
+     {:cooperates}
+       Cooperating loop or mover procedure.
 
      {:linear ""domain""}
        Permission type for domain.

Test/civl/GC.bpl

@@ -473,7 +473,7 @@ requires {:layer 98,99,100} tid == GcTid;
     call snapColor := GhostReadColor100();
     while (localSweepPtr < memHi)
     invariant {:layer 95,96}{:yields} true;
-    invariant {:terminates} {:layer 97,98,99,100} true;
+    invariant {:cooperates} {:layer 97,98,99,100} true;
     invariant {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0);
     invariant {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
     invariant {:layer 100} SweepPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase);
@@ -585,7 +585,7 @@ requires {:layer 99} tid == GcTid;
     {:yield_loop "Yield_MsWellFormed", tid, 0}
     {:yield_loop "Yield_CollectorPhase_98", tid, old(collectorPhase)}
     true;
-    invariant {:terminates}{:layer 99} true;
+    invariant {:cooperates}{:layer 99} true;
     invariant {:layer 99} Mutators == mutatorsInRootScanBarrier && rootScanOn;
     invariant {:layer 99} 0 <= i && i <= numRoots;
     invariant {:layer 99} Color == (lambda u: int :: if memAddr(u) && White(snapColor[u]) && (exists k: int :: 0 <= k && k < i && root[k] == u) then GRAY() else snapColor[u]);

Test/civl/async/2agree_1.bpl

@@ -42,7 +42,7 @@ requires {:layer 2} perm(p);
 // ###########################################################################
 // Event handlers of process B
 
-procedure {:yields} {:layer 2} {:left} {:terminates}  propose_by_a (val : int, {:linear_in "lin"} p : int)
+procedure {:yields} {:layer 2} {:left} {:cooperates}  propose_by_a (val : int, {:linear_in "lin"} p : int)
 requires {:layer 2} perm(p);
 requires {:layer 2} val_a == val;
 ensures {:layer 2} Consistent(val_a, val_b, done_a, done_b);
@@ -75,7 +75,7 @@ modifies done_b;
 // ###########################################################################
 // Event handlers of process A
 
-procedure {:yields} {:layer 2} {:left} {:terminates} propose_by_b (val : int, {:linear_in "lin"} p : int)
+procedure {:yields} {:layer 2} {:left} {:cooperates} propose_by_b (val : int, {:linear_in "lin"} p : int)
 requires {:layer 2} perm(p);
 requires {:layer 2} val_b == val;
 ensures {:layer 2} Consistent(val_a, val_b, done_a, done_b);

Test/civl/async/2agree_2.bpl

@@ -37,7 +37,7 @@ requires {:layer 2} perm(p);
 // ###########################################################################
 // Event handlers of process B
 
-procedure {:yields} {:layer 2} {:left} {:terminates}  propose_by_a (val : int, {:linear_in "lin"} p : int)
+procedure {:yields} {:layer 2} {:left} {:cooperates}  propose_by_a (val : int, {:linear_in "lin"} p : int)
 requires {:layer 2} perm(p);
 requires {:layer 2} val_a == val;
 ensures {:layer 2} done_a && done_b && val_a == val_b;
@@ -70,7 +70,7 @@ modifies done_b;
 // ###########################################################################
 // Event handlers of process A
 
-procedure {:yields} {:layer 2} {:left} {:terminates} propose_by_b (val : int, {:linear_in "lin"} p : int)
+procedure {:yields} {:layer 2} {:left} {:cooperates} propose_by_b (val : int, {:linear_in "lin"} p : int)
 requires {:layer 2} perm(p);
 requires {:layer 2} val_b == val;
 ensures {:layer 2} done_a && done_b && val_a == val_b;

Test/civl/async/2agree_3.bpl

@@ -33,7 +33,7 @@ requires {:layer 2} perm(p);
 // ###########################################################################
 // Event handlers of process B
 
-procedure {:yields} {:layer 2} {:left} {:terminates}  propose_by_a (val : int, {:linear_in "lin"} p : int)
+procedure {:yields} {:layer 2} {:left} {:cooperates}  propose_by_a (val : int, {:linear_in "lin"} p : int)
 requires {:layer 2} perm(p);
 requires {:layer 2} val_a == val;
 ensures {:layer 2} val_a == val_b;
@@ -63,7 +63,7 @@ ensures {:layer 2} val_a == val_b;
 // ###########################################################################
 // Event handlers of process A
 
-procedure {:yields} {:layer 2} {:left} {:terminates} propose_by_b (val : int, {:linear_in "lin"} p : int)
+procedure {:yields} {:layer 2} {:left} {:cooperates} propose_by_b (val : int, {:linear_in "lin"} p : int)
 requires {:layer 2} perm(p);
 requires {:layer 2} val_b == val;
 ensures {:layer 2} val_a == val_b;

Test/civl/async/2pc-triggers.bpl

@@ -242,7 +242,7 @@ Coordinator_TransactionReq () returns (xid: Xid)
   call snapshot := GhostRead_10();
   i := 1;
   while (i <= numParticipants)
-  invariant {:terminates} {:layer 8,9,10} true;
+  invariant {:cooperates} {:layer 8,9,10} true;
   invariant {:layer 8} Inv_8(state, B, votes);
   invariant {:layer 8,10} pairs == (lambda p: Pair :: pair(xid, mid#Pair(p), p) && i <= mid#Pair(p));
   invariant {:layer 8} votes[xid] == -1 || (forall p: Pair :: pairs[p] ==> UndecidedOrCommitted(state[xid][mid#Pair(p)]));
@@ -326,7 +326,7 @@ Coordinator_VoteYes (xid: Xid, mid: Mid, {:linear_in "pair"} pair: Pair)
     assert {:layer 8} xUndecidedOrCommitted(state[xid]);
     i := 1;
     while (i <= numParticipants)
-    invariant {:layer 8} {:terminates} true;
+    invariant {:layer 8} {:cooperates} true;
     invariant {:layer 8} 1 <= i && i <= numParticipants + 1;
     invariant {:layer 8} Inv_8(state, B, votes);
     invariant {:layer 8} ExistsMonotoneExtension(snapshot, state, xid);
@@ -370,7 +370,7 @@ Coordinator_VoteNo (xid: Xid, mid: Mid, {:linear_in "pair"} pair: Pair)
   {
     i := 1;
     while (i <= numParticipants)
-    invariant {:layer 8} {:terminates} true;
+    invariant {:layer 8} {:cooperates} true;
     invariant {:layer 8} 1 <= i && i <= numParticipants + 1;
     invariant {:layer 8} Aborted(state[xid][CoordinatorMid]);
     invariant {:layer 8} xUndecidedOrAborted(state[xid]);

Test/civl/async/2pc.bpl

@@ -231,7 +231,7 @@ Coordinator_TransactionReq () returns (xid: Xid)
   call snapshot := GhostRead_10();
   i := 1;
   while (i <= numParticipants)
-  invariant {:terminates} {:layer 8,9,10} true;
+  invariant {:cooperates} {:layer 8,9,10} true;
   invariant {:layer 8} Inv_8(state, B, votes);
   invariant {:layer 8,10} pairs == (lambda p: Pair :: pair(xid, mid#Pair(p), p) && i <= mid#Pair(p));
   invariant {:layer 8} votes[xid] == -1 || (forall p: Pair :: pairs[p] ==> UndecidedOrCommitted(state[xid][mid#Pair(p)]));
@@ -311,7 +311,7 @@ Coordinator_VoteYes (xid: Xid, mid: Mid, {:linear_in "pair"} pair: Pair)
     assert {:layer 8} xUndecidedOrCommitted(state[xid]);
     i := 1;
     while (i <= numParticipants)
-    invariant {:layer 8} {:terminates} true;
+    invariant {:layer 8} {:cooperates} true;
     invariant {:layer 8} 1 <= i && i <= numParticipants + 1;
     invariant {:layer 8} Inv_8(state, B, votes);
     invariant {:layer 8} ExistsMonotoneExtension(snapshot, state, xid);
@@ -349,7 +349,7 @@ Coordinator_VoteNo (xid: Xid, mid: Mid, {:linear_in "pair"} pair: Pair)
   {
     i := 1;
     while (i <= numParticipants)
-    invariant {:layer 8} {:terminates} true;
+    invariant {:layer 8} {:cooperates} true;
     invariant {:layer 8} 1 <= i && i <= numParticipants + 1;
     invariant {:layer 8} Aborted(state[xid][CoordinatorMid]);
     invariant {:layer 8} xUndecidedOrAborted(state[xid]);

Test/civl/async/inc-dec-2.bpl

@@ -22,7 +22,7 @@ procedure {:yields} {:layer 1} {:refines "skip"} Main ()
   i := 0;
   call old_x := snapshot_x();
   while (i != N)
-  invariant {:layer 1} {:terminates} true;
+  invariant {:layer 1} {:cooperates} true;
   invariant {:layer 1} x == old_x;
   {
     async call {:sync} inc();

Test/civl/async/inc-dec.bpl

@@ -26,7 +26,7 @@ ensures {:layer 1} x == old(x) + N;
 
   i := 0;
   while (i != N)
-  invariant {:layer 1} {:terminates} true;
+  invariant {:layer 1} {:cooperates} true;
   invariant {:layer 1} x == old(x) + i;
   {
     i := i + 1;
@@ -42,7 +42,7 @@ ensures {:layer 1} x == old(x) - N;
 
   i := 0;
   while (i != N)
-  invariant {:layer 1} {:terminates} true;
+  invariant {:layer 1} {:cooperates} true;
   invariant {:layer 1} x == old(x) - i;
   {
     i := i + 1;

Test/civl/async/leader.bpl

@@ -69,7 +69,7 @@ ensures {:layer 1} all_decided(init_val, dec_dom, dec_val);
   s := 1;
   perms' := perms;
   while (s <= N)
-  invariant {:layer 1}{:terminates} true;
+  invariant {:layer 1}{:cooperates} true;
   invariant {:layer 1} perms' == s_perms_geq(s);
   invariant {:layer 1} inv_val(s, init_val, col_dom, col_val);
   invariant {:layer 1} s > N ==> all_decided(init_val, dec_dom, dec_val);
@@ -96,7 +96,7 @@ modifies col_dom, col_val, dec_dom, dec_val;
   r := 1;
   call v := read_init_val(s);
   while (r <= N)
-  invariant {:layer 1}{:terminates} true;
+  invariant {:layer 1}{:cooperates} true;
   invariant {:layer 1} perms' == s_r_perms_geq(s,r);
   invariant {:layer 1} inv_val'(s, r, init_val, col_dom, col_val);
   invariant {:layer 1} s == N ==> all_decided'(r, init_val, dec_dom, dec_val);