From 29a06a9c63907a8eef430c63c8bd963523a521d2 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 9 Nov 2024 17:01:18 -0800 Subject: [PATCH] [Civl] Bug fix in anonymous actions (#981) --- Source/Concurrency/LinearRewriter.cs | 9 +- Source/Concurrency/LinearTypeChecker.cs | 10 +- Source/Concurrency/YieldingProcDuplicator.cs | 2 +- Source/Core/Analysis/ModSetCollector.cs | 9 + Source/Core/BoogiePL.atg | 8 +- Source/Core/CivlAttributes.cs | 5 + Source/Core/Parser.cs | 8 +- Test/civl/large-samples/shared-vector.bpl | 117 +++++----- Test/civl/large-samples/treiber-stack.bpl | 202 ++++++++---------- Test/civl/paxos/PaxosImpl.bpl | 50 ++--- .../anonymous-action-fail.bpl | 9 + .../anonymous-action-fail.bpl.expect | 2 + 12 files changed, 203 insertions(+), 228 deletions(-) create mode 100644 Test/civl/regression-tests/anonymous-action-fail.bpl create mode 100644 Test/civl/regression-tests/anonymous-action-fail.bpl.expect diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index b7669f65e..c5a2c181b 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -17,14 +17,9 @@ public LinearRewriter(CivlTypeChecker civlTypeChecker) this.civlTypeChecker = civlTypeChecker; } - public static bool IsPrimitive(DeclWithFormals decl) - { - return CivlPrimitives.LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name); - } - public static void Rewrite(CivlTypeChecker civlTypeChecker, Implementation impl) { - if (IsPrimitive(impl)) { + if (CivlPrimitives.IsPrimitive(impl)) { return; } var linearRewriter = new LinearRewriter(civlTypeChecker); @@ -38,7 +33,7 @@ private List RewriteCmdSeq(List cmdSeq) { if (cmd is CallCmd callCmd) { - if (IsPrimitive(callCmd.Proc)) + if (CivlPrimitives.IsPrimitive(callCmd.Proc)) { newCmdSeq.AddRange(RewriteCallCmd(callCmd)); } diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 883bf4e71..ec49ab946 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -191,7 +191,7 @@ private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) } else if (cmd is CallCmd callCmd) { - var isPrimitive = LinearRewriter.IsPrimitive(callCmd.Proc); + var isPrimitive = CivlPrimitives.IsPrimitive(callCmd.Proc); if (!isPrimitive) { linearGlobalVariables.Except(start).ForEach(g => @@ -338,7 +338,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) public override Implementation VisitImplementation(Implementation node) { - if (LinearRewriter.IsPrimitive(node)) + if (CivlPrimitives.IsPrimitive(node)) { return node; } @@ -538,7 +538,7 @@ public override Cmd VisitUnpackCmd(UnpackCmd node) public override Cmd VisitCallCmd(CallCmd node) { - var isPrimitive = LinearRewriter.IsPrimitive(node.Proc); + var isPrimitive = CivlPrimitives.IsPrimitive(node.Proc); var inVars = new HashSet(); var globalInVars = new HashSet(); for (int i = 0; i < node.Proc.InParams.Count; i++) @@ -752,7 +752,7 @@ enclosingProc is not YieldProcedureDecl && public override Cmd VisitParCallCmd(ParCallCmd node) { - if (node.CallCmds.Any(callCmd => LinearRewriter.IsPrimitive(callCmd.Proc))) + if (node.CallCmds.Any(callCmd => CivlPrimitives.IsPrimitive(callCmd.Proc))) { Error(node, "linear primitives may not be invoked in a parallel call"); return node; @@ -831,7 +831,7 @@ private bool InvalidAssignmentWithKeyCollection(Variable target, Variable source private void CheckLinearStoreAccessInGuards() { program.Implementations.ForEach(impl => { - if (LinearRewriter.IsPrimitive(impl)) + if (CivlPrimitives.IsPrimitive(impl)) { return; } diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index 00179df17..182c494db 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -259,7 +259,7 @@ private void ProcessCallCmd(CallCmd newCall) InjectGate(pureAction, newCall); newCmdSeq.Add(newCall); } - else if (LinearRewriter.IsPrimitive(newCall.Proc)) + else if (CivlPrimitives.IsPrimitive(newCall.Proc)) { newCmdSeq.AddRange(linearRewriter.RewriteCallCmd(newCall)); } diff --git a/Source/Core/Analysis/ModSetCollector.cs b/Source/Core/Analysis/ModSetCollector.cs index f7e0f0a4f..c1939d9c1 100644 --- a/Source/Core/Analysis/ModSetCollector.cs +++ b/Source/Core/Analysis/ModSetCollector.cs @@ -194,6 +194,15 @@ public override Cmd VisitCallCmd(CallCmd callCmd) } } + if (CivlPrimitives.IsPrimitive(callCmd.Proc)) + { + var modifiedArgument = CivlPrimitives.ModifiedArgument(callCmd)?.Decl; + if (modifiedArgument != null) + { + ProcessVariable(modifiedArgument); + } + } + return ret; } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 348ac2580..7cabd38ce 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -759,17 +759,19 @@ SpecRefinedActionForAtomicAction SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List ins, List outs.> = - (. IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; .) + (. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; .) "refines" { Attribute } ( MoverQualifier "action" (. tok = t; .) { Attribute } - Ident + Ident ImplBody (. - if (refinedAction == null) { + if (m.val != "_") { + this.SemErr("expected _ for name of anoonymous action"); + } else if (refinedAction == null) { var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), false, new List(), null, null, new List(), new List(), new List(), new List(), null, akv); diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 3e3ff4bc5..425d70be4 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -223,6 +223,11 @@ public static class CivlPrimitives "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" }; + public static bool IsPrimitive(DeclWithFormals decl) + { + return LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name); + } + public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr) { if (expr is IdentifierExpr identifierExpr) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 703fa7b8b..e048776fe 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1219,7 +1219,7 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) { } void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List ins, List outs) { - IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; + IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; Expect(41); while (la.kind == 26) { Attribute(ref kv); @@ -1231,9 +1231,11 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken while (la.kind == 26) { Attribute(ref akv); } - Ident(out unused); + Ident(out m); ImplBody(out locals, out stmtList); - if (refinedAction == null) { + if (m.val != "_") { + this.SemErr("expected _ for name of anoonymous action"); + } else if (refinedAction == null) { var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), false, new List(), null, null, new List(), new List(), new List(), new List(), null, akv); diff --git a/Test/civl/large-samples/shared-vector.bpl b/Test/civl/large-samples/shared-vector.bpl index 08e859471..aae697472 100644 --- a/Test/civl/large-samples/shared-vector.bpl +++ b/Test/civl/large-samples/shared-vector.bpl @@ -4,7 +4,7 @@ //////////////////////////////////////////////////////////////////////////////// // Shared integer array implementation -var {:layer 9, 100} IntArrayPool: Map Loc (Vec int); +var {:layer 2, 3} IntArrayPool: Map Loc (Vec int); datatype IntArray { IntArray( @@ -13,12 +13,12 @@ datatype IntArray { ) } -var {:layer 0, 9} {:linear} IntArrayPoolLow: Map Loc IntArray; +var {:layer 0, 2} {:linear} IntArrayPoolLow: Map Loc IntArray; -yield invariant {:layer 9} IntArrayDom(); +yield invariant {:layer 2} IntArrayDom(); invariant IntArrayPool->dom == IntArrayPoolLow->dom; -yield invariant {:layer 9} Yield(loc_iv: Loc); +yield invariant {:layer 2} Yield(loc_iv: Loc); invariant Map_Contains(IntArrayPoolLow, loc_iv); invariant (var intvec_low, intvec_high := Map_At(IntArrayPoolLow, loc_iv), Map_At(IntArrayPool, loc_iv); @@ -27,8 +27,7 @@ invariant (forall j: int:: 0 <= j && j < Vec_Len(intvec_high) ==> Map_Contains(MutexPool, Map_At(intvec_low->mutexes, j)->val)) && (forall j: int:: 0 <= j && j < Vec_Len(intvec_high) ==> Map_At(intvec_low->values, j)->val == Vec_Nth(intvec_high, j))); - -atomic action {:layer 10, 100} Atomic_IntArray_Alloc(v: Vec int) returns (loc_iv: Loc) +atomic action {:layer 3} Atomic_IntArray_Alloc(v: Vec int) returns (loc_iv: Loc) modifies IntArrayPool; { var {:linear} one_loc_iv: One Loc; @@ -37,7 +36,7 @@ modifies IntArrayPool; assume !Map_Contains(IntArrayPool, loc_iv); IntArrayPool := Map_Update(IntArrayPool, loc_iv, v); } -yield procedure {:layer 9} IntArray_Alloc(v: Vec int) returns (loc_iv: Loc) +yield procedure {:layer 2} IntArray_Alloc(v: Vec int) returns (loc_iv: Loc) refines Atomic_IntArray_Alloc; preserves call IntArrayDom(); { @@ -49,20 +48,20 @@ preserves call IntArrayDom(); var i: int; var {:linear} one_loc_i: One Loc; var {:linear} one_loc_iv: One Loc; - var {:layer 9} OldMutexPool: Map Loc Mutex; + var {:layer 2} OldMutexPool: Map Loc Mutex; call mutexes := Map_MakeEmpty(); call values := Map_MakeEmpty(); - call {:layer 9} OldMutexPool := Copy(MutexPool); + call {:layer 2} OldMutexPool := Copy(MutexPool); i := 0; while (i < Vec_Len(v)) - invariant {:layer 9} 0 <= i; - invariant {:layer 9} mutexes->dom == values->dom; - invariant {:layer 9} mutexes->dom->val == (lambda j: int :: 0 <= j && j < i); - invariant {:layer 9} (forall j: int:: 0 <= j && j < i ==> Map_Contains(MutexPool, Map_At(mutexes, j)->val)); - invariant {:layer 9} (forall j: int:: 0 <= j && j < i ==> Map_At(values, j)->val == Vec_Nth(v, j)); - invariant {:layer 9} Set_IsSubset(OldMutexPool->dom, MutexPool->dom); + invariant {:layer 2} 0 <= i; + invariant {:layer 2} mutexes->dom == values->dom; + invariant {:layer 2} mutexes->dom->val == (lambda j: int :: 0 <= j && j < i); + invariant {:layer 2} (forall j: int:: 0 <= j && j < i ==> Map_Contains(MutexPool, Map_At(mutexes, j)->val)); + invariant {:layer 2} (forall j: int:: 0 <= j && j < i ==> Map_At(values, j)->val == Vec_Nth(v, j)); + invariant {:layer 2} Set_IsSubset(OldMutexPool->dom, MutexPool->dom); { call one_loc_mutex := Mutex_Alloc(); call Map_PutValue(mutexes, i, one_loc_mutex); @@ -76,10 +75,10 @@ preserves call IntArrayDom(); call one_loc_iv := Loc_New(); loc_iv := one_loc_iv->val; call AddIntArrayToPool(one_loc_iv, intvec); - call {:layer 9} IntArrayPool := Copy(Map_Update(IntArrayPool, one_loc_iv->val, v)); + call {:layer 2} IntArrayPool := Copy(Map_Update(IntArrayPool, one_loc_iv->val, v)); } -atomic action {:layer 10, 100} Atomic_IntArray_Read({:linear} tid: One Tid, loc_iv: Loc, i: int) returns (v: int) +atomic action {:layer 3} Atomic_IntArray_Read({:linear} tid: One Tid, loc_iv: Loc, i: int) returns (v: int) { var vec: Vec int; assert Map_Contains(IntArrayPool, loc_iv); @@ -87,7 +86,7 @@ atomic action {:layer 10, 100} Atomic_IntArray_Read({:linear} tid: One Tid, loc_ assert Vec_Contains(vec, i); v := Vec_Nth(vec, i); } -yield procedure {:layer 9} IntArray_Read({:linear} tid: One Tid, loc_iv: Loc, i: int) returns (v: int) +yield procedure {:layer 2} IntArray_Read({:linear} tid: One Tid, loc_iv: Loc, i: int) returns (v: int) refines Atomic_IntArray_Read; preserves call IntArrayDom(); preserves call Yield(loc_iv); @@ -105,7 +104,7 @@ preserves call Yield(loc_iv); call Mutex_Release(tid, loc_mutex); } -atomic action {:layer 10, 100} Atomic_IntArray_Write({:linear} tid: One Tid, loc_iv: Loc, i: int, v: int) +atomic action {:layer 3} Atomic_IntArray_Write({:linear} tid: One Tid, loc_iv: Loc, i: int, v: int) modifies IntArrayPool; { var vec: Vec int; @@ -115,7 +114,7 @@ modifies IntArrayPool; vec := Vec_Update(vec, i, v); IntArrayPool := Map_Update(IntArrayPool, loc_iv, vec); } -yield procedure {:layer 9} IntArray_Write({:linear} tid: One Tid, loc_iv: Loc, i: int, v: int) +yield procedure {:layer 2} IntArray_Write({:linear} tid: One Tid, loc_iv: Loc, i: int, v: int) refines Atomic_IntArray_Write; preserves call IntArrayDom(); preserves call Yield(loc_iv); @@ -132,10 +131,10 @@ preserves call Yield(loc_iv); cell_int := Cell(one_loc_int, v); call Locked_PutOwnedLocInt(tid, loc_iv, i, cell_int); call Mutex_Release(tid, loc_mutex); - call {:layer 9} IntArrayPool := Copy(Map_Update(IntArrayPool, loc_iv, Vec_Update(Map_At(IntArrayPool, loc_iv), i, v))); + call {:layer 2} IntArrayPool := Copy(Map_Update(IntArrayPool, loc_iv, Vec_Update(Map_At(IntArrayPool, loc_iv), i, v))); } -atomic action {:layer 10, 100} Atomic_IntArray_Swap({:linear} tid: One Tid, loc_iv: Loc, i: int, j: int) +atomic action {:layer 3} Atomic_IntArray_Swap({:linear} tid: One Tid, loc_iv: Loc, i: int, j: int) modifies IntArrayPool; { var vec: Vec int; @@ -145,7 +144,7 @@ modifies IntArrayPool; vec := Vec_Swap(vec, i, j); IntArrayPool := Map_Update(IntArrayPool, loc_iv, vec); } -yield procedure {:layer 9} IntArray_Swap({:linear} tid: One Tid, loc_iv: Loc, i: int, j: int) +yield procedure {:layer 2} IntArray_Swap({:linear} tid: One Tid, loc_iv: Loc, i: int, j: int) refines Atomic_IntArray_Swap; preserves call IntArrayDom(); preserves call Yield(loc_iv); @@ -184,30 +183,10 @@ preserves call Yield(loc_iv); call Locked_PutOwnedLocInt(tid, loc_iv, j, cell_int_i); call Mutex_Release(tid, loc_mutex_j); call Mutex_Release(tid, loc_mutex_i); - call {:layer 9} IntArrayPool := Copy(Map_Update(IntArrayPool, loc_iv, Vec_Swap(Map_At(IntArrayPool, loc_iv), i, j))); + call {:layer 2} IntArrayPool := Copy(Map_Update(IntArrayPool, loc_iv, Vec_Swap(Map_At(IntArrayPool, loc_iv), i, j))); } -right action {:layer 1, 9} Atomic_GetLocMutex(loc_iv: Loc, i: int) returns (loc_mutex: Loc) -modifies IntArrayPoolLow; -{ - var {:linear} one_loc_iv: One Loc; - var {:linear} intvec: IntArray; - var {:linear "no_collect_keys"} mutexes: Map int (One Loc); - var {:linear "no_collect_keys"} values: Map int (Cell Loc int); - var {:linear} one_loc_mutex: One Loc; - - call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); - IntArray(mutexes, values) := intvec; - call one_loc_mutex := Map_GetValue(mutexes, i); - loc_mutex := one_loc_mutex->val; - call Map_PutValue(mutexes, i, one_loc_mutex); - intvec := IntArray(mutexes, values); - call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); -} -yield procedure {:layer 0} GetLocMutex(loc_iv: Loc, i: int) returns (loc_mutex: Loc); -refines Atomic_GetLocMutex; - -both action {:layer 2, 9} Atomic_Locked_GetOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int) +both action {:layer 2} Atomic_Locked_GetOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int) modifies IntArrayPoolLow; { var {:linear} one_loc_iv: One Loc; @@ -232,7 +211,7 @@ refines Atomic_Locked_GetOwnedLocInt; call cell_int := GetOwnedLocInt(loc_iv, i); } -both action {:layer 2, 9} Atomic_Locked_PutOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int) +both action {:layer 2} Atomic_Locked_PutOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int) modifies IntArrayPoolLow; { var {:linear} one_loc_iv: One Loc; @@ -257,25 +236,41 @@ refines Atomic_Locked_PutOwnedLocInt; call PutOwnedLocInt(loc_iv, i, cell_int); } -atomic action {:layer 1, 1} Atomic_GetOwnedLocInt(loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int) -modifies IntArrayPoolLow; +yield procedure {:layer 0} GetLocMutex(loc_iv: Loc, i: int) returns (loc_mutex: Loc); +refines right action {:layer 1, 2} _ { var {:linear} one_loc_iv: One Loc; var {:linear} intvec: IntArray; var {:linear "no_collect_keys"} mutexes: Map int (One Loc); var {:linear "no_collect_keys"} values: Map int (Cell Loc int); + var {:linear} one_loc_mutex: One Loc; call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); IntArray(mutexes, values) := intvec; - call cell_int := Map_GetValue(values, i); + call one_loc_mutex := Map_GetValue(mutexes, i); + loc_mutex := one_loc_mutex->val; + call Map_PutValue(mutexes, i, one_loc_mutex); intvec := IntArray(mutexes, values); call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); } + yield procedure {:layer 0} GetOwnedLocInt(loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int); -refines Atomic_GetOwnedLocInt; +refines atomic action {:layer 1, 1} _ +{ + var {:linear} one_loc_iv: One Loc; + var {:linear} intvec: IntArray; + var {:linear "no_collect_keys"} mutexes: Map int (One Loc); + var {:linear "no_collect_keys"} values: Map int (Cell Loc int); -atomic action {:layer 1, 1} Atomic_PutOwnedLocInt(loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int) -modifies IntArrayPoolLow; + call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); + IntArray(mutexes, values) := intvec; + call cell_int := Map_GetValue(values, i); + intvec := IntArray(mutexes, values); + call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); +} + +yield procedure {:layer 0} PutOwnedLocInt(loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int); +refines atomic action {:layer 1, 1} _ { var {:linear} one_loc_iv: One Loc; var {:linear} intvec: IntArray; @@ -288,25 +283,19 @@ modifies IntArrayPoolLow; intvec := IntArray(mutexes, values); call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); } -yield procedure {:layer 0} PutOwnedLocInt(loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int); -refines Atomic_PutOwnedLocInt; -atomic action {:layer 1, 9} Atomic_AddIntArrayToPool({:linear_in} one_loc_iv: One Loc, {:linear_in} intvec: IntArray) -modifies IntArrayPoolLow; +yield procedure {:layer 0} AddIntArrayToPool({:linear_in} one_loc_iv: One Loc, {:linear_in} intvec: IntArray); +refines atomic action {:layer 1, 2} _ { call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); } -yield procedure {:layer 0} AddIntArrayToPool({:linear_in} one_loc_iv: One Loc, {:linear_in} intvec: IntArray); -refines Atomic_AddIntArrayToPool; -//////////////////////////////////////////////////////////////////////////////// -// Low-level primitives for shared mutexes type Tid; type Mutex = Option Tid; -var {:layer 0, 9} MutexPool: Map Loc Mutex; +var {:layer 0, 2} MutexPool: Map Loc Mutex; yield procedure {:layer 0} Mutex_Alloc() returns ({:linear} one_loc_l: One Loc); -refines right action {:layer 1, 9} _ +refines right action {:layer 1, 2} _ { call one_loc_l := Loc_New(); assume !Map_Contains(MutexPool, one_loc_l->val); @@ -314,7 +303,7 @@ refines right action {:layer 1, 9} _ } yield procedure {:layer 0} Mutex_Acquire({:linear} tid: One Tid, loc_l: Loc); -refines right action {:layer 1, 9} _ +refines right action {:layer 1, 2} _ { assert Map_Contains(MutexPool, loc_l); assume Map_At(MutexPool, loc_l) == None(); @@ -322,7 +311,7 @@ refines right action {:layer 1, 9} _ } yield procedure {:layer 0} Mutex_Release({:linear} tid: One Tid, loc_l: Loc); -refines left action {:layer 1, 9} _ +refines left action {:layer 1, 2} _ { assert Map_Contains(MutexPool, loc_l); assert Map_At(MutexPool, loc_l) == Some(tid->val); diff --git a/Test/civl/large-samples/treiber-stack.bpl b/Test/civl/large-samples/treiber-stack.bpl index 44008baa2..5c67d70ae 100644 --- a/Test/civl/large-samples/treiber-stack.bpl +++ b/Test/civl/large-samples/treiber-stack.bpl @@ -9,67 +9,64 @@ function {:inline} AllLocPieces(): Set LocPiece { type LocTreiberNode = KeyedLoc LocPiece; type StackElem T = Node LocTreiberNode T; type StackMap T = Map LocTreiberNode (StackElem T); -datatype Treiber { Treiber(top: Option LocTreiberNode, {:linear} stack: StackMap T) } +datatype Treiber { Treiber(top: Option LocTreiberNode, {:linear} nodes: StackMap T) } type X; // module type parameter -var {:layer 4, 5} Stack: Map Loc (Vec X); -var {:layer 0, 4} {:linear} ts: Map Loc (Treiber X); +var {:layer 4, 5} TreiberPool: Map Loc (Vec X); +var {:layer 0, 4} {:linear} TreiberPoolLow: Map Loc (Treiber X); /// Yield invariants function {:inline} Domain(ts: Map Loc (Treiber X), loc_t: Loc): Set LocTreiberNode { - ts->val[loc_t]->stack->dom + ts->val[loc_t]->nodes->dom } yield invariant {:layer 1} Yield(); yield invariant {:layer 2} TopInStack(loc_t: Loc); -invariant Map_Contains(ts, loc_t); -invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); -invariant (forall loc_n: LocTreiberNode :: Set_Contains(Domain(ts, loc_t), loc_n) ==> - (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); +invariant Map_Contains(TreiberPoolLow, loc_t); +invariant (var loc_n := Map_At(TreiberPoolLow, loc_t)->top; loc_n is None || Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n->t)); +invariant (forall loc_n: LocTreiberNode :: Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n) ==> + (var loc_n' := Map_At(Map_At(TreiberPoolLow, loc_t)->nodes, loc_n)->next; loc_n' is None || Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n'->t))); yield invariant {:layer 2} LocInStackOrNone(loc_t: Loc, loc_n: Option LocTreiberNode); -invariant Map_Contains(ts, loc_t); -invariant loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); +invariant Map_Contains(TreiberPoolLow, loc_t); +invariant loc_n is None || Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n->t); yield invariant {:layer 3} LocInStack(loc_t: Loc, loc_n: LocTreiberNode); -invariant Map_Contains(ts, loc_t); -invariant Set_Contains(Domain(ts, loc_t), loc_n); +invariant Map_Contains(TreiberPoolLow, loc_t); +invariant Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n); yield invariant {:layer 4} ReachInStack(loc_t: Loc); -invariant Map_Contains(ts, loc_t); -invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None())); -invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val)); -invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); -invariant (forall {:pool "A"} loc_n: LocTreiberNode :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==> - loc_n == KeyedLoc(loc_n->l, Left()) && - (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); -invariant Map_At(Stack, loc_t) == Abs(Map_At(ts, loc_t)); +invariant Map_Contains(TreiberPoolLow, loc_t); +invariant (var t := TreiberPoolLow->val[loc_t]; Between(t->nodes->val, t->top, t->top, None())); +invariant (var t := TreiberPoolLow->val[loc_t]; IsSubset(BetweenSet(t->nodes->val, t->top, None()), Domain(TreiberPoolLow, loc_t)->val)); +invariant (var loc_n := Map_At(TreiberPoolLow, loc_t)->top; loc_n is None || Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n->t)); +invariant (forall {:pool "A"} loc_n: LocTreiberNode :: {:add_to_pool "A", loc_n} Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n) ==> loc_n == KeyedLoc(loc_n->l, Left())); +invariant Map_At(TreiberPool, loc_t) == Abs(Map_At(TreiberPoolLow, loc_t)); yield invariant {:layer 4} StackDom(); -invariant Stack->dom == ts->dom; +invariant TreiberPool->dom == TreiberPoolLow->dom; -yield invariant {:layer 4} PushLocInStack( - loc_t: Loc, node: StackElem X, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode); -invariant Map_Contains(ts, loc_t); -invariant Set_Contains(Domain(ts, loc_t), new_loc_n); -invariant right_loc_piece->val == KeyedLoc(new_loc_n->l, Right()); +yield invariant {:layer 4} PushLocInStack(loc_t: Loc, node: StackElem X, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode); +invariant Map_Contains(TreiberPoolLow, loc_t); +invariant Set_Contains(Domain(TreiberPoolLow, loc_t), new_loc_n); invariant new_loc_n == KeyedLoc(new_loc_n->l, Left()); -invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !BetweenSet(t->stack->val, t->top, None())[new_loc_n]); +invariant right_loc_piece->val == KeyedLoc(new_loc_n->l, Right()); +invariant (var t := TreiberPoolLow->val[loc_t]; Map_At(t->nodes, new_loc_n) == node && !BetweenSet(t->nodes->val, t->top, None())[new_loc_n]); /// Layered implementation atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc) -modifies Stack; +modifies TreiberPool; { var {:linear} one_loc_t: One Loc; call one_loc_t := Loc_New(); loc_t := one_loc_t->val; - assume !Map_Contains(Stack, loc_t); - Stack := Map_Update(Stack, loc_t, Vec_Empty()); + assume !Map_Contains(TreiberPool, loc_t); + TreiberPool := Map_Update(TreiberPool, loc_t, Vec_Empty()); } yield procedure {:layer 4} Alloc() returns (loc_t: Loc) refines AtomicAlloc; @@ -86,15 +83,15 @@ preserves call StackDom(); call one_loc_t := Loc_New(); loc_t := one_loc_t->val; call AllocTreiber#0(one_loc_t, treiber); - call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty())); + call {:layer 4} TreiberPool := Copy(Map_Update(TreiberPool, loc_t, Vec_Empty())); call {:layer 4} AbsLemma(treiber); } atomic action {:layer 5} AtomicPush(loc_t: Loc, x: X) returns (success: bool) -modifies Stack; +modifies TreiberPool; { if (*) { - Stack := Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x)); + TreiberPool := Map_Update(TreiberPool, loc_t, Vec_Append(Map_At(TreiberPool, loc_t), x)); success := true; } else { success := false; @@ -111,28 +108,28 @@ preserves call StackDom(); var {:linear} right_loc_piece: One LocTreiberNode; var {:layer 4} old_treiber: Treiber X; - call {:layer 4} old_treiber := Copy(ts->val[loc_t]); + call {:layer 4} old_treiber := Copy(TreiberPoolLow->val[loc_t]); call loc_n, new_loc_n, right_loc_piece := AllocNode#3(loc_t, x); - call {:layer 4} FrameLemma(old_treiber, ts->val[loc_t]); + call {:layer 4} FrameLemma(old_treiber, TreiberPoolLow->val[loc_t]); par ReachInStack(loc_t) | StackDom() | PushLocInStack(loc_t, Node(loc_n, x), new_loc_n, right_loc_piece); call success := WriteTopOfStack#0(loc_t, loc_n, Some(new_loc_n)); if (success) { - call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x))); - assert {:layer 4} ts->val[loc_t]->top != None(); - call {:layer 4} AbsLemma(ts->val[loc_t]); + call {:layer 4} TreiberPool := Copy(Map_Update(TreiberPool, loc_t, Vec_Append(Map_At(TreiberPool, loc_t), x))); + assert {:layer 4} TreiberPoolLow->val[loc_t]->top != None(); + call {:layer 4} AbsLemma(TreiberPoolLow->val[loc_t]); } } atomic action {:layer 5} AtomicPop(loc_t: Loc) returns (success: bool, x_opt: Option X) -modifies Stack; +modifies TreiberPool; { var stack: Vec X; if (*) { - stack := Map_At(Stack, loc_t); + stack := Map_At(TreiberPool, loc_t); if (Vec_Len(stack) > 0) { x_opt := Some(Vec_Nth(stack, Vec_Len(stack) - 1)); - Stack := Map_Update(Stack, loc_t, Vec_Remove(stack)); + TreiberPool := Map_Update(TreiberPool, loc_t, Vec_Remove(stack)); } else { x_opt := None(); } @@ -148,18 +145,18 @@ preserves call TopInStack(loc_t); preserves call ReachInStack(loc_t); preserves call StackDom(); { - call {:layer 4} AbsLemma(ts->val[loc_t]); + call {:layer 4} AbsLemma(TreiberPoolLow->val[loc_t]); call success, x_opt := PopIntermediate(loc_t); if (x_opt is Some) { - assert {:layer 4} Vec_Len(Map_At(Stack, loc_t)) > 0; - call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Remove(Map_At(Stack, loc_t)))); + assert {:layer 4} Vec_Len(Map_At(TreiberPool, loc_t)) > 0; + call {:layer 4} TreiberPool := Copy(Map_Update(TreiberPool, loc_t, Vec_Remove(Map_At(TreiberPool, loc_t)))); } } atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc, x: X) returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode) -modifies ts; -asserts Map_Contains(ts, loc_t); +modifies TreiberPoolLow; +asserts Map_Contains(TreiberPoolLow, loc_t); { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; @@ -169,7 +166,7 @@ asserts Map_Contains(ts, loc_t); var {:linear} loc_pieces: Set LocTreiberNode; var {:linear} left_loc_piece: One LocTreiberNode; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call one_loc_t, treiber := Map_Get(TreiberPoolLow, loc_t); Treiber(top, stack) := treiber; assume loc_n is None || Map_Contains(stack, loc_n->t); call loc, loc_pieces := KeyedLocSet_New(AllLocPieces()); @@ -178,7 +175,7 @@ asserts Map_Contains(ts, loc_t); call right_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Right())); call Map_Put(stack, left_loc_piece, Node(loc_n, x)); treiber := Treiber(top, stack); - call Map_Put(ts, one_loc_t, treiber); + call Map_Put(TreiberPoolLow, one_loc_t, treiber); } yield procedure {:layer 3} AllocNode#3(loc_t: Loc, x: X) returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode) @@ -199,7 +196,7 @@ refines AtomicAllocNode#3; } atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc) returns (success: bool, x_opt: Option X) -modifies ts; +modifies TreiberPoolLow; { var {:linear} one_loc_t: One Loc; var loc_n: Option LocTreiberNode; @@ -208,19 +205,19 @@ modifies ts; var {:linear} stack: StackMap X; var x: X; - assert Map_Contains(ts, loc_t); + assert Map_Contains(TreiberPoolLow, loc_t); if (*) { - call one_loc_t, treiber := Map_Get(ts, loc_t); + call one_loc_t, treiber := Map_Get(TreiberPoolLow, loc_t); Treiber(top, stack) := treiber; assume top is Some && Map_Contains(stack, top->t); Node(loc_n, x) := Map_At(stack, top->t); treiber := Treiber(loc_n, stack); - call Map_Put(ts, one_loc_t, treiber); + call Map_Put(TreiberPoolLow, one_loc_t, treiber); x_opt := Some(x); success := true; } else if (*) { - assume Map_At(ts, loc_t)->top is None; + assume Map_At(TreiberPoolLow, loc_t)->top is None; x_opt := None(); success := true; } else { @@ -256,8 +253,8 @@ preserves call TopInStack(loc_t); right action {:layer 3} AtomicReadTopOfStack#Push(loc_t: Loc) returns (loc_n: Option LocTreiberNode) { - assert Map_Contains(ts, loc_t); - assume loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); + assert Map_Contains(TreiberPoolLow, loc_t); + assume loc_n is None || Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n->t); } yield procedure {:layer 2} ReadTopOfStack#Push(loc_t: Loc) returns (loc_n: Option LocTreiberNode) preserves call TopInStack(loc_t); @@ -269,8 +266,8 @@ refines AtomicReadTopOfStack#Push; atomic action {:layer 3} AtomicReadTopOfStack#Pop(loc_t: Loc) returns (loc_n: Option LocTreiberNode) { - assert Map_Contains(ts, loc_t); - assume if loc_n is None then Map_At(ts, loc_t)->top is None else Set_Contains(Domain(ts, loc_t), loc_n->t); + assert Map_Contains(TreiberPoolLow, loc_t); + assume if loc_n is None then Map_At(TreiberPoolLow, loc_t)->top is None else Set_Contains(Domain(TreiberPoolLow, loc_t), loc_n->t); } yield procedure {:layer 2} ReadTopOfStack#Pop(loc_t: Loc) returns (loc_n: Option LocTreiberNode) preserves call TopInStack(loc_t); @@ -282,15 +279,15 @@ refines AtomicReadTopOfStack#Pop; right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc, loc_n: LocTreiberNode) returns (node: StackElem X) { - assert Map_Contains(ts, loc_t); - assert Map_Contains(Map_At(ts, loc_t)->stack, loc_n); - node := Map_At(Map_At(ts, loc_t)->stack, loc_n); + assert Map_Contains(TreiberPoolLow, loc_t); + assert Map_Contains(Map_At(TreiberPoolLow, loc_t)->nodes, loc_n); + node := Map_At(Map_At(TreiberPoolLow, loc_t)->nodes, loc_n); } /// Primitives atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) returns (node: StackElem X) -modifies ts; +modifies TreiberPoolLow; refines AtomicLoadNode#1; { var {:linear} one_loc_t: One Loc; @@ -299,69 +296,60 @@ refines AtomicLoadNode#1; var {:linear} stack: StackMap X; var {:linear} one_loc_n: One LocTreiberNode; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call one_loc_t, treiber := Map_Get(TreiberPoolLow, loc_t); Treiber(top, stack) := treiber; call one_loc_n, node := Map_Get(stack, loc_n); call Map_Put(stack, one_loc_n, node); treiber := Treiber(top, stack); - call Map_Put(ts, one_loc_t, treiber); + call Map_Put(TreiberPoolLow, one_loc_t, treiber); } yield procedure {:layer 0} LoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) returns (node: StackElem X); refines AtomicLoadNode#0; -atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode) -modifies ts; +yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode); +refines atomic action {:layer 1,2} _ { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call one_loc_t, treiber := Map_Get(TreiberPoolLow, loc_t); loc_n := treiber->top; - call Map_Put(ts, one_loc_t, treiber); + call Map_Put(TreiberPoolLow, one_loc_t, treiber); } -yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode); -refines AtomicReadTopOfStack#0; -atomic action {:layer 1,4} AtomicWriteTopOfStack#0( - loc_t: Loc, old_loc_n: Option LocTreiberNode, new_loc_n: Option LocTreiberNode) returns (success: bool) -modifies ts; +yield procedure {:layer 0} WriteTopOfStack#0( + loc_t: Loc, old_loc_n: Option LocTreiberNode, new_loc_n: Option LocTreiberNode) returns (success: bool); +refines atomic action {:layer 1,4} _ { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call one_loc_t, treiber := Map_Get(TreiberPoolLow, loc_t); if (old_loc_n == treiber->top) { treiber->top := new_loc_n; success := true; } else { success := false; } - call Map_Put(ts, one_loc_t, treiber); + call Map_Put(TreiberPoolLow, one_loc_t, treiber); } -yield procedure {:layer 0} WriteTopOfStack#0( - loc_t: Loc, old_loc_n: Option LocTreiberNode, new_loc_n: Option LocTreiberNode) returns (success: bool); -refines AtomicWriteTopOfStack#0; -atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X) -modifies ts; +yield procedure {:layer 0} AllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X); +refines atomic action {:layer 1,3} _ { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call one_loc_t, treiber := Map_Get(ts, loc_t); - call Map_Put(treiber->stack, loc_piece, node); - call Map_Put(ts, one_loc_t, treiber); + call one_loc_t, treiber := Map_Get(TreiberPoolLow, loc_t); + call Map_Put(treiber->nodes, loc_piece, node); + call Map_Put(TreiberPoolLow, one_loc_t, treiber); } -yield procedure {:layer 0} AllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X); -refines AtomicAllocNode#0; -atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X) -modifies ts; +yield procedure {:layer 0} AllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X); +refines atomic action {:layer 1,4} _ { - call Map_Put(ts, one_loc_t, treiber); + call Map_Put(TreiberPoolLow, one_loc_t, treiber); } -yield procedure {:layer 0} AllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X); -refines AtomicAllocTreiber#0; /// Proof of abstraction with a manual encoding of termination @@ -370,18 +358,18 @@ function Abs(treiber: Treiber X): Vec X; function {:inline} AbsDefinition(treiber: Treiber X): Vec X { if treiber->top == None() then Vec_Empty() else - (var n := Map_At(treiber->stack, treiber->top->t); - (var treiber' := Treiber(n->next, treiber->stack); + (var n := Map_At(treiber->nodes, treiber->top->t); + (var treiber' := Treiber(n->next, treiber->nodes); Vec_Append(Abs(treiber'), n->val))) } pure procedure AbsCompute(treiber: Treiber X, treiber': Treiber X) returns (absStack: Vec X) requires treiber->top == treiber'->top; -requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val); -requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == - MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); -requires Between(treiber->stack->val, treiber->top, treiber->top, None()); -requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); +requires IsSubset(treiber->nodes->dom->val, treiber'->nodes->dom->val); +requires MapIte(treiber->nodes->dom->val, treiber->nodes->val, MapConst(Default())) == + MapIte(treiber->nodes->dom->val, treiber'->nodes->val, MapConst(Default())); +requires Between(treiber->nodes->val, treiber->top, treiber->top, None()); +requires IsSubset(BetweenSet(treiber->nodes->val, treiber->top, None()), treiber->nodes->dom->val); ensures absStack == AbsDefinition(treiber); ensures absStack == AbsDefinition(treiber'); free ensures absStack == Abs(treiber); @@ -394,12 +382,12 @@ free ensures absStack == Abs(treiber'); absStack := Vec_Empty(); } else { loc_n := treiber->top; - assert Map_Contains(treiber->stack, loc_n->t); - n := Map_At(treiber->stack, loc_n->t); + assert Map_Contains(treiber->nodes, loc_n->t); + n := Map_At(treiber->nodes, loc_n->t); // Use well-founded list reachability to prove that recursion will terminate: // treiber@caller->top --> treiber@callee->top --> None() - assert Between(treiber->stack->val, loc_n, n->next, None()); - call absStack := AbsCompute(Treiber(n->next, treiber->stack), Treiber(n->next, treiber'->stack)); + assert Between(treiber->nodes->val, loc_n, n->next, None()); + call absStack := AbsCompute(Treiber(n->next, treiber->nodes), Treiber(n->next, treiber'->nodes)); absStack := Vec_Append(absStack, n->val); } } @@ -407,8 +395,8 @@ free ensures absStack == Abs(treiber'); /// Useful lemmas obtained by wrapping AbsCompute pure procedure AbsLemma(treiber: Treiber X) -requires Between(treiber->stack->val, treiber->top, treiber->top, None()); -requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); +requires Between(treiber->nodes->val, treiber->top, treiber->top, None()); +requires IsSubset(BetweenSet(treiber->nodes->val, treiber->top, None()), treiber->nodes->dom->val); ensures Abs(treiber) == AbsDefinition(treiber); { var absStack: Vec X; @@ -417,11 +405,11 @@ ensures Abs(treiber) == AbsDefinition(treiber); pure procedure FrameLemma(treiber: Treiber X, treiber': Treiber X) requires treiber->top == treiber'->top; -requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val); -requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == - MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); -requires Between(treiber->stack->val, treiber->top, treiber->top, None()); -requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); +requires IsSubset(treiber->nodes->dom->val, treiber'->nodes->dom->val); +requires MapIte(treiber->nodes->dom->val, treiber->nodes->val, MapConst(Default())) == + MapIte(treiber->nodes->dom->val, treiber'->nodes->val, MapConst(Default())); +requires Between(treiber->nodes->val, treiber->top, treiber->top, None()); +requires IsSubset(BetweenSet(treiber->nodes->val, treiber->top, None()), treiber->nodes->dom->val); ensures Abs(treiber) == Abs(treiber'); { var absStack: Vec X; diff --git a/Test/civl/paxos/PaxosImpl.bpl b/Test/civl/paxos/PaxosImpl.bpl index 9e97e1917..81479d4ba 100644 --- a/Test/civl/paxos/PaxosImpl.bpl +++ b/Test/civl/paxos/PaxosImpl.bpl @@ -290,9 +290,8 @@ ensures MaxRound(r, MapOr(ns1, ns2), voteInfo) == //////////////////////////////////////////////////////////////////////////////// -atomic action {:layer 1} A_JoinUpdate(r: Round, n: Node) -returns (join:bool, lastVoteRound: Round, lastVoteValue: Value) -modifies acceptorState; +yield procedure {:layer 0} JoinUpdate(r: Round, n: Node) returns (join:bool, lastVoteRound: Round, lastVoteValue: Value); +refines atomic action {:layer 1} _ { var lastJoinRound: Round; lastJoinRound := acceptorState[n]->lastJoinRound; @@ -306,9 +305,8 @@ modifies acceptorState; } } -atomic action {:layer 1} A_VoteUpdate(r: Round, n: Node, v: Value) -returns (vote:bool) -modifies acceptorState; +yield procedure {:layer 0} VoteUpdate(r: Round, n: Node, v: Value) returns (vote:bool); +refines atomic action {:layer 1} _ { var lastJoinRound: Round; lastJoinRound := acceptorState[n]->lastJoinRound; @@ -320,58 +318,34 @@ modifies acceptorState; } } -yield procedure {:layer 0} JoinUpdate(r: Round, n: Node) returns (join:bool, lastVoteRound: Round, lastVoteValue: Value); -refines A_JoinUpdate; - -yield procedure {:layer 0} VoteUpdate(r: Round, n: Node, v: Value) returns (vote:bool); -refines A_VoteUpdate; - //// Channel send/receive actions -left action {:layer 1} A_SendJoinResponse(round: Round, from: Node, lastVoteRound: Round, lastVoteValue: Value) -modifies joinChannel; +yield procedure {:layer 0} SendJoinResponse(round: Round, from: Node, lastVoteRound: Round, lastVoteValue: Value); +refines left action {:layer 1} _ { joinChannel[round][JoinResponse(from, lastVoteRound, lastVoteValue)] := joinChannel[round][JoinResponse(from, lastVoteRound, lastVoteValue)] + 1; } -right action {:layer 1} A_ReceiveJoinResponse(round: Round) -returns (joinResponse: JoinResponse) -modifies joinChannel; +yield procedure {:layer 0} ReceiveJoinResponse(round: Round) returns (joinResponse: JoinResponse); +refines right action {:layer 1} _ { assume joinChannel[round][joinResponse] > 0; joinChannel[round][joinResponse] := joinChannel[round][joinResponse] - 1; } -left action {:layer 1} A_SendVoteResponse(round: Round, from: Node) -modifies voteChannel; +yield procedure {:layer 0} SendVoteResponse(round: Round, from: Node); +refines left action {:layer 1} _ { voteChannel[round][VoteResponse(from)] := voteChannel[round][VoteResponse(from)] + 1; } -right action {:layer 1} A_ReceiveVoteResponse(round: Round) -returns (voteResponse: VoteResponse) -modifies voteChannel; +yield procedure {:layer 0} ReceiveVoteResponse(round: Round) returns (voteResponse: VoteResponse); +refines right action {:layer 1} _ { assume voteChannel[round][voteResponse] > 0; voteChannel[round][voteResponse] := voteChannel[round][voteResponse] - 1; } -yield procedure {:layer 0} -SendJoinResponse(round: Round, from: Node, lastVoteRound: Round, lastVoteValue: Value); -refines A_SendJoinResponse; - -yield procedure {:layer 0} -ReceiveJoinResponse(round: Round) returns (joinResponse: JoinResponse); -refines A_ReceiveJoinResponse; - -yield procedure {:layer 0} -SendVoteResponse(round: Round, from: Node); -refines A_SendVoteResponse; - -yield procedure {:layer 0} -ReceiveVoteResponse(round: Round) returns (voteResponse: VoteResponse); -refines A_ReceiveVoteResponse; - //// Introduction procedures to make send/receive more abstract pure action SendJoinResponseIntro(joinResponse: JoinResponse, {:linear_in} p: One Permission, {:linear_in} permJoinChannel: JoinResponseChannel) diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl b/Test/civl/regression-tests/anonymous-action-fail.bpl new file mode 100644 index 000000000..3ce5c15b1 --- /dev/null +++ b/Test/civl/regression-tests/anonymous-action-fail.bpl @@ -0,0 +1,9 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var {:layer 0,2} x: int; + +yield procedure {:layer 0} A(i: int) returns (j: int); +refines both action {:layer 1} B { + x := x + 1; +} \ No newline at end of file diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl.expect b/Test/civl/regression-tests/anonymous-action-fail.bpl.expect new file mode 100644 index 000000000..ad2fa5050 --- /dev/null +++ b/Test/civl/regression-tests/anonymous-action-fail.bpl.expect @@ -0,0 +1,2 @@ +anonymous-action-fail.bpl(9,1): error: expected _ for name of anoonymous action +1 parse errors detected in anonymous-action-fail.bpl