From 50a6de91a7a063955ee8a2e738e74a477889dd3c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 4 May 2024 13:31:14 -0700 Subject: [PATCH] first commit --- Source/Concurrency/LinearDomainCollector.cs | 6 ++ Source/Concurrency/LinearRewriter.cs | 33 ++++++--- Source/Concurrency/LinearTypeChecker.cs | 4 +- Source/Core/CivlAttributes.cs | 7 +- Source/Core/base.bpl | 30 +++++--- Test/civl/paxos/PaxosImpl.bpl | 18 +++-- Test/civl/samples/alloc-mem.bpl | 76 ++++++++++----------- Test/civl/samples/alloc-mem.bpl.expect | 2 +- Test/civl/samples/civl-paper.bpl | 12 +++- Test/civl/samples/treiber-stack.bpl | 63 +++++++++-------- 10 files changed, 149 insertions(+), 102 deletions(-) diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs index 47f273660..c81a0c10c 100644 --- a/Source/Concurrency/LinearDomainCollector.cs +++ b/Source/Concurrency/LinearDomainCollector.cs @@ -150,6 +150,12 @@ private void RegisterType(Type type) var collector = program.monomorphizer.InstantiateFunction("Set_Collector", typeParamInstantiationMap); collectors[type][permissionType] = collector; } + else if (typeName == "Cell") + { + var typeParamInstantiationMap = new Dictionary { { "T", actualTypeParams[0] }, { "U", actualTypeParams[1] } }; + var collector = program.monomorphizer.InstantiateFunction("Cell_Collector", typeParamInstantiationMap); + collectors[type][permissionType] = collector; + } else { Debug.Assert(typeName == "One"); diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 038e4b534..daaac2881 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -59,10 +59,10 @@ public List RewriteCallCmd(CallCmd callCmd) switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { case "One_New": + case "Cell_Pack": + case "Cell_Unpack": case "Set_MakeEmpty": case "Map_MakeEmpty": - case "Map_Pack": - case "Map_Unpack": case "Map_Assume": return new List{callCmd}; case "Set_Split": @@ -153,6 +153,14 @@ private Function OneConstructor(Type type) return oneConstructor; } + private Function CellConstructor(Type keyType, Type valType) + { + var actualTypeParams = new List() { keyType, valType }; + var cellTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Cell", actualTypeParams); + var cellConstructor = cellTypeCtorDecl.Constructors[0]; + return cellConstructor; + } + private Function SetConstructor(Type type) { var actualTypeParams = new List() { type }; @@ -161,6 +169,11 @@ private Function SetConstructor(Type type) return setConstructor; } + private static Expr Key(Expr path) + { + return ExprHelper.FieldAccess(path, "key"); + } + private static Expr Val(Expr path) { return ExprHelper.FieldAccess(path, "val"); @@ -299,8 +312,7 @@ private List RewriteMapGet(CallCmd callCmd) var cmdSeq = new List(); var path = callCmd.Ins[0]; var k = callCmd.Ins[1]; - var l = callCmd.Outs[0]; - var v = callCmd.Outs[1]; + var c = callCmd.Outs[0]; var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); var domain = instantiation["K"]; @@ -309,9 +321,9 @@ private List RewriteMapGet(CallCmd callCmd) var mapRemoveFunc = MapRemove(domain, range); var mapAtFunc = MapAt(domain, range); cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(mapContainsFunc, path, k), "Map_Get failed")); - var oneConstructor = OneConstructor(domain); - cmdSeq.Add(CmdHelper.AssignCmd(l.Decl, ExprHelper.FunctionCall(oneConstructor, k))); - cmdSeq.Add(CmdHelper.AssignCmd(v.Decl, ExprHelper.FunctionCall(mapAtFunc, path, k))); + var cellConstructor = CellConstructor(domain, range); + cmdSeq.Add( + CmdHelper.AssignCmd(c.Decl, ExprHelper.FunctionCall(cellConstructor, k, ExprHelper.FunctionCall(mapAtFunc, path, k)))); cmdSeq.Add( CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapRemoveFunc, path, k))); @@ -323,8 +335,7 @@ private List RewriteMapPut(CallCmd callCmd) { var cmdSeq = new List(); var path = callCmd.Ins[0]; - var l = callCmd.Ins[1]; - var v = callCmd.Ins[2]; + var c = callCmd.Ins[1]; var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); var domain = instantiation["K"]; @@ -332,9 +343,9 @@ private List RewriteMapPut(CallCmd callCmd) var mapContainsFunc = MapContains(domain, range); var mapUpdateFunc = MapUpdate(domain, range); var attribute = new QKeyValue(Token.NoToken, "linear", new List(), null); - cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Not(ExprHelper.FunctionCall(mapContainsFunc, path, Val(l))), attribute)); + cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Not(ExprHelper.FunctionCall(mapContainsFunc, path, Key(c))), attribute)); cmdSeq.Add( - CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, Val(l), v))); + CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, Key(c), Val(c)))); ResolveAndTypecheck(options, cmdSeq); return cmdSeq; diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 5573b86b9..efa687775 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -774,7 +774,7 @@ public Type GetPermissionType(Type type) { var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl); var typeName = originalTypeCtorDecl.Name; - if (typeName == "Map" || typeName == "Set" || typeName == "One") + if (typeName == "Map" || typeName == "Set" || typeName == "Cell" | typeName == "One") { var actualTypeParams = program.monomorphizer.GetTypeInstantiation(datatypeTypeCtorDecl); return actualTypeParams[0]; @@ -974,7 +974,7 @@ private void CheckType(Type type) return; } var typeCtorDeclName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name; - if (typeCtorDeclName == "Map") + if (typeCtorDeclName == "Map" || typeCtorDeclName == "Cell") { hasLinearStoreAccess = true; } diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 10462d398..e8d629042 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -181,7 +181,8 @@ public static class CivlPrimitives public static HashSet LinearPrimitives = new() { "One_New", - "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Get", "Map_Put", "Map_Assume", + "Cell_Pack", "Cell_Unpack", + "Map_MakeEmpty", "Map_Split", "Map_Get", "Map_Put", "Map_Assume", "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" }; @@ -206,10 +207,10 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { case "One_New": + case "Cell_Pack": + case "Cell_Unpack": case "Set_MakeEmpty": case "Map_MakeEmpty": - case "Map_Pack": - case "Map_Unpack": case "Map_Assume": return null; default: diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 11adac487..cd0b90dd2 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -287,7 +287,7 @@ function {:inline} Map_Collector(a: Map T U): [T]bool Set_Collector(a->dom) } -/// singleton +/// singleton set datatype One { One(val: T) } function {:inline} One_Collector(a: One T): [T]bool @@ -295,6 +295,14 @@ function {:inline} One_Collector(a: One T): [T]bool MapOne(a->val) } +/// singleton map +datatype Cell { Cell(key: T, val: U) } + +function {:inline} Cell_Collector(a: Cell T U): [T]bool +{ + MapOne(a->key) +} + /// linear primitives pure procedure {:inline 1} Set_MakeEmpty() returns ({:linear} l: Set K) { @@ -307,23 +315,23 @@ pure procedure One_Split({:linear} path: Set K, {:linear_out} l: One K); pure procedure One_Get({:linear} path: Set K, k: K) returns ({:linear} l: One K); pure procedure One_Put({:linear} path: Set K, {:linear_in} l: One K); -pure procedure {:inline 1} Map_MakeEmpty() returns ({:linear} m: Map K V) +pure procedure {:inline 1} Cell_Pack({:linear_in} l: One K, {:linear_in} v: V) returns ({:linear} c: Cell K V) { - m := Map_Empty(); + c := Cell(l->val, v); } -pure procedure {:inline 1} Map_Pack({:linear_in} l: One K, {:linear_in} v: V) returns ({:linear} m: Map K V) +pure procedure {:inline 1} Cell_Unpack({:linear_in} c: Cell K V) returns ({:linear} l: One K, {:linear} v: V) { - m := Map_Singleton(l->val, v); + l := One(c->key); + v := c->val; } -pure procedure {:inline 1} Map_Unpack(k: K, {:linear_in} m: Map K V) returns ({:linear} l: One K, {:linear} v: V) + +pure procedure {:inline 1} Map_MakeEmpty() returns ({:linear} m: Map K V) { - assert Map_Contains(m, k); - l := One(k); - v := Map_At(m, k); + m := Map_Empty(); } pure procedure Map_Split({:linear} path: Map K V, {:linear_out} l: One K) returns ({:linear} v: V); -pure procedure Map_Get({:linear} path: Map K V, k: K) returns ({:linear} l: One K, {:linear} v: V); -pure procedure Map_Put({:linear} path: Map K V, {:linear_in} l: One K, {:linear_in} v: V); +pure procedure Map_Get({:linear} path: Map K V, k: K) returns ({:linear} c: Cell K V); +pure procedure Map_Put({:linear} path: Map K V, {:linear_in} c: Cell K V); pure procedure {:inline 1} Map_Assume({:linear} src: Map K V, {:linear} dst: Map K V) { assume Set_IsDisjoint(src->dom, dst->dom); diff --git a/Test/civl/paxos/PaxosImpl.bpl b/Test/civl/paxos/PaxosImpl.bpl index ad3271766..29c1e27c2 100644 --- a/Test/civl/paxos/PaxosImpl.bpl +++ b/Test/civl/paxos/PaxosImpl.bpl @@ -376,31 +376,37 @@ refines A_ReceiveVoteResponse; pure action SendJoinResponseIntro(joinResponse: JoinResponse, {:linear_in} p: One Permission, {:linear_in} permJoinChannel: JoinResponseChannel) returns ({:linear} permJoinChannel': JoinResponseChannel) { + var {:linear} cell_p: Cell Permission JoinResponse; permJoinChannel' := permJoinChannel; - call Map_Put(permJoinChannel', p, joinResponse); + call cell_p := Cell_Pack(p, joinResponse); + call Map_Put(permJoinChannel', cell_p); } pure action ReceiveJoinResponseIntro(round: Round, joinResponse: JoinResponse, {:linear_in} permJoinChannel: JoinResponseChannel) returns ({:linear} receivedPermission: One Permission, {:linear} permJoinChannel': JoinResponseChannel) { - var x: JoinResponse; + var _x: JoinResponse; permJoinChannel' := permJoinChannel; - call receivedPermission, x := Map_Get(permJoinChannel', JoinPerm(round, joinResponse->from)); + receivedPermission := One(JoinPerm(round, joinResponse->from)); + call _x := Map_Split(permJoinChannel', receivedPermission); } pure action SendVoteResponseIntro(voteResponse: VoteResponse, {:linear_in} p: One Permission, {:linear_in} permVoteChannel: VoteResponseChannel) returns ({:linear} permVoteChannel': VoteResponseChannel) { + var {:linear} cell_p: Cell Permission VoteResponse; permVoteChannel' := permVoteChannel; - call Map_Put(permVoteChannel', p, voteResponse); + call cell_p := Cell_Pack(p, voteResponse); + call Map_Put(permVoteChannel', cell_p); } pure action ReceiveVoteResponseIntro(round: Round, voteResponse: VoteResponse, {:linear_in} permVoteChannel: VoteResponseChannel) returns ({:linear} receivedPermission: One Permission, {:linear} permVoteChannel': VoteResponseChannel) { - var x: VoteResponse; + var _x: VoteResponse; permVoteChannel' := permVoteChannel; - call receivedPermission, x := Map_Get(permVoteChannel', VotePerm(round, voteResponse->from)); + receivedPermission := One(VotePerm(round, voteResponse->from)); + call _x := Map_Split(permVoteChannel', receivedPermission); } //// Permission accounting diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl index 3a2a5cc88..999327047 100644 --- a/Test/civl/samples/alloc-mem.bpl +++ b/Test/civl/samples/alloc-mem.bpl @@ -9,7 +9,7 @@ function {:inline} PoolInv(unallocated: [int]bool, pool: Set int): (bool) yield procedure {:layer 2} Main () preserves call Yield(); { - var {:layer 1,2} {:linear} l: Map int int; + var {:layer 1,2} {:linear} l: Cell int int; var i: int; while (*) invariant {:yields} true; @@ -20,13 +20,13 @@ preserves call Yield(); } } -yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in: Map int int, i: int) +yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in: Cell int int, i: int) preserves call Yield(); -requires {:layer 1,2} Map_Contains(local_in, i); +requires {:layer 1,2} local_in->key == i; { var y, o: int; - var {:layer 1,2} {:linear} local: Map int int; - var {:layer 1,2} {:linear} l: Map int int; + var {:layer 1,2} {:linear} local: Cell int int; + var {:layer 1,2} {:linear} l: Cell int int; call local := Write(local_in, i, 42); call o := Read(local, i); @@ -43,7 +43,7 @@ requires {:layer 1,2} Map_Contains(local_in, i); } } -right action {:layer 2} atomic_Alloc() returns ({:linear} l: Map int int, i: int) +right action {:layer 2} atomic_Alloc() returns ({:linear} l: Cell int int, i: int) modifies pool; { assume Set_Contains(pool, i); @@ -51,51 +51,50 @@ modifies pool; } yield procedure {:layer 1} -Alloc() returns ({:layer 1} {:linear} l: Map int int, i: int) +Alloc() returns ({:layer 1} {:linear} l: Cell int int, i: int) refines atomic_Alloc; preserves call Yield(); -ensures {:layer 1} Map_Contains(l, i); +ensures {:layer 1} l->key == i; { call i := PickAddr(); call {:layer 1} l, pool := AllocLinear(i, pool); } -left action {:layer 2} atomic_Free({:linear_in} l: Map int int, i: int) +left action {:layer 2} atomic_Free({:linear_in} l: Cell int int, i: int) modifies pool; { var {:linear} one_i: One int; - var v: int; - call one_i, v := Map_Unpack(i, l); + var _v: int; + call one_i, _v := Cell_Unpack(l); call One_Put(pool, one_i); } -yield procedure {:layer 1} Free({:layer 1} {:linear_in} l: Map int int, i: int) +yield procedure {:layer 1} Free({:layer 1} {:linear_in} l: Cell int int, i: int) refines atomic_Free; -requires {:layer 1} Map_Contains(l, i); +requires {:layer 1} l->key == i; preserves call Yield(); { call {:layer 1} pool := FreeLinear(l, i, pool); call ReturnAddr(i); } -both action {:layer 2} atomic_Read ({:linear} l: Map int int, i: int) returns (o: int) +both action {:layer 2} atomic_Read ({:linear} l: Cell int int, i: int) returns (o: int) { - assert Map_Contains(l, i); - o := l->val[i]; + assert l->key == i; + o := l->val; } -both action {:layer 2} atomic_Write ({:linear_in} l: Map int int, i: int, o: int) - returns ({:linear} l': Map int int) +both action {:layer 2} atomic_Write ({:linear_in} l: Cell int int, i: int, o: int) + returns ({:linear} l': Cell int int) { var {:linear} one_i: One int; - var v: int; - l' := l; - call one_i, v := Map_Get(l', i); - call Map_Put(l', one_i, o); + var _v: int; + call one_i, _v := Cell_Unpack(l); + call l' := Cell_Pack(one_i, o); } yield procedure {:layer 1} -Read ({:layer 1} {:linear} l: Map int int, i: int) returns (o: int) +Read ({:layer 1} {:linear} l: Cell int int, i: int) returns (o: int) refines atomic_Read; requires call YieldMem(l, i); ensures call Yield(); @@ -104,11 +103,11 @@ ensures call Yield(); } yield procedure {:layer 1} -Write ({:layer 1} {:linear_in} l: Map int int, i: int, o: int) - returns ({:layer 1} {:linear} l': Map int int) +Write ({:layer 1} {:linear_in} l: Cell int int, i: int, o: int) + returns ({:layer 1} {:linear} l': Cell int int) refines atomic_Write; requires call Yield(); -requires {:layer 1} Map_Contains(l, i); +requires {:layer 1} l->key == i; ensures call YieldMem(l', i); { call WriteLow(i, o); @@ -116,41 +115,40 @@ ensures call YieldMem(l', i); } pure action AllocLinear (i: int, {:linear_in} pool: Set int) - returns ({:linear} l: Map int int, {:linear} pool': Set int) + returns ({:linear} l: Cell int int, {:linear} pool': Set int) { var {:linear} one_i: One int; var m: int; pool' := pool; call one_i := One_Get(pool', i); - call l := Map_Pack(one_i, m); + call l := Cell_Pack(one_i, m); } -pure action FreeLinear ({:linear_in} l: Map int int, i: int, {:linear_in} pool: Set int) +pure action FreeLinear ({:linear_in} l: Cell int int, i: int, {:linear_in} pool: Set int) returns ({:linear} pool': Set int) { var {:linear} one_i: One int; - var v: int; - call one_i, v := Map_Unpack(i, l); + var _v: int; + call one_i, _v := Cell_Unpack(l); pool' := pool; call One_Put(pool', one_i); } -pure action WriteLinear ({:layer 1} {:linear_in} l: Map int int, i: int, o: int) - returns ({:layer 1} {:linear} l': Map int int) +pure action WriteLinear ({:layer 1} {:linear_in} l: Cell int int, i: int, o: int) + returns ({:layer 1} {:linear} l': Cell int int) { var {:linear} one_i: One int; - var v: int; - l' := l; - call one_i, v := Map_Get(l', i); - call Map_Put(l', one_i, o); + var _v: int; + call one_i, _v := Cell_Unpack(l); + call l' := Cell_Pack(one_i, o); } yield invariant {:layer 1} Yield (); invariant PoolInv(unallocated, pool); -yield invariant {:layer 1} YieldMem ({:layer 1} {:linear} l: Map int int, i: int); +yield invariant {:layer 1} YieldMem ({:layer 1} {:linear} l: Cell int int, i: int); invariant PoolInv(unallocated, pool); -invariant Map_Contains(l, i) && Map_At(l, i) == mem[i]; +invariant l->key == i && l->val == mem[i]; var {:layer 1, 2} {:linear} pool: Set int; var {:layer 0, 1} mem: [int]int; diff --git a/Test/civl/samples/alloc-mem.bpl.expect b/Test/civl/samples/alloc-mem.bpl.expect index 4f69d0535..0999d9ead 100644 --- a/Test/civl/samples/alloc-mem.bpl.expect +++ b/Test/civl/samples/alloc-mem.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 15 verified, 0 errors +Boogie program verifier finished with 13 verified, 0 errors diff --git a/Test/civl/samples/civl-paper.bpl b/Test/civl/samples/civl-paper.bpl index aa5c8cd3d..75b282591 100644 --- a/Test/civl/samples/civl-paper.bpl +++ b/Test/civl/samples/civl-paper.bpl @@ -139,7 +139,17 @@ refines AtomicLoad; both action {:layer 1,3} AtomicStore({:linear_in} l_in: Map int int, a: int, v: int) returns ({:linear} l_out: Map int int) -{ var {:linear} one_a: One int; var v': int; l_out := l_in; call one_a, v' := Map_Get(l_out, a); call Map_Put(l_out, one_a, v); } +{ + var {:linear} one_a: One int; + var {:linear} cell_a: Cell int int; + var _v: int; + + l_out := l_in; + one_a := One(a); + call _v := Map_Split(l_out, one_a); + call cell_a := Cell_Pack(one_a, v); + call Map_Put(l_out, cell_a); +} yield procedure {:layer 0} Store({:linear_in} l_in: Map int int, a: int, v: int) returns ({:linear} l_out: Map int int); refines AtomicStore; diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 4bfb3e184..595a46332 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -26,15 +26,15 @@ preserves call YieldInvDom#4(); var {:linear} stack: Map (Loc (Node X)) (Node X); var {:linear} treiber: Treiber X; var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} map_t: Map (Loc (Treiber X)) (Treiber X); + var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); top := None(); call stack := Map_MakeEmpty(); treiber := Treiber(top, stack); call one_loc_t := One_New(); - call map_t := Map_Pack(one_loc_t, treiber); + call cell_t := Cell_Pack(one_loc_t, treiber); loc_t := one_loc_t->val; - call AllocTreiber(loc_t, map_t); + call AllocTreiber(cell_t); call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty())); call {:layer 4} AbsLemma(treiber); } @@ -99,16 +99,19 @@ modifies ts; var {:linear} treiber: Treiber X; var top: Option (Loc (Node X)); var {:linear} stack: Map (Loc (Node X)) (Node X); + var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); assume Map_Contains(ts, loc_t); if (success) { - call one_loc_t, treiber := Map_Get(ts, loc_t); + call cell_t := Map_Get(ts, loc_t); + call one_loc_t, treiber := Cell_Unpack(cell_t); Treiber(top, stack) := treiber; assume top != None(); assume 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 cell_t := Cell_Pack(one_loc_t, treiber); + call Map_Put(ts, cell_t); } } yield procedure {:layer 3} PopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x: X) @@ -137,16 +140,21 @@ modifies ts; var top: Option (Loc (Node X)); var {:linear} stack: Map (Loc (Node X)) (Node X); var {:linear} one_loc_n: One (Loc (Node X)); + var {:linear} cell_n: Cell (Loc (Node X)) (Node X); + var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); success := false; if (*) { success := true; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call cell_t := Map_Get(ts, loc_t); + call one_loc_t, treiber := Cell_Unpack(cell_t); Treiber(top, stack) := treiber; call one_loc_n := One_New(); - call Map_Put(stack, one_loc_n, Node(top, x)); + call cell_n := Cell_Pack(one_loc_n, Node(top, x)); + call Map_Put(stack, cell_n); treiber := Treiber(Some(one_loc_n->val), stack); - call Map_Put(ts, one_loc_t, treiber); + call cell_t := Cell_Pack(one_loc_t, treiber); + call Map_Put(ts, cell_t); } } yield procedure {:layer 2} PushIntermediate(loc_t: Loc (Treiber X), x: X) returns (success: bool) @@ -156,15 +164,15 @@ preserves call YieldInv#2(loc_t); var loc_n: Option (Loc (Node X)); var new_loc_n: Loc (Node X); var {:linear} one_loc_n: One (Loc (Node X)); - var {:linear} map_n: Map (Loc (Node X)) (Node X); + var {:linear} cell_n: Cell (Loc (Node X)) (Node X); call loc_n := ReadTopOfStack#Push(loc_t); call one_loc_n := One_New(); new_loc_n := one_loc_n->val; - call map_n := Map_Pack(one_loc_n, Node(loc_n, x)); + call cell_n := Cell_Pack(one_loc_n, Node(loc_n, x)); call success := WriteTopOfStack(loc_t, loc_n, Some(new_loc_n)); if (success) { - call AllocNode(loc_t, new_loc_n, map_n); + call AllocNode(loc_t, cell_n); } } @@ -236,22 +244,22 @@ yield procedure {:layer 0} LoadNode#0(loc_t: Loc (Treiber X), loc_n: Loc (Node X refines AtomicLoadNode#0; left action {:layer 1, 2} AtomicAllocNode( - loc_t: Loc (Treiber X), loc_n: Loc (Node X), {:linear_in} map_n: Map (Loc (Node X)) (Node X)) + loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (Loc (Node X)) (Node X)) modifies ts; { var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} one_loc_n: One (Loc (Node X)); - var node: Node X; var {:linear} treiber: Treiber X; + var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); assert Map_Contains(ts, loc_t); - call one_loc_t, treiber := Map_Get(ts, loc_t); - call one_loc_n, node := Map_Unpack(loc_n, map_n); - call Map_Put(treiber->stack, one_loc_n, node); - call Map_Put(ts, one_loc_t, treiber); + call cell_t := Map_Get(ts, loc_t); + call one_loc_t, treiber := Cell_Unpack(cell_t); + call Map_Put(treiber->stack, cell_n); + call cell_t := Cell_Pack(one_loc_t, treiber); + call Map_Put(ts, cell_t); } yield procedure {:layer 0} AllocNode( - loc_t: Loc (Treiber X), loc_n: Loc (Node X), {:linear_in} map_n: Map (Loc (Node X)) (Node X)); + loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (Loc (Node X)) (Node X)); refines AtomicAllocNode; atomic action {:layer 1, 3} AtomicWriteTopOfStack( @@ -259,32 +267,31 @@ atomic action {:layer 1, 3} AtomicWriteTopOfStack( modifies ts; { var {:linear} treiber: Treiber X; + var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); var {:linear} one_loc_t: One (Loc (Treiber X)); assert Map_Contains(ts, loc_t); - call one_loc_t, treiber := Map_Get(ts, loc_t); + call cell_t := Map_Get(ts, loc_t); + call one_loc_t, treiber := Cell_Unpack(cell_t); if (old_loc_n == treiber->top) { treiber->top := new_loc_n; r := true; } else { r := false; } - call Map_Put(ts, one_loc_t, treiber); + call cell_t := Cell_Pack(one_loc_t, treiber); + call Map_Put(ts, cell_t); } yield procedure {:layer 0} WriteTopOfStack( loc_t: Loc (Treiber X), old_loc_n: Option (Loc (Node X)), new_loc_n: Option (Loc (Node X))) returns (r: bool); refines AtomicWriteTopOfStack; -atomic action {:layer 1, 4} AtomicAllocTreiber(loc_t: Loc (Treiber X), {:linear_in} map_t: Map (Loc (Treiber X)) (Treiber X)) +atomic action {:layer 1, 4} AtomicAllocTreiber({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)) modifies ts; { - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} treiber: Treiber X; - - call one_loc_t, treiber := Map_Unpack(loc_t, map_t); - call Map_Put(ts, one_loc_t, treiber); + call Map_Put(ts, cell_t); } -yield procedure {:layer 0} AllocTreiber(loc_t: Loc (Treiber X), {:linear_in} map_t: Map (Loc (Treiber X)) (Treiber X)); +yield procedure {:layer 0} AllocTreiber({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)); refines AtomicAllocTreiber; function {:inline} Domain(ts: Map (Loc (Treiber X)) (Treiber X), loc_t: Loc (Treiber X)): Set (Loc (Node X)) {