From 2e77c2845e3243479e7497b83bde7fa2ca174005 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Wed, 2 Dec 2020 15:45:18 -0800 Subject: [PATCH] [CIVL] renamed non-blocking -> cooperation, terminates -> cooperates (#314) * renamed non-blocking -> cooperation, terminates -> cooperates * added more explanation --- Source/Concurrency/CivlTypeChecker.cs | 34 +++++++++---------- Source/Concurrency/MoverCheck.cs | 18 +++++----- .../TransitionRelationComputation.cs | 4 +-- .../YieldSufficiencyTypeChecker.cs | 8 ++--- Source/Core/CivlAttributes.cs | 4 +-- Source/Core/CommandLineOptions.cs | 4 +-- Test/civl/GC.bpl | 4 +-- Test/civl/async/2agree_1.bpl | 4 +-- Test/civl/async/2agree_2.bpl | 4 +-- Test/civl/async/2agree_3.bpl | 4 +-- Test/civl/async/2pc-triggers.bpl | 6 ++-- Test/civl/async/2pc.bpl | 6 ++-- Test/civl/async/inc-dec-2.bpl | 2 +- Test/civl/async/inc-dec.bpl | 4 +-- Test/civl/async/leader.bpl | 4 +-- Test/civl/async/rec-inc.bpl | 2 +- Test/civl/async/tds.bpl | 2 +- Test/civl/async/tds2.bpl | 2 +- Test/civl/bar.bpl | 2 +- Test/civl/cyclic-concur.bpl | 6 ++-- Test/civl/foo.bpl | 2 +- Test/civl/inc-dec.bpl | 4 +-- Test/civl/inductive-sequentialization/2PC.bpl | 6 ++-- .../BroadcastConsensus.bpl | 4 +-- .../ChangRoberts.bpl | 2 +- .../ChangRoberts_pendingAsyncs.bpl | 2 +- .../inductive-sequentialization/NBuyer.bpl | 4 +-- .../paxos/PaxosImpl.bpl | 6 ++-- Test/civl/intro-nonblocking.bpl.expect | 2 +- Test/civl/lamport.bpl | 2 +- Test/civl/lamport_prophecy.bpl | 2 +- Test/civl/left-mover.bpl.expect | 2 +- Test/civl/lock.bpl | 2 +- Test/civl/lock2.bpl | 2 +- Test/civl/pending-async-1.bpl | 2 +- Test/civl/termination2.bpl | 2 +- 36 files changed, 85 insertions(+), 85 deletions(-) diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 2983ba89f..bc368ce44 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -18,8 +18,8 @@ public class CivlTypeChecker private string namePrefix; public Dictionary yieldingLoops; - public Dictionary> terminatingLoopHeaders; - public HashSet terminatingProcedures; + public Dictionary> cooperatingLoopHeaders; + public HashSet cooperatingProcedures; public Dictionary procToAtomicAction; public Dictionary procToIsInvariant; @@ -56,8 +56,8 @@ public CivlTypeChecker(Program program) this.globalVarToLayerRange = new Dictionary(); this.localVarToLayerRange = new Dictionary(); this.yieldingLoops = new Dictionary(); - this.terminatingLoopHeaders = new Dictionary>(); - this.terminatingProcedures = new HashSet(); + this.cooperatingLoopHeaders = new Dictionary>(); + this.cooperatingProcedures = new HashSet(); this.absyToLayerNums = new Dictionary>(); this.procToAtomicAction = new Dictionary(); this.procToIsInvariant = new Dictionary(); @@ -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,7 +664,7 @@ private void TypeCheckLoopAnnotations() foreach (var header in graph.Headers) { var yieldingLayers = new HashSet(); - var terminatingLayers = new HashSet(); + var cooperatingLayers = new HashSet(); foreach (PredicateCmd predCmd in header.Cmds.TakeWhile(cmd => cmd is PredicateCmd)) { if (predCmd.HasAttribute(CivlAttributes.YIELDS)) @@ -672,15 +672,15 @@ private void TypeCheckLoopAnnotations() 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) diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 68666aeca..c43e49d7b 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -58,7 +58,7 @@ 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 @@ -66,12 +66,12 @@ where action.layerRange.Contains(IS.inputAction.layerRange.upperLayerNum) 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(), 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 frame = new HashSet(); @@ -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(impl.InParams), new List(), - new List(), requires, new List { nonBlockingCheck }); + new List(), requires, new List { cooperationCheck }); } } } \ No newline at end of file diff --git a/Source/Concurrency/TransitionRelationComputation.cs b/Source/Concurrency/TransitionRelationComputation.cs index ed473deea..dd00a7acf 100644 --- a/Source/Concurrency/TransitionRelationComputation.cs +++ b/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 frame) + public static Expr Cooperation(CivlTypeChecker civlTypeChecker, Action action, HashSet 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() diff --git a/Source/Concurrency/YieldSufficiencyTypeChecker.cs b/Source/Concurrency/YieldSufficiencyTypeChecker.cs index e4464ef75..48277a4c3 100644 --- a/Source/Concurrency/YieldSufficiencyTypeChecker.cs +++ b/Source/Concurrency/YieldSufficiencyTypeChecker.cs @@ -239,7 +239,7 @@ 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 {RM}; } @@ -247,7 +247,7 @@ private void AtomicityCheck() { foreach (var call in impl.Blocks.SelectMany(b => b.cmds).OfType()) { - if (!IsTerminatingCall(call)) + if (!IsCooperatingCall(call)) { initialConstraints[call] = new HashSet {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> simulationRelation) diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index e3025e485..740f36aa1 100644 --- a/Source/Core/CivlAttributes.cs +++ b/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 = diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index d364aeadb..4f294784a 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/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. diff --git a/Test/civl/GC.bpl b/Test/civl/GC.bpl index e5cbc5438..197b39e8d 100644 --- a/Test/civl/GC.bpl +++ b/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]); diff --git a/Test/civl/async/2agree_1.bpl b/Test/civl/async/2agree_1.bpl index 28fa51e12..003dbfc4b 100644 --- a/Test/civl/async/2agree_1.bpl +++ b/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); diff --git a/Test/civl/async/2agree_2.bpl b/Test/civl/async/2agree_2.bpl index b87395328..56c087eb9 100644 --- a/Test/civl/async/2agree_2.bpl +++ 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; diff --git a/Test/civl/async/2agree_3.bpl b/Test/civl/async/2agree_3.bpl index b650c0e90..93a1f0cc9 100644 --- a/Test/civl/async/2agree_3.bpl +++ 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; diff --git a/Test/civl/async/2pc-triggers.bpl b/Test/civl/async/2pc-triggers.bpl index 452e8e536..c0cda8fe7 100644 --- a/Test/civl/async/2pc-triggers.bpl +++ 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]); diff --git a/Test/civl/async/2pc.bpl b/Test/civl/async/2pc.bpl index eca5ad33a..5f40ff0f1 100644 --- a/Test/civl/async/2pc.bpl +++ b/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]); diff --git a/Test/civl/async/inc-dec-2.bpl b/Test/civl/async/inc-dec-2.bpl index 076cc5eb3..3e88e50f2 100644 --- a/Test/civl/async/inc-dec-2.bpl +++ b/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(); diff --git a/Test/civl/async/inc-dec.bpl b/Test/civl/async/inc-dec.bpl index 2c21048fd..5ca55068a 100644 --- a/Test/civl/async/inc-dec.bpl +++ b/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; diff --git a/Test/civl/async/leader.bpl b/Test/civl/async/leader.bpl index 412373d7d..9eba116a7 100644 --- a/Test/civl/async/leader.bpl +++ b/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); diff --git a/Test/civl/async/rec-inc.bpl b/Test/civl/async/rec-inc.bpl index 14b237f5d..ac29bec7c 100644 --- a/Test/civl/async/rec-inc.bpl +++ b/Test/civl/async/rec-inc.bpl @@ -13,7 +13,7 @@ requires {:layer 1} n >= 0; call inc(n); } -procedure {:yields} {:left} {:layer 1} {:terminates} inc (i : int) +procedure {:yields} {:left} {:layer 1} {:cooperates} inc (i : int) modifies x; requires {:layer 1} i >= 0; ensures {:layer 1} x == old(x) + i; diff --git a/Test/civl/async/tds.bpl b/Test/civl/async/tds.bpl index 88c5e6c40..9a2377860 100644 --- a/Test/civl/async/tds.bpl +++ b/Test/civl/async/tds.bpl @@ -80,7 +80,7 @@ procedure {:yields} {:layer 3} {:refines "atomic_server"} server3({:linear "tid" call snapshot := StatusSnapshot(); tids' := tids; while (i < n) - invariant {:terminates} {:layer 3} true; + invariant {:cooperates} {:layer 3} true; invariant {:layer 3} 0 <= i && i <= n; invariant {:layer 3} (forall j: int :: i <= j && j < n <==> tids'[j]); invariant {:layer 3} status == (lambda j: int :: if (0 <= j && j < i) then CREATED else snapshot[j]); diff --git a/Test/civl/async/tds2.bpl b/Test/civl/async/tds2.bpl index eedba140a..4976d0606 100644 --- a/Test/civl/async/tds2.bpl +++ b/Test/civl/async/tds2.bpl @@ -64,7 +64,7 @@ procedure {:yields} {:layer 1} {:refines "AtomicMain"} Main({:linear_in "tid"} t tids' := tids; call snapshot := StatusSnapshot(); while (i < n) - invariant {:terminates} {:layer 1} true; + invariant {:cooperates} {:layer 1} true; invariant {:layer 1} 0 <= i && i <= n; invariant {:layer 1} (forall j: int :: i <= j && j < n <==> tids'[j]); invariant {:layer 1} status == (lambda j: int :: if (0 <= j && j < i) then FINISHED else snapshot[j]); diff --git a/Test/civl/bar.bpl b/Test/civl/bar.bpl index 6811a8c2a..2b671bcdc 100644 --- a/Test/civl/bar.bpl +++ b/Test/civl/bar.bpl @@ -37,7 +37,7 @@ procedure {:yields} {:layer 1} PD() procedure {:yields} {:layer 1} Main2() { while (*) - invariant {:terminates} {:layer 1} true; + invariant {:cooperates} {:layer 1} true; { async call PB(); async call PE(); diff --git a/Test/civl/cyclic-concur.bpl b/Test/civl/cyclic-concur.bpl index dedbecd40..bbe2a2b5e 100644 --- a/Test/civl/cyclic-concur.bpl +++ b/Test/civl/cyclic-concur.bpl @@ -15,7 +15,7 @@ procedure {:yields} {:layer 1} {:refines "MAIN"} main () async call {:sync} a(); } -procedure {:yields} {:layer 1} {:left} {:terminates} a () +procedure {:yields} {:layer 1} {:left} {:cooperates} a () modifies x; ensures {:layer 1} x > old(x) && (x - old(x)) mod 6 == 0; { @@ -23,7 +23,7 @@ ensures {:layer 1} x > old(x) && (x - old(x)) mod 6 == 0; async call {:sync} b(); } -procedure {:yields} {:layer 1} {:left} {:terminates} b () +procedure {:yields} {:layer 1} {:left} {:cooperates} b () modifies x; ensures {:layer 1} x > old(x) && (x - old(x)) mod 6 == 5; { @@ -31,7 +31,7 @@ ensures {:layer 1} x > old(x) && (x - old(x)) mod 6 == 5; async call {:sync} c(); } -procedure {:yields} {:layer 1} {:left} {:terminates} c () +procedure {:yields} {:layer 1} {:left} {:cooperates} c () modifies x; ensures {:layer 1} x > old(x) && (x - old(x)) mod 6 == 3; { diff --git a/Test/civl/foo.bpl b/Test/civl/foo.bpl index a4a7a439d..6bef1b7a9 100644 --- a/Test/civl/foo.bpl +++ b/Test/civl/foo.bpl @@ -39,7 +39,7 @@ procedure {:yields} {:layer 1} PD() procedure {:yields} {:layer 1} Main() { while (*) - invariant {:terminates} {:layer 1} true; + invariant {:cooperates} {:layer 1} true; { async call PB(); async call PE(); diff --git a/Test/civl/inc-dec.bpl b/Test/civl/inc-dec.bpl index 42bd501de..7e675c7ed 100644 --- a/Test/civl/inc-dec.bpl +++ b/Test/civl/inc-dec.bpl @@ -25,7 +25,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; diff --git a/Test/civl/inductive-sequentialization/2PC.bpl b/Test/civl/inductive-sequentialization/2PC.bpl index 253174c2a..722894d14 100644 --- a/Test/civl/inductive-sequentialization/2PC.bpl +++ b/Test/civl/inductive-sequentialization/2PC.bpl @@ -344,7 +344,7 @@ requires {:layer 1} Init(pids, ReqCH, VoteCH, DecCH, decisions); async call coordinator1(pid); i := 1; while (i <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= i && i <= n+1; invariant {:layer 1} (forall ii:int :: pid(ii) && ii >= i ==> pids'[ii]); invariant {:layer 1} PAs == MapAddPA(SingletonPA(Coordinator1(0)), (lambda pa:PA :: if is#Participant1(pa) && pid(pid#Participant1(pa)) && pid#Participant1(pa) < i then 1 else 0)); @@ -392,7 +392,7 @@ requires {:layer 1} (forall vv:vote :: VoteCH[vv] >= 0); call old_ReqCH := Snapshot_ReqCH(); i := 1; while (i <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= i && i <= n+1; invariant {:layer 1} ReqCH == (lambda ii:int :: if pid(ii) && ii < i then old_ReqCH[ii] + 1 else old_ReqCH[ii]); { @@ -434,7 +434,7 @@ requires {:layer 1} (forall vv:vote :: VoteCH[vv] >= 0); call set_decision(pid, d); i := 1; while (i <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= i && i <= n+1; invariant {:layer 1} DecCH == (lambda ii:int :: (lambda dd:decision :: if pid(ii) && ii < i && dd == d then old_DecCH[ii][dd] + 1 else old_DecCH[ii][dd])); { diff --git a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl index cff57b2f2..20753958d 100644 --- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl +++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl @@ -228,7 +228,7 @@ requires {:layer 1} CH == MultisetEmpty; rr := pidsCollect; i := 1; while (i <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= i && i <= n + 1; invariant {:layer 1} ss == (lambda ii:pid :: pid(ii) && ii >= i) && ss == rr; invariant {:layer 1} PAs == InitialPAs(i); @@ -252,7 +252,7 @@ requires {:layer 1} pid(i); call v := get_value(i); j := 1; while (j <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= j && j <= n+1; invariant {:layer 1} CH_low == (lambda jj: pid :: (if pid(jj) && jj < j then MultisetPlus(old_CH_low[jj], MultisetSingleton(value[i])) else old_CH_low[jj])); { diff --git a/Test/civl/inductive-sequentialization/ChangRoberts.bpl b/Test/civl/inductive-sequentialization/ChangRoberts.bpl index bc6c653cb..b246c6ac2 100644 --- a/Test/civl/inductive-sequentialization/ChangRoberts.bpl +++ b/Test/civl/inductive-sequentialization/ChangRoberts.bpl @@ -264,7 +264,7 @@ requires {:layer 1} Init(pids, channel, terminated, id, leader); pids' := pids; i := 1; while (i <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= i && i <= n+1; invariant {:layer 1} (forall ii:int :: pid(ii) && ii >= i ==> pids'[ii]); invariant {:layer 1} PAs == (lambda pa:PA :: if is#PInit_PA(pa) && pid(pid#PInit_PA(pa)) && pid#PInit_PA(pa) < i then 1 else 0); diff --git a/Test/civl/inductive-sequentialization/ChangRoberts_pendingAsyncs.bpl b/Test/civl/inductive-sequentialization/ChangRoberts_pendingAsyncs.bpl index 4600273ee..b1ff1856f 100644 --- a/Test/civl/inductive-sequentialization/ChangRoberts_pendingAsyncs.bpl +++ b/Test/civl/inductive-sequentialization/ChangRoberts_pendingAsyncs.bpl @@ -267,7 +267,7 @@ requires {:layer 1} Init(pids, channel, pendingAsyncs, id, leader); pids' := pids; i := 1; while (i <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= i && i <= n+1; invariant {:layer 1} (forall ii:int :: pid(ii) && ii >= i ==> pids'[ii]); invariant {:layer 1} PAs == (lambda pa:PA :: if is#PInit_PA(pa) && pid(pid#PInit_PA(pa)) && pid#PInit_PA(pa) < i then 1 else 0); diff --git a/Test/civl/inductive-sequentialization/NBuyer.bpl b/Test/civl/inductive-sequentialization/NBuyer.bpl index aa0f910c7..4709dd42a 100644 --- a/Test/civl/inductive-sequentialization/NBuyer.bpl +++ b/Test/civl/inductive-sequentialization/NBuyer.bpl @@ -468,7 +468,7 @@ requires {:layer 1} Init(pids, ReqCH, QuoteCH, RemCH, DecCH, contribution); async call lastBuyer(pid); i := 2; while (i < n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 2 <= i && i <= n; invariant {:layer 1} (forall ii:int :: middleBuyerID(ii) && ii >= i ==> pids'[ii]); invariant {:layer 1} PAs == MapAddPA4(SellerInitPA(0), FirstBuyerInitPA(1), LastBuyerPA(n), (lambda pa:PA :: if is#MiddleBuyerPA(pa) && middleBuyerID(pid#MiddleBuyerPA(pa)) && pid#MiddleBuyerPA(pa) < i then 1 else 0)); @@ -490,7 +490,7 @@ requires {:layer 1} sellerID(pid); call receive_req(); i := 1; while (i <= n) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= i && i <= n+1; invariant {:layer 1} QuoteCH == (lambda ii:int :: (lambda q:int :: if buyerID(ii) && ii < i && q == price then old_QuoteCH[ii][q] + 1 else old_QuoteCH[ii][q])); { diff --git a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl index d125febe4..d1d531e38 100644 --- a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl +++ b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl @@ -90,7 +90,7 @@ requires {:layer 1} InitLow(acceptorState, joinChannel, voteChannel, permJoinCha r := 0; rs' := rs; while (*) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 0 <= r; invariant {:layer 1} (forall r': Round :: r < r' ==> rs'[r']); invariant {:layer 1} PAs == (lambda pa: PA :: if (is#StartRound_PA(pa) && round#StartRound_PA(pa) == round_lin#StartRound_PA(pa) && Round(round#StartRound_PA(pa)) && round#StartRound_PA(pa) <= r) then 1 else 0); @@ -116,7 +116,7 @@ requires {:layer 1} InvChannels(joinChannel, permJoinChannel, voteChannel, permV call ps, ps' := SplitPermissions(r_lin); n := 1; while (n <= numNodes) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= n && n <= numNodes+1; invariant {:layer 1} (forall n': Node :: n <= n' && n' <= numNodes ==> ps[JoinPerm(r, n')]); invariant {:layer 1} PAs == (lambda pa: PA :: if is#Join_PA(pa) && round#Join_PA(pa) == r && 1 <= node#Join_PA(pa) && node#Join_PA(pa) < n && p#Join_PA(pa) == JoinPerm(round#Join_PA(pa), node#Join_PA(pa)) then 1 else 0); @@ -196,7 +196,7 @@ requires {:layer 1} Inv(joinedNodes, voteInfo, acceptorState, permJoinChannel, p call ps', cp := SplitConcludePermission(r, ps); n := 1; while (n <= numNodes) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 1 <= n && n <= numNodes+1; invariant {:layer 1} (forall n': Node :: n <= n' && n' <= numNodes ==> ps'[VotePerm(r, n')]); invariant {:layer 1} PAs == (lambda pa: PA :: if is#Vote_PA(pa) && round#Vote_PA(pa) == r && 1 <= node#Vote_PA(pa) && node#Vote_PA(pa) < n && value#Vote_PA(pa) == maxValue && p#Vote_PA(pa) == VotePerm(round#Vote_PA(pa), node#Vote_PA(pa)) then 1 else 0); diff --git a/Test/civl/intro-nonblocking.bpl.expect b/Test/civl/intro-nonblocking.bpl.expect index e53dbecd4..464301338 100644 --- a/Test/civl/intro-nonblocking.bpl.expect +++ b/Test/civl/intro-nonblocking.bpl.expect @@ -1,4 +1,4 @@ -intro-nonblocking.bpl(4,30): Error BP5001: Non-blocking check for intro failed +intro-nonblocking.bpl(4,30): Error BP5001: Cooperation check for intro failed Execution trace: (0,0): init diff --git a/Test/civl/lamport.bpl b/Test/civl/lamport.bpl index 25a6d9972..75e837180 100644 --- a/Test/civl/lamport.bpl +++ b/Test/civl/lamport.bpl @@ -33,7 +33,7 @@ Main() assert {:layer 1} Trigger(0); i := 0; while (i < N) - invariant {:terminates} {:layer 1} true; + invariant {:cooperates} {:layer 1} true; invariant {:layer 1} ind_inv(done, y, x); { async call Proc(i); diff --git a/Test/civl/lamport_prophecy.bpl b/Test/civl/lamport_prophecy.bpl index 5e5154ae8..1424aad71 100644 --- a/Test/civl/lamport_prophecy.bpl +++ b/Test/civl/lamport_prophecy.bpl @@ -45,7 +45,7 @@ requires {:layer 1} IsProcId(p) && IsProcId(c) && p == c; yield; assert {:layer 1} Invariant(i, p, c, x); while (i < N) - invariant {:terminates} {:layer 0,1,2} true; + invariant {:cooperates} {:layer 0,1,2} true; invariant {:layer 1} (IsProcId(i) || i == N) && IsProcId(p) && IsProcId(c) && (p == c || x[c] == 1); invariant {:layer 2} (IsProcId(i) || i == N) && IsProcId(c) && (i <= (c+1) mod N || y[(c+1) mod N] == 1); { diff --git a/Test/civl/left-mover.bpl.expect b/Test/civl/left-mover.bpl.expect index f900d250b..422ca869c 100644 --- a/Test/civl/left-mover.bpl.expect +++ b/Test/civl/left-mover.bpl.expect @@ -8,7 +8,7 @@ Execution trace: left-mover.bpl(19,32): inline$init$0$Entry left-mover.bpl(8,5): inline$inc$0$anon0 left-mover.bpl(6,30): inline$inc$0$Return -left-mover.bpl(26,30): Error BP5001: Non-blocking check for block failed +left-mover.bpl(26,30): Error BP5001: Cooperation check for block failed Execution trace: (0,0): init diff --git a/Test/civl/lock.bpl b/Test/civl/lock.bpl index ac276e233..2cd2005b1 100644 --- a/Test/civl/lock.bpl +++ b/Test/civl/lock.bpl @@ -5,7 +5,7 @@ var {:layer 0,2} b: bool; procedure {:yields} {:layer 2} main() { while (*) - invariant {:terminates} {:layer 1,2} true; + invariant {:cooperates} {:layer 1,2} true; { async call Customer(); } diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl index 439a2a816..5c4a5e10d 100644 --- a/Test/civl/lock2.bpl +++ b/Test/civl/lock2.bpl @@ -5,7 +5,7 @@ var {:layer 0,2} b: int; procedure {:yields} {:layer 2} main() { while (*) - invariant {:terminates} {:layer 1,2} true; + invariant {:cooperates} {:layer 1,2} true; { async call Customer(); } diff --git a/Test/civl/pending-async-1.bpl b/Test/civl/pending-async-1.bpl index 80003b271..7b3971984 100644 --- a/Test/civl/pending-async-1.bpl +++ b/Test/civl/pending-async-1.bpl @@ -86,7 +86,7 @@ procedure {:yields}{:layer 1}{:refines "TEST5"} test5 () i := 0; while (i < 10) - invariant {:layer 1}{:terminates} true; + invariant {:layer 1}{:cooperates} true; invariant {:layer 1} 0 <= i && i <= 10; invariant {:layer 1} PAs == NoPAs()[A_PA() := i]; { diff --git a/Test/civl/termination2.bpl b/Test/civl/termination2.bpl index 0629dd99f..04732e6da 100644 --- a/Test/civl/termination2.bpl +++ b/Test/civl/termination2.bpl @@ -9,7 +9,7 @@ procedure {:yields} {:layer 0} Y(); procedure {:yields} {:layer 1} main() { call X(); while (*) - invariant {:terminates} {:layer 1} true; + invariant {:cooperates} {:layer 1} true; { call Y(); }