From 3785d51e5668d8e697307ac04d3bd712b8332c8d Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 30 Sep 2024 15:38:18 -0700 Subject: [PATCH 01/10] One_New -> Loc_New --- Source/Concurrency/LinearRewriter.cs | 2 +- Source/Core/CivlAttributes.cs | 4 ++-- Source/Core/base.bpl | 4 ++-- .../inductive-sequentialization/distributed-snapshot.bpl | 2 +- Test/civl/samples/treiber-stack.bpl | 8 ++++---- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 778cae571..4b0ad4e6a 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -149,7 +149,7 @@ public List RewriteCallCmd(CallCmd callCmd) { switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { - case "One_New": + case "Loc_New": case "One_To_Fractions": case "Fractions_To_One": case "Cell_Pack": diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 8c6e77732..d20124a84 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -217,7 +217,7 @@ public static class CivlPrimitives { public static HashSet LinearPrimitives = new() { - "One_New", "One_To_Fractions", "Fractions_To_One", + "Loc_New", "One_To_Fractions", "Fractions_To_One", "Cell_Pack", "Cell_Unpack", "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join", "Map_Get", "Map_Put", "Map_Assume", "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" @@ -243,7 +243,7 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) { switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { - case "One_New": + case "Loc_New": case "One_To_Fractions": case "Fractions_To_One": case "Cell_Pack": diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 0f9b93fa4..8ab574bdf 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -360,9 +360,9 @@ pure procedure {:inline 1} Map_Assume({:linear} src: Map K V, {:linear} dst type Loc; -pure procedure {:inline 1} One_New() returns ({:linear} {:pool "One_New"} l: One Loc) +pure procedure {:inline 1} Loc_New() returns ({:linear} {:pool "Loc_New"} l: One Loc) { - assume {:add_to_pool "One_New", l} true; + assume {:add_to_pool "Loc_New", l} true; } procedure create_async(PA: T); diff --git a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl index 1fd91f61b..1c88d56c0 100644 --- a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl +++ b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl @@ -100,7 +100,7 @@ refines GetSnapshot; var {:linear} sps_second: Set MemIndexPiece; var snapshot': Snapshot; - call one_loc_channel := One_New(); + call one_loc_channel := Loc_New(); call channelOps := One_To_Fractions(one_loc_channel, ChannelOps()); call one_r := One_Get(channelOps, ToReceive(one_loc_channel->val)); call one_s_first := One_Get(channelOps, ToSendFirst(one_loc_channel->val)); diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 5a164c949..c635766ac 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -67,7 +67,7 @@ modifies Stack; { var {:linear} one_loc_t: One Loc; - call one_loc_t := One_New(); + 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()); @@ -85,7 +85,7 @@ preserves call StackDom(); top := None(); call stack := Map_MakeEmpty(); treiber := Treiber(top, stack); - call one_loc_t := One_New(); + call one_loc_t := Loc_New(); call cell_t := Cell_Pack(one_loc_t, treiber); loc_t := one_loc_t->val; call AllocTreiber#0(cell_t); @@ -178,7 +178,7 @@ asserts Map_Contains(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); Treiber(top, stack) := treiber; assume loc_n is None || Map_Contains(stack, loc_n->t); - call one_loc_n := One_New(); + call one_loc_n := Loc_New(); call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces()); call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces())); new_loc_n := left_loc_piece->val; @@ -201,7 +201,7 @@ refines AtomicAllocNode#3; var {:linear} left_loc_piece: One (Fraction Loc LocPiece); call loc_n := ReadTopOfStack#Push(loc_t); - call one_loc_n := One_New(); + call one_loc_n := Loc_New(); call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces()); call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces())); new_loc_n := left_loc_piece->val; From c48a9d46757f0fd125982c32f9fa0c0794b003ef Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 30 Sep 2024 16:31:21 -0700 Subject: [PATCH 02/10] removed Cell from Map_Get and Map_Put --- Source/Concurrency/LinearRewriter.cs | 16 +- Source/Core/base.bpl | 4 +- .../distributed-snapshot.bpl | 8 +- Test/civl/paxos/PaxosImpl.bpl | 16 +- Test/civl/samples/civl-paper.bpl | 7 +- Test/civl/samples/treiber-stack.bpl | 150 +++++++----------- 6 files changed, 80 insertions(+), 121 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 4b0ad4e6a..1d631a74b 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -451,7 +451,8 @@ private List RewriteMapGet(CallCmd callCmd) var cmdSeq = new List(); var path = callCmd.Ins[0]; var k = callCmd.Ins[1]; - var c = callCmd.Outs[0]; + var l = callCmd.Outs[0]; + var v = callCmd.Outs[1]; var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); var domain = instantiation["K"]; @@ -460,9 +461,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 cellConstructor = CellConstructor(domain, range); - cmdSeq.Add( - CmdHelper.AssignCmd(c.Decl, ExprHelper.FunctionCall(cellConstructor, k, ExprHelper.FunctionCall(mapAtFunc, path, k)))); + 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))); cmdSeq.Add( CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapRemoveFunc, path, k))); @@ -474,7 +475,8 @@ private List RewriteMapPut(CallCmd callCmd) { var cmdSeq = new List(); var path = callCmd.Ins[0]; - var c = callCmd.Ins[1]; + var l = callCmd.Ins[1]; + var v = callCmd.Ins[2]; var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); var domain = instantiation["K"]; @@ -482,9 +484,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, Key(c))), attribute)); + cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Not(ExprHelper.FunctionCall(mapContainsFunc, path, Val(l))), attribute)); cmdSeq.Add( - CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, Key(c), Val(c)))); + CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, Val(l), v))); ResolveAndTypecheck(options, cmdSeq); return cmdSeq; diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 8ab574bdf..7309d5f7e 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -351,8 +351,8 @@ pure procedure {:inline 1} Map_Unpack({:linear_in} m: Map K V) returns ({:l } pure procedure Map_Split({:linear} path: Map K V, s: Set K) returns ({:linear} m: Map K V); pure procedure Map_Join({:linear} path: Map K V, {:linear_in} m: Map K 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 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 {: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/inductive-sequentialization/distributed-snapshot.bpl b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl index 1c88d56c0..337d0a721 100644 --- a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl +++ b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl @@ -215,14 +215,12 @@ asserts IsSendFirst(perm->val->val) && IsValidMemIndexPiece(perm->val); { var {:pool "SV_read_f"} sv: StampedValue; var piece: MemIndexPiece; - var {:linear} cell: Cell MemIndexPiece StampedValue; piece := perm->val; assume {:add_to_pool "MemIndexPieces", piece} true; assume {:add_to_pool "MemIndices", 0, NumMemIndices} true; assume {:add_to_pool "SV_read_f", sv, mem[piece->id]} sv->ts < mem[piece->id]->ts || sv == mem[piece->id]; - call cell := Cell_Pack(perm, sv); - call Map_Put(pset, cell); + call Map_Put(pset, perm, sv); assume {:add_to_pool "Data", pset->val} true; } @@ -291,14 +289,12 @@ asserts {:add_to_pool "SV_read_s", mem[perm->val->id]} IsSendSecond(perm->val->v { var {:pool "SV_read_s"} sv: StampedValue; var piece: MemIndexPiece; - var {:linear} cell: Cell MemIndexPiece StampedValue; piece := perm->val; assume {:add_to_pool "MemIndexPieces", piece} true; assume {:add_to_pool "MemIndices", 0, NumMemIndices} true; assume {:add_to_pool "SV_read_s", sv, mem[piece->id]} sv->ts > mem[piece->id]->ts || sv == mem[piece->id]; - call cell := Cell_Pack(perm, sv); - call Map_Put(pset, cell); + call Map_Put(pset, perm, sv); assume {:add_to_pool "Data", pset->val} true; } diff --git a/Test/civl/paxos/PaxosImpl.bpl b/Test/civl/paxos/PaxosImpl.bpl index 0b4ecb290..9e97e1917 100644 --- a/Test/civl/paxos/PaxosImpl.bpl +++ b/Test/civl/paxos/PaxosImpl.bpl @@ -377,41 +377,33 @@ 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 cell_p := Cell_Pack(p, joinResponse); - call Map_Put(permJoinChannel', cell_p); + call Map_Put(permJoinChannel', p, joinResponse); } pure action ReceiveJoinResponseIntro(round: Round, joinResponse: JoinResponse, {:linear_in} permJoinChannel: JoinResponseChannel) returns ({:linear} receivedPermission: One Permission, {:linear} permJoinChannel': JoinResponseChannel) { var _x: JoinResponse; - var {:linear} cell_p: Cell Permission JoinResponse; permJoinChannel' := permJoinChannel; - call cell_p := Map_Get(permJoinChannel', JoinPerm(round, joinResponse->from)); - call receivedPermission, _x := Cell_Unpack(cell_p); + call receivedPermission, _x := Map_Get(permJoinChannel', JoinPerm(round, joinResponse->from)); } 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 cell_p := Cell_Pack(p, voteResponse); - call Map_Put(permVoteChannel', cell_p); + call Map_Put(permVoteChannel', p, voteResponse); } pure action ReceiveVoteResponseIntro(round: Round, voteResponse: VoteResponse, {:linear_in} permVoteChannel: VoteResponseChannel) returns ({:linear} receivedPermission: One Permission, {:linear} permVoteChannel': VoteResponseChannel) { - var {:linear} cell_p: Cell Permission VoteResponse; var _x: VoteResponse; permVoteChannel' := permVoteChannel; - call cell_p := Map_Get(permVoteChannel', VotePerm(round, voteResponse->from)); - call receivedPermission, _x := Cell_Unpack(cell_p); + call receivedPermission, _x := Map_Get(permVoteChannel', VotePerm(round, voteResponse->from)); } //// Permission accounting diff --git a/Test/civl/samples/civl-paper.bpl b/Test/civl/samples/civl-paper.bpl index af3bd3f29..6b06e5312 100644 --- a/Test/civl/samples/civl-paper.bpl +++ b/Test/civl/samples/civl-paper.bpl @@ -141,14 +141,11 @@ both action {:layer 1,3} AtomicStore({:linear_in} l_in: Map int int, a: int, v: returns ({:linear} l_out: Map int int) { var {:linear} one_a: One int; - var {:linear} cell_a: Cell int int; var _v: int; l_out := l_in; - call cell_a := Map_Get(l_out, a); - call one_a, _v := Cell_Unpack(cell_a); - call cell_a := Cell_Pack(one_a, v); - call Map_Put(l_out, cell_a); + call one_a, _v := Map_Get(l_out, a); + call Map_Put(l_out, one_a, v); } yield procedure {:layer 0} Store({:linear_in} l_in: Map int int, a: int, v: int) returns ({:linear} l_out: Map int int); diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index c635766ac..bacb9d408 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -6,11 +6,10 @@ function {:inline} AllLocPieces(): Set LocPiece { Set_Add(Set_Add(Set_Empty(), Left()), Right()) } -type TreiberNode _; -type LocTreiberNode T = Fraction Loc LocPiece; -type StackElem T = Node (LocTreiberNode T) T; -type StackMap T = Map (LocTreiberNode T) (StackElem T); -datatype Treiber { Treiber(top: Option (LocTreiberNode T), {:linear} stack: StackMap T) } +type LocTreiberNode = Fraction Loc LocPiece; +type StackElem T = Node LocTreiberNode T; +type StackMap T = Map LocTreiberNode (StackElem T); +datatype Treiber { Treiber(top: Option LocTreiberNode, {:linear} stack: StackMap T) } type X; // module type parameter @@ -19,7 +18,7 @@ var {:layer 0, 4} {:linear} ts: Map Loc (Treiber X); /// Yield invariants -function {:inline} Domain(ts: Map Loc (Treiber X), loc_t: Loc): Set (LocTreiberNode X) { +function {:inline} Domain(ts: Map Loc (Treiber X), loc_t: Loc): Set LocTreiberNode { ts->val[loc_t]->stack->dom } @@ -28,14 +27,14 @@ 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 X :: Set_Contains(Domain(ts, loc_t), loc_n) ==> +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))); -yield invariant {:layer 2} LocInStackOrNone(loc_t: Loc, loc_n: Option (LocTreiberNode X)); +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); -yield invariant {:layer 3} LocInStack(loc_t: Loc, loc_n: LocTreiberNode X); +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); @@ -44,7 +43,7 @@ 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 X :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==> +invariant (forall {:pool "A"} loc_n: LocTreiberNode :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==> loc_n == Fraction(loc_n->val, Left(), AllLocPieces()) && (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)); @@ -53,7 +52,7 @@ yield invariant {:layer 4} StackDom(); invariant Stack->dom == ts->dom; yield invariant {:layer 4} PushLocInStack( - loc_t: Loc, node: StackElem X, new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)); + 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 == Fraction(new_loc_n->val, Right(), AllLocPieces()); @@ -76,19 +75,17 @@ yield procedure {:layer 4} Alloc() returns (loc_t: Loc) refines AtomicAlloc; preserves call StackDom(); { - var top: Option (LocTreiberNode X); + var top: Option LocTreiberNode; var {:linear} stack: StackMap X; var {:linear} treiber: Treiber X; var {:linear} one_loc_t: One Loc; - var {:linear} cell_t: Cell Loc (Treiber X); top := None(); call stack := Map_MakeEmpty(); treiber := Treiber(top, stack); call one_loc_t := Loc_New(); - call cell_t := Cell_Pack(one_loc_t, treiber); loc_t := one_loc_t->val; - call AllocTreiber#0(cell_t); + call AllocTreiber#0(one_loc_t, treiber); call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty())); call {:layer 4} AbsLemma(treiber); } @@ -109,9 +106,9 @@ preserves call TopInStack(loc_t); preserves call ReachInStack(loc_t); preserves call StackDom(); { - var loc_n: Option (LocTreiberNode X); - var new_loc_n: LocTreiberNode X; - var {:linear} right_loc_piece: One (LocTreiberNode X); + var loc_n: Option LocTreiberNode; + var new_loc_n: LocTreiberNode; + var {:linear} right_loc_piece: One LocTreiberNode; var {:layer 4} old_treiber: Treiber X; call {:layer 4} old_treiber := Copy(ts->val[loc_t]); @@ -160,22 +157,19 @@ preserves call StackDom(); } atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc, x: X) - returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) + returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode) modifies ts; asserts Map_Contains(ts, loc_t); { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - var top: Option (LocTreiberNode X); + var top: Option LocTreiberNode; var {:linear} stack: StackMap X; var {:linear} one_loc_n: One Loc; - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - var {:linear} cell_t: Cell Loc (Treiber X); - var {:linear} loc_pieces: Set (Fraction Loc LocPiece); - var {:linear} left_loc_piece: One (Fraction Loc LocPiece); + var {:linear} loc_pieces: Set LocTreiberNode; + var {:linear} left_loc_piece: One LocTreiberNode; - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); Treiber(top, stack) := treiber; assume loc_n is None || Map_Contains(stack, loc_n->t); call one_loc_n := Loc_New(); @@ -183,22 +177,19 @@ asserts Map_Contains(ts, loc_t); call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces())); new_loc_n := left_loc_piece->val; call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces())); - call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x)); - call Map_Put(stack, cell_n); + call Map_Put(stack, left_loc_piece, Node(loc_n, x)); treiber := Treiber(top, stack); - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); + call Map_Put(ts, one_loc_t, treiber); } yield procedure {:layer 3} AllocNode#3(loc_t: Loc, x: X) - returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) + returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode) preserves call TopInStack(loc_t); ensures call LocInStackOrNone(loc_t, Some(new_loc_n)); refines AtomicAllocNode#3; { var {:linear} one_loc_n: One Loc; - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - var {:linear} loc_pieces: Set (Fraction Loc LocPiece); - var {:linear} left_loc_piece: One (Fraction Loc LocPiece); + var {:linear} loc_pieces: Set LocTreiberNode; + var {:linear} left_loc_piece: One LocTreiberNode; call loc_n := ReadTopOfStack#Push(loc_t); call one_loc_n := Loc_New(); @@ -206,31 +197,27 @@ refines AtomicAllocNode#3; call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces())); new_loc_n := left_loc_piece->val; call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces())); - call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x)); - call AllocNode#0(loc_t, cell_n); + call AllocNode#0(loc_t, left_loc_piece, Node(loc_n, x)); } atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc) returns (success: bool, x_opt: Option X) modifies ts; { var {:linear} one_loc_t: One Loc; - var loc_n: Option (LocTreiberNode X); + var loc_n: Option LocTreiberNode; var {:linear} treiber: Treiber X; - var top: Option (LocTreiberNode X); + var top: Option LocTreiberNode; var {:linear} stack: StackMap X; - var {:linear} cell_t: Cell Loc (Treiber X); var x: X; assert Map_Contains(ts, loc_t); if (*) { - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); + call one_loc_t, treiber := Map_Get(ts, 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 cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); + call Map_Put(ts, one_loc_t, treiber); x_opt := Some(x); success := true; } @@ -247,7 +234,7 @@ yield procedure {:layer 3} PopIntermediate(loc_t: Loc) returns (success: bool, x refines AtomicPopIntermediate; preserves call TopInStack(loc_t); { - var loc_n, new_loc_n: Option (LocTreiberNode X); + var loc_n, new_loc_n: Option LocTreiberNode; var node: StackElem X; var x: X; @@ -269,12 +256,12 @@ preserves call TopInStack(loc_t); } } -right action {:layer 3} AtomicReadTopOfStack#Push(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) +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); } -yield procedure {:layer 2} ReadTopOfStack#Push(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) +yield procedure {:layer 2} ReadTopOfStack#Push(loc_t: Loc) returns (loc_n: Option LocTreiberNode) preserves call TopInStack(loc_t); ensures call LocInStackOrNone(loc_t, loc_n); refines AtomicReadTopOfStack#Push; @@ -282,12 +269,12 @@ refines AtomicReadTopOfStack#Push; call loc_n := ReadTopOfStack#0(loc_t); } -atomic action {:layer 3} AtomicReadTopOfStack#Pop(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) +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); } -yield procedure {:layer 2} ReadTopOfStack#Pop(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) +yield procedure {:layer 2} ReadTopOfStack#Pop(loc_t: Loc) returns (loc_n: Option LocTreiberNode) preserves call TopInStack(loc_t); ensures call LocInStackOrNone(loc_t, loc_n); refines AtomicReadTopOfStack#Pop; @@ -295,7 +282,7 @@ refines AtomicReadTopOfStack#Pop; call loc_n := ReadTopOfStack#0(loc_t); } -right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc, loc_n: LocTreiberNode X) returns (node: StackElem X) +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); @@ -304,93 +291,78 @@ right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc, loc_n: LocTreiberNode X) /// Primitives -atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc, loc_n: LocTreiberNode X) returns (node: StackElem X) +atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) returns (node: StackElem X) modifies ts; refines AtomicLoadNode#1; { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell Loc (Treiber X); - var top: Option (LocTreiberNode X); + var top: Option LocTreiberNode; var {:linear} stack: StackMap X; - var {:linear} one_loc_n: One (LocTreiberNode X); - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); + var {:linear} one_loc_n: One LocTreiberNode; - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); Treiber(top, stack) := treiber; - call cell_n := Map_Get(stack, loc_n); - call one_loc_n, node := Cell_Unpack(cell_n); - call cell_n := Cell_Pack(one_loc_n, node); - call Map_Put(stack, cell_n); + call one_loc_n, node := Map_Get(stack, loc_n); + call Map_Put(stack, one_loc_n, node); treiber := Treiber(top, stack); - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); + call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} LoadNode#0(loc_t: Loc, loc_n: LocTreiberNode X) returns (node: StackElem X); +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 X)) +atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode) modifies ts; { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell Loc (Treiber X); - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); loc_n := treiber->top; - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); + call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)); +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 X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool) + loc_t: Loc, old_loc_n: Option LocTreiberNode, new_loc_n: Option LocTreiberNode) returns (success: bool) modifies ts; { var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell Loc (Treiber X); var {:linear} one_loc_t: One Loc; - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); if (old_loc_n == treiber->top) { treiber->top := new_loc_n; success := true; } else { success := false; } - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); + call Map_Put(ts, one_loc_t, treiber); } yield procedure {:layer 0} WriteTopOfStack#0( - loc_t: Loc, old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool); + 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} cell_n: Cell (LocTreiberNode X) (StackElem X)) +atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X) modifies ts; { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell Loc (Treiber X); - 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); + 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); } -yield procedure {:layer 0} AllocNode#0(loc_t: Loc, {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)); +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} cell_t: Cell Loc (Treiber X)) +atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X) modifies ts; { - call Map_Put(ts, cell_t); + call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} AllocTreiber#0({:linear_in} cell_t: Cell Loc (Treiber X)); +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 @@ -417,7 +389,7 @@ ensures absStack == AbsDefinition(treiber'); free ensures absStack == Abs(treiber); free ensures absStack == Abs(treiber'); { - var loc_n: Option (LocTreiberNode X); + var loc_n: Option LocTreiberNode; var n: StackElem X; if (treiber->top == None()) { From ab6ff888ad6a641de142f726d017598d4e291e17 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 30 Sep 2024 21:50:22 -0700 Subject: [PATCH 03/10] removed Fraction --- Source/Concurrency/LinearRewriter.cs | 3 +- Source/Core/CivlAttributes.cs | 5 +- Source/Core/base.bpl | 25 +- .../distributed-snapshot.bpl | 329 ------------------ .../distributed-snapshot.bpl.expect | 2 - Test/civl/samples/treiber-stack.bpl | 26 +- 6 files changed, 23 insertions(+), 367 deletions(-) delete mode 100644 Test/civl/inductive-sequentialization/distributed-snapshot.bpl delete mode 100644 Test/civl/inductive-sequentialization/distributed-snapshot.bpl.expect diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 1d631a74b..3c895ec6c 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -150,8 +150,7 @@ public List RewriteCallCmd(CallCmd callCmd) switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { case "Loc_New": - case "One_To_Fractions": - case "Fractions_To_One": + case "KeyedLocs_New": case "Cell_Pack": case "Cell_Unpack": case "Set_MakeEmpty": diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index d20124a84..15c08303b 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -217,7 +217,7 @@ public static class CivlPrimitives { public static HashSet LinearPrimitives = new() { - "Loc_New", "One_To_Fractions", "Fractions_To_One", + "Loc_New", "KeyedLocs_New", "Cell_Pack", "Cell_Unpack", "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join", "Map_Get", "Map_Put", "Map_Assume", "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" @@ -244,8 +244,7 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { case "Loc_New": - case "One_To_Fractions": - case "Fractions_To_One": + case "KeyedLocs_New": case "Cell_Pack": case "Cell_Unpack": case "Set_MakeEmpty": diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 7309d5f7e..17c364c2c 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -289,23 +289,6 @@ function {:inline} One_Collector(a: One T): [T]bool MapOne(a->val) } -datatype Fraction { Fraction(val: T, id: K, ids: Set K) } - -function {:inline} AllPieces(t: T, ids: Set K): Set (Fraction T K) -{ - Set((lambda piece: Fraction T K :: piece->val == t && Set_Contains(ids, piece->id) && piece->ids == ids)) -} - -pure procedure {:inline 1} One_To_Fractions({:linear_in} one_t: One T, ids: Set K) returns ({:linear} pieces: Set (Fraction T K)) -{ - pieces := AllPieces(one_t->val, ids); -} - -pure procedure {:inline 1} Fractions_To_One({:linear_out} one_t: One T, ids: Set K, {:linear_in} pieces: Set (Fraction T K)) -{ - assert pieces == AllPieces(one_t->val, ids); -} - /// singleton map datatype Cell { Cell(key: T, val: U) } @@ -365,6 +348,14 @@ pure procedure {:inline 1} Loc_New() returns ({:linear} {:pool "Loc_New"} l: One assume {:add_to_pool "Loc_New", l} true; } +datatype KeyedLoc { KeyedLoc(l: Loc, k: K) } + +pure procedure {:inline 1} KeyedLocs_New(ks: Set K) returns ({:pool "Loc_New"} l: Loc, {:linear} keyed_locs: Set (KeyedLoc K)) +{ + assume {:add_to_pool "Loc_New", l} true; + keyed_locs := Set((lambda x: KeyedLoc K :: x->l == l && Set_Contains(ks, x->k))); +} + procedure create_async(PA: T); procedure create_asyncs(PAs: [T]bool); procedure create_multi_asyncs(PAs: [T]int); diff --git a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl deleted file mode 100644 index 337d0a721..000000000 --- a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl +++ /dev/null @@ -1,329 +0,0 @@ -// RUN: %parallel-boogie /vcsSplitOnEveryAssert "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type Value; - -type Tid; - -datatype StampedValue { - StampedValue(ts: int, value: Value) -} - -type Channel; // Send + Receive -type ChannelPiece = Fraction Loc ChannelOp; // Send or Receive piece -type MemIndexPiece = Fraction ChannelPiece int; // Each mem index piece of Channel Piece - -type Snapshot = [int]StampedValue; - -datatype ChannelOp { - Receive(), - SendFirst(), - SendSecond() -} - -function {:inline} ChannelOps(): Set ChannelOp { - Set_Add(Set_Add(Set_Add(Set_Empty(), Receive()), SendFirst()), SendSecond()) -} - -function {:inline} IsReceive(piece: ChannelPiece): bool { - piece == Fraction(piece->val, Receive(), ChannelOps()) -} - -function {:inline} IsSendFirst(piece: ChannelPiece): bool { - piece == Fraction(piece->val, SendFirst(), ChannelOps()) -} - -function {:inline} IsSendSecond(piece: ChannelPiece): bool { - piece == Fraction(piece->val, SendSecond(), ChannelOps()) -} - -function {:inline} ToReceive(loc_channel: Loc): ChannelPiece { - Fraction(loc_channel, Receive(), ChannelOps()) -} - -function {:inline} ToSendFirst(loc_channel: Loc): ChannelPiece { - Fraction(loc_channel, SendFirst(), ChannelOps()) -} - -function {:inline} ToSendSecond(loc_channel: Loc): ChannelPiece { - Fraction(loc_channel, SendSecond(), ChannelOps()) -} - -const NumMemIndices: int; -axiom NumMemIndices >= 1; - -const MemIndices: Set int; -axiom (forall x: int :: Set_Contains(MemIndices, x) <==> 1 <= x && x <= NumMemIndices); - -function {:inline} MemIndexPieces(s: ChannelPiece, j: int): Set MemIndexPiece { - Set((lambda {:pool "MemIndexPieces"} x: MemIndexPiece :: x->val == s && x->ids == MemIndices && 1 <= x->id && x->id <= j)) -} - -function {:inline} AllMemIndexPieces(s: ChannelPiece): Set MemIndexPiece { - MemIndexPieces(s, NumMemIndices) -} - -function {:inline} IsValidMemIndexPiece(piece: MemIndexPiece): bool { - Set_Contains(piece->ids, piece->id) && - piece->ids == MemIndices -} - -function {:inline} MemIndexPiece(cp: ChannelPiece, i: int): MemIndexPiece -{ - Fraction(cp, i, MemIndices) -} - -function {:inline} Read_f_asyncs(sps: Set MemIndexPiece): [read_f]bool { - (lambda {:pool "Read_PAs"} pa: read_f :: Set_Contains(sps, pa->perm->val)) -} - -function {:inline} Read_s_asyncs(sps: Set MemIndexPiece): [read_s]bool { - (lambda {:pool "Read_PAs"} pa: read_s :: Set_Contains(sps, pa->perm->val)) -} - -var {:layer 0,3} mem: Snapshot; -var {:linear} {:layer 0,2} pset: Map MemIndexPiece StampedValue; - -atomic action {:layer 3} GetSnapshot() returns (snapshot: [int]StampedValue) -{ - assume (forall i:int :: 1 <= i && i <= NumMemIndices ==> snapshot[i] == mem[i]); -} -yield procedure {:layer 2} Coordinator() returns (snapshot: [int]StampedValue) -refines GetSnapshot; -{ - var {:linear} one_loc_channel: One Loc; - var {:linear} channelOps: Set ChannelPiece; - var {:linear} one_r: One ChannelPiece; - var {:linear} one_s_first: One ChannelPiece; - var {:linear} one_s_second: One ChannelPiece; - var {:linear} sps_first: Set MemIndexPiece; - var {:linear} sps_second: Set MemIndexPiece; - var snapshot': Snapshot; - - call one_loc_channel := Loc_New(); - call channelOps := One_To_Fractions(one_loc_channel, ChannelOps()); - call one_r := One_Get(channelOps, ToReceive(one_loc_channel->val)); - call one_s_first := One_Get(channelOps, ToSendFirst(one_loc_channel->val)); - call one_s_second := One_Get(channelOps, ToSendSecond(one_loc_channel->val)); - call sps_first := One_To_Fractions(one_s_first, MemIndices); - call sps_second := One_To_Fractions(one_s_second, MemIndices); - - while (true) - invariant {:yields} true; - invariant {:layer 2} sps_first == AllMemIndexPieces(one_s_first->val); - invariant {:layer 2} sps_second == AllMemIndexPieces(one_s_second->val); - { - async call {:skip} _main_f(one_s_first->val, sps_first); - par Yield() | YieldFirstScan(one_r, one_s_first->val); - call sps_first, snapshot := _ReceiveFirst(one_r, one_s_first->val); - call _main_s(one_s_second->val, sps_second); - call sps_second, snapshot' := _ReceiveSecond(one_r, one_s_second->val); - if (snapshot == snapshot') { - return; - } - } -} - -yield invariant {:layer 1} Yield(); - -yield invariant {:layer 2} YieldFirstScan({:linear} one_r: One ChannelPiece, s_first: ChannelPiece); -invariant IsReceive(one_r->val); -invariant s_first == ToSendFirst(one_r->val->val); -invariant (forall piece: MemIndexPiece :: Set_Contains(AllMemIndexPieces(s_first), piece) && Map_Contains(pset, piece) ==> - Map_At(pset, piece)->ts < mem[piece->id]->ts || Map_At(pset, piece) == mem[piece->id]); - -left action {:layer 2} ReceiveSecond({:linear} one_r: One ChannelPiece, s: ChannelPiece) returns ({:linear} sps: Set MemIndexPiece, snapshot: Snapshot) -modifies pset; -asserts one_r->val->val == s->val; -asserts IsReceive(one_r->val); -asserts IsSendSecond(s); -asserts Set_IsSubset(AllMemIndexPieces(s), pset->dom); -{ - var {:linear} map: Map MemIndexPiece StampedValue; - var data: [MemIndexPiece]StampedValue; - - call map := Map_Split(pset, AllMemIndexPieces(s)); - call sps, data := Map_Unpack(map); - snapshot := (lambda x: int :: data[Fraction(s, x, MemIndices)]); -} -yield procedure {:layer 1} _ReceiveSecond({:linear} one_r: One ChannelPiece, s: ChannelPiece) returns ({:linear} sps: Set MemIndexPiece, snapshot: Snapshot) -refines ReceiveSecond; -{ - call sps, snapshot := _ReceiveFirst(one_r, s); -} - -right action {:layer 1,2} ReceiveFirst({:linear} one_r: One ChannelPiece, s: ChannelPiece) returns ({:linear} sps: Set MemIndexPiece, snapshot: Snapshot) -modifies pset; -asserts one_r->val->val == s->val; -asserts IsReceive(one_r->val); -asserts IsSendFirst(s) || IsSendSecond(s); -{ - var {:linear} map: Map MemIndexPiece StampedValue; - var data: [MemIndexPiece]StampedValue; - - assume Set_IsSubset(AllMemIndexPieces(s), pset->dom); - call map := Map_Split(pset, AllMemIndexPieces(s)); - call sps, data := Map_Unpack(map); - snapshot := (lambda x: int :: data[Fraction(s, x, MemIndices)]); -} -yield procedure {:layer 0} _ReceiveFirst({:linear} one_r: One ChannelPiece, s: ChannelPiece) returns ({:linear} sps: Set MemIndexPiece, snapshot: Snapshot); -refines ReceiveFirst; - -async atomic action {:layer 1,2} write(i: int,v: Value) -modifies mem; -{ - var x: StampedValue; - - x := mem[i]; - mem[i] := StampedValue(x->ts + 1, v); -} -///////////////////////////////////////////////////////////////////////////////////////////// - -async action {:layer 2} main_f'(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece) -modifies pset; -asserts IsSendFirst(s); -asserts sps == AllMemIndexPieces(s); -{ - var {:pool "Data"} data: [MemIndexPiece]StampedValue; - var {:linear} map: Map MemIndexPiece StampedValue; - - assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - assume (forall i: int :: {:add_to_pool "X", i} 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i])); - call map := Map_Pack(sps, data); - call Map_Join(pset, map); -} - -async action {:layer 1} main_f(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece) -refines {:IS_right} main_f' using Inv_f; -creates read_f; -asserts IsSendFirst(s); -asserts sps == AllMemIndexPieces(s); -{ - var data: [MemIndexPiece]StampedValue; - - assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - call {:linear sps} create_asyncs(Read_f_asyncs(sps)); -} -yield procedure {:layer 0} _main_f(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece); -refines main_f; - -async action {:layer 1} -{:exit_condition Set_IsSubset(AllMemIndexPieces(perm->val->val), Set_Add(pset->dom, perm->val))} -read_f({:linear_in} perm: One MemIndexPiece) -modifies pset; -asserts IsSendFirst(perm->val->val) && IsValidMemIndexPiece(perm->val); -{ - var {:pool "SV_read_f"} sv: StampedValue; - var piece: MemIndexPiece; - - piece := perm->val; - assume {:add_to_pool "MemIndexPieces", piece} true; - assume {:add_to_pool "MemIndices", 0, NumMemIndices} true; - assume {:add_to_pool "SV_read_f", sv, mem[piece->id]} sv->ts < mem[piece->id]->ts || sv == mem[piece->id]; - call Map_Put(pset, perm, sv); - assume {:add_to_pool "Data", pset->val} true; -} - -action {:layer 1} Inv_f(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece) -modifies pset; -creates read_f; -asserts IsSendFirst(s); -asserts sps == AllMemIndexPieces(s); -{ - var {:pool "MemIndices"} j: int; - var {:linear} sps': Set MemIndexPiece; - var {:linear} done_set: Set MemIndexPiece; - var choice: read_f; - var {:linear} map: Map MemIndexPiece StampedValue; - var {:pool "Data"} data: [MemIndexPiece]StampedValue; - - assume {:add_to_pool "MemIndices", 0, j+1, NumMemIndices} {:add_to_pool "Data", data} 0 <= j && j <= NumMemIndices; - assume (forall {:pool "X"} i: int :: {:add_to_pool "X", i} 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i])); - assume {:add_to_pool "MemIndexPieces", Fraction(s, 1, MemIndices), Fraction(s, j+1, MemIndices), Fraction(s, NumMemIndices, MemIndices)} true; - sps' := sps; - call done_set := Set_Get(sps', MemIndexPieces(s, j)->val); - call map := Map_Pack(done_set, data); - call Map_Join(pset, map); - - if (j < NumMemIndices) { - choice := read_f(One(Fraction(s, j+1, MemIndices))); - call set_choice(choice); - assume {:add_to_pool "Read_PAs", choice} true; - call {:linear sps'} create_asyncs((Read_f_asyncs(sps'))); - } -} - -///////////////////////////////////////////////////////////////////////////////////////////// - -async action {:layer 2} main_s'(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece) -modifies pset; -asserts IsSendSecond(s); -asserts sps == AllMemIndexPieces(s); -{ - var {:pool "Data"} data: [MemIndexPiece]StampedValue; - var {:linear} map: Map MemIndexPiece StampedValue; - - assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - assume (forall i: int :: {:add_to_pool "X", i} 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i])); - call map := Map_Pack(sps, data); - call Map_Join(pset, map); -} - -async action {:layer 1} main_s(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece) -refines {:IS_left} main_s' using Inv_s; -creates read_s; -asserts IsSendSecond(s); -asserts sps == AllMemIndexPieces(s); -{ - var data: [MemIndexPiece]StampedValue; - - assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - call {:linear sps} create_asyncs(Read_s_asyncs(sps)); -} -yield procedure {:layer 0} _main_s(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece); -refines main_s; - -async left action {:layer 1} read_s({:linear_in} perm: One MemIndexPiece) -modifies pset; -asserts {:add_to_pool "SV_read_s", mem[perm->val->id]} IsSendSecond(perm->val->val) && IsValidMemIndexPiece(perm->val); -{ - var {:pool "SV_read_s"} sv: StampedValue; - var piece: MemIndexPiece; - - piece := perm->val; - assume {:add_to_pool "MemIndexPieces", piece} true; - assume {:add_to_pool "MemIndices", 0, NumMemIndices} true; - assume {:add_to_pool "SV_read_s", sv, mem[piece->id]} sv->ts > mem[piece->id]->ts || sv == mem[piece->id]; - call Map_Put(pset, perm, sv); - assume {:add_to_pool "Data", pset->val} true; -} - -action {:layer 1} Inv_s(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece) -modifies pset; -creates read_s; -asserts IsSendSecond(s); -asserts sps == AllMemIndexPieces(s); -{ - var {:pool "MemIndices"} j: int; - var {:linear} sps': Set MemIndexPiece; - var {:linear} done_set: Set MemIndexPiece; - var choice: read_s; - var {:linear} map: Map MemIndexPiece StampedValue; - var {:pool "Data"} data: [MemIndexPiece]StampedValue; - - assume {:add_to_pool "MemIndices", 0, j+1, NumMemIndices} {:add_to_pool "Data", data} 0 <= j && j <= NumMemIndices; - assume (forall {:pool "X"} i: int :: {:add_to_pool "X", i} 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i])); - assume {:add_to_pool "MemIndexPieces", Fraction(s, 1, MemIndices), Fraction(s, j+1, MemIndices), Fraction(s, NumMemIndices, MemIndices)} true; - - sps' := sps; - call done_set := Set_Get(sps', MemIndexPieces(s, j)->val); - call map := Map_Pack(done_set, data); - call Map_Join(pset, map); - - if (j < NumMemIndices) { - choice := read_s(One(Fraction(s, j+1, MemIndices))); - call set_choice(choice); - assume {:add_to_pool "Read_PAs", choice} true; - call {:linear sps'} create_asyncs(Read_s_asyncs(sps')); - } -} diff --git a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl.expect b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl.expect deleted file mode 100644 index 309f0e6f6..000000000 --- a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 55 verified, 0 errors diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index bacb9d408..022370ebd 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -6,7 +6,7 @@ function {:inline} AllLocPieces(): Set LocPiece { Set_Add(Set_Add(Set_Empty(), Left()), Right()) } -type LocTreiberNode = Fraction Loc 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) } @@ -44,7 +44,7 @@ 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 == Fraction(loc_n->val, Left(), AllLocPieces()) && + 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)); @@ -55,8 +55,8 @@ 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 == Fraction(new_loc_n->val, Right(), AllLocPieces()); -invariant new_loc_n == Fraction(new_loc_n->val, Left(), AllLocPieces()); +invariant right_loc_piece->val == KeyedLoc(new_loc_n->l, Right()); +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]); /// Layered implementation @@ -165,18 +165,17 @@ asserts Map_Contains(ts, loc_t); var {:linear} treiber: Treiber X; var top: Option LocTreiberNode; var {:linear} stack: StackMap X; - var {:linear} one_loc_n: One Loc; + var loc: Loc; var {:linear} loc_pieces: Set LocTreiberNode; var {:linear} left_loc_piece: One LocTreiberNode; call one_loc_t, treiber := Map_Get(ts, loc_t); Treiber(top, stack) := treiber; assume loc_n is None || Map_Contains(stack, loc_n->t); - call one_loc_n := Loc_New(); - call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces()); - call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces())); + call loc, loc_pieces := KeyedLocs_New(AllLocPieces()); + call left_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Left())); new_loc_n := left_loc_piece->val; - call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces())); + 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); @@ -187,16 +186,15 @@ preserves call TopInStack(loc_t); ensures call LocInStackOrNone(loc_t, Some(new_loc_n)); refines AtomicAllocNode#3; { - var {:linear} one_loc_n: One Loc; + var loc: Loc; var {:linear} loc_pieces: Set LocTreiberNode; var {:linear} left_loc_piece: One LocTreiberNode; call loc_n := ReadTopOfStack#Push(loc_t); - call one_loc_n := Loc_New(); - call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces()); - call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces())); + call loc, loc_pieces := KeyedLocs_New(AllLocPieces()); + call left_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Left())); new_loc_n := left_loc_piece->val; - call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces())); + call right_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Right())); call AllocNode#0(loc_t, left_loc_piece, Node(loc_n, x)); } From 8ea487a11e5a07265855c11e56050369ed9337f5 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 1 Oct 2024 06:29:30 -0700 Subject: [PATCH 04/10] KeyedLocs_New -> KeyedLocSet_New --- Source/Concurrency/LinearRewriter.cs | 2 +- Source/Core/CivlAttributes.cs | 4 ++-- Source/Core/base.bpl | 2 +- Test/civl/samples/treiber-stack.bpl | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 3c895ec6c..ede761988 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -150,7 +150,7 @@ public List RewriteCallCmd(CallCmd callCmd) switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { case "Loc_New": - case "KeyedLocs_New": + case "KeyedLocSet_New": case "Cell_Pack": case "Cell_Unpack": case "Set_MakeEmpty": diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 15c08303b..e110eb1d3 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -217,7 +217,7 @@ public static class CivlPrimitives { public static HashSet LinearPrimitives = new() { - "Loc_New", "KeyedLocs_New", + "Loc_New", "KeyedLocSet_New", "Cell_Pack", "Cell_Unpack", "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join", "Map_Get", "Map_Put", "Map_Assume", "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" @@ -244,7 +244,7 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { case "Loc_New": - case "KeyedLocs_New": + case "KeyedLocSet_New": case "Cell_Pack": case "Cell_Unpack": case "Set_MakeEmpty": diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 17c364c2c..c70cb59f2 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -350,7 +350,7 @@ pure procedure {:inline 1} Loc_New() returns ({:linear} {:pool "Loc_New"} l: One datatype KeyedLoc { KeyedLoc(l: Loc, k: K) } -pure procedure {:inline 1} KeyedLocs_New(ks: Set K) returns ({:pool "Loc_New"} l: Loc, {:linear} keyed_locs: Set (KeyedLoc K)) +pure procedure {:inline 1} KeyedLocSet_New(ks: Set K) returns ({:pool "Loc_New"} l: Loc, {:linear} keyed_locs: Set (KeyedLoc K)) { assume {:add_to_pool "Loc_New", l} true; keyed_locs := Set((lambda x: KeyedLoc K :: x->l == l && Set_Contains(ks, x->k))); diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 022370ebd..4db45658e 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -172,7 +172,7 @@ asserts Map_Contains(ts, loc_t); call one_loc_t, treiber := Map_Get(ts, loc_t); Treiber(top, stack) := treiber; assume loc_n is None || Map_Contains(stack, loc_n->t); - call loc, loc_pieces := KeyedLocs_New(AllLocPieces()); + call loc, loc_pieces := KeyedLocSet_New(AllLocPieces()); call left_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Left())); new_loc_n := left_loc_piece->val; call right_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Right())); @@ -191,7 +191,7 @@ refines AtomicAllocNode#3; var {:linear} left_loc_piece: One LocTreiberNode; call loc_n := ReadTopOfStack#Push(loc_t); - call loc, loc_pieces := KeyedLocs_New(AllLocPieces()); + call loc, loc_pieces := KeyedLocSet_New(AllLocPieces()); call left_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Left())); new_loc_n := left_loc_piece->val; call right_loc_piece := One_Get(loc_pieces, KeyedLoc(loc, Right())); From 2e39c89864f2c8e9d43576df1b0406f585e44993 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 1 Oct 2024 07:55:17 -0700 Subject: [PATCH 05/10] remove Cell_Pack and Cell_Unpack --- Source/Concurrency/LinearRewriter.cs | 10 ---------- Source/Concurrency/LinearTypeChecker.cs | 2 +- Source/Core/CivlAttributes.cs | 3 --- Source/Core/base.bpl | 14 ++----------- Test/civl/samples/alloc-mem.bpl | 26 ++++++++++++------------- 5 files changed, 16 insertions(+), 39 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index ede761988..9666d807f 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -151,8 +151,6 @@ public List RewriteCallCmd(CallCmd callCmd) { case "Loc_New": case "KeyedLocSet_New": - case "Cell_Pack": - case "Cell_Unpack": case "Set_MakeEmpty": case "Map_MakeEmpty": case "Map_Pack": @@ -269,14 +267,6 @@ 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 }; diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 2e3fb6aa8..d5f6ba8c5 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -871,7 +871,7 @@ public Type GetPermissionType(Type type) { var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl); var typeName = originalTypeCtorDecl.Name; - if (typeName == "Map" || typeName == "Set" || typeName == "Cell" | typeName == "One") + if (typeName == "Map" || typeName == "Set" || typeName == "One") { var actualTypeParams = program.monomorphizer.GetTypeInstantiation(datatypeTypeCtorDecl); return actualTypeParams[0]; diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index e110eb1d3..b8667e0f5 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -218,7 +218,6 @@ public static class CivlPrimitives public static HashSet LinearPrimitives = new() { "Loc_New", "KeyedLocSet_New", - "Cell_Pack", "Cell_Unpack", "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join", "Map_Get", "Map_Put", "Map_Assume", "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" }; @@ -245,8 +244,6 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) { case "Loc_New": case "KeyedLocSet_New": - case "Cell_Pack": - case "Cell_Unpack": case "Set_MakeEmpty": case "Map_MakeEmpty": case "Map_Pack": diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index c70cb59f2..cd3d482ea 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -290,11 +290,11 @@ function {:inline} One_Collector(a: One T): [T]bool } /// singleton map -datatype Cell { Cell(key: T, val: U) } +datatype Cell { Cell({:linear} key: One T, val: U) } function {:inline} Cell_Collector(a: Cell T U): [T]bool { - MapOne(a->key) + MapOne(a->key->val) } /// linear primitives @@ -309,16 +309,6 @@ 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} Cell_Pack({:linear_in} l: One K, {:linear_in} v: V) returns ({:linear} c: Cell K V) -{ - c := Cell(l->val, v); -} -pure procedure {:inline 1} Cell_Unpack({:linear_in} c: Cell K V) returns ({:linear} l: One K, {:linear} v: V) -{ - l := One(c->key); - v := c->val; -} - pure procedure {:inline 1} Map_MakeEmpty() returns ({:linear} m: Map K V) { m := Map_Empty(); diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl index 999327047..3f01b43f9 100644 --- a/Test/civl/samples/alloc-mem.bpl +++ b/Test/civl/samples/alloc-mem.bpl @@ -22,7 +22,7 @@ preserves call Yield(); yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in: Cell int int, i: int) preserves call Yield(); -requires {:layer 1,2} local_in->key == i; +requires {:layer 1,2} local_in->key == One(i); { var y, o: int; var {:layer 1,2} {:linear} local: Cell int int; @@ -54,7 +54,7 @@ yield procedure {:layer 1} Alloc() returns ({:layer 1} {:linear} l: Cell int int, i: int) refines atomic_Alloc; preserves call Yield(); -ensures {:layer 1} l->key == i; +ensures {:layer 1} l->key == One(i); { call i := PickAddr(); call {:layer 1} l, pool := AllocLinear(i, pool); @@ -65,13 +65,13 @@ modifies pool; { var {:linear} one_i: One int; var _v: int; - call one_i, _v := Cell_Unpack(l); + Cell(one_i, _v) := l; call One_Put(pool, one_i); } yield procedure {:layer 1} Free({:layer 1} {:linear_in} l: Cell int int, i: int) refines atomic_Free; -requires {:layer 1} l->key == i; +requires {:layer 1} l->key == One(i); preserves call Yield(); { call {:layer 1} pool := FreeLinear(l, i, pool); @@ -80,7 +80,7 @@ preserves call Yield(); both action {:layer 2} atomic_Read ({:linear} l: Cell int int, i: int) returns (o: int) { - assert l->key == i; + assert l->key == One(i); o := l->val; } @@ -89,8 +89,8 @@ both action {:layer 2} atomic_Write ({:linear_in} l: Cell int int, i: int, o: in { var {:linear} one_i: One int; var _v: int; - call one_i, _v := Cell_Unpack(l); - call l' := Cell_Pack(one_i, o); + Cell(one_i, _v) := l; + l' := Cell(one_i, o); } yield procedure {:layer 1} @@ -107,7 +107,7 @@ 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} l->key == i; +requires {:layer 1} l->key == One(i); ensures call YieldMem(l', i); { call WriteLow(i, o); @@ -121,7 +121,7 @@ pure action AllocLinear (i: int, {:linear_in} pool: Set int) var m: int; pool' := pool; call one_i := One_Get(pool', i); - call l := Cell_Pack(one_i, m); + l := Cell(one_i, m); } pure action FreeLinear ({:linear_in} l: Cell int int, i: int, {:linear_in} pool: Set int) @@ -129,7 +129,7 @@ pure action FreeLinear ({:linear_in} l: Cell int int, i: int, {:linear_in} pool: { var {:linear} one_i: One int; var _v: int; - call one_i, _v := Cell_Unpack(l); + Cell(one_i, _v) := l; pool' := pool; call One_Put(pool', one_i); } @@ -139,8 +139,8 @@ pure action WriteLinear ({:layer 1} {:linear_in} l: Cell int int, i: int, o: int { var {:linear} one_i: One int; var _v: int; - call one_i, _v := Cell_Unpack(l); - call l' := Cell_Pack(one_i, o); + Cell(one_i, _v) := l; + l' := Cell(one_i, o); } yield invariant {:layer 1} Yield (); @@ -148,7 +148,7 @@ invariant PoolInv(unallocated, pool); yield invariant {:layer 1} YieldMem ({:layer 1} {:linear} l: Cell int int, i: int); invariant PoolInv(unallocated, pool); -invariant l->key == i && l->val == mem[i]; +invariant l->key == One(i) && l->val == mem[i]; var {:layer 1, 2} {:linear} pool: Set int; var {:layer 0, 1} mem: [int]int; From 7d23bc0bd5cc59f04b5b46bda246c4152a34cb5c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 1 Oct 2024 10:07:58 -0700 Subject: [PATCH 06/10] small fix --- Source/Concurrency/LinearTypeChecker.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index d5f6ba8c5..e17df72a7 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -1077,7 +1077,7 @@ private void CheckType(Type type) return; } var typeCtorDeclName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name; - if (typeCtorDeclName == "Map" || typeCtorDeclName == "Cell") + if (typeCtorDeclName == "Map") { hasLinearStoreAccess = true; } From 7f54dea257196fa5aeb913bcd0631ebb40f0a578 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 1 Oct 2024 14:33:35 -0700 Subject: [PATCH 07/10] added support for no_collect_keys --- Source/Concurrency/LinearRewriter.cs | 49 +++++++++++++++- Source/Concurrency/LinearTypeChecker.cs | 76 ++++++++++++++++++++++++- Source/Core/CivlAttributes.cs | 4 +- Source/Core/base.bpl | 10 ++-- Test/civl/samples/treiber-stack.bpl | 48 +++++++--------- 5 files changed, 148 insertions(+), 39 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 9666d807f..d7b41a311 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -155,7 +155,6 @@ public List RewriteCallCmd(CallCmd callCmd) case "Map_MakeEmpty": case "Map_Pack": case "Map_Unpack": - case "Map_Assume": return new List{callCmd}; case "Set_Split": return RewriteSetSplit(callCmd); @@ -177,6 +176,10 @@ public List RewriteCallCmd(CallCmd callCmd) return RewriteMapGet(callCmd); case "Map_Put": return RewriteMapPut(callCmd); + case "Map_GetValue": + return RewriteMapGetValue(callCmd); + case "Map_PutValue": + return RewriteMapPutValue(callCmd); default: Contract.Assume(false); return null; @@ -481,6 +484,50 @@ private List RewriteMapPut(CallCmd callCmd) return cmdSeq; } + private List RewriteMapGetValue(CallCmd callCmd) + { + var cmdSeq = new List(); + var path = callCmd.Ins[0]; + var k = callCmd.Ins[1]; + var v = callCmd.Outs[0]; + + var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); + var domain = instantiation["K"]; + var range = instantiation["V"]; + var mapContainsFunc = MapContains(domain, range); + var mapRemoveFunc = MapRemove(domain, range); + var mapAtFunc = MapAt(domain, range); + cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(mapContainsFunc, path, k), "Map_GetValue failed")); + var oneConstructor = OneConstructor(domain); + cmdSeq.Add(CmdHelper.AssignCmd(v.Decl, ExprHelper.FunctionCall(mapAtFunc, path, k))); + cmdSeq.Add( + CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapRemoveFunc, path, k))); + + ResolveAndTypecheck(options, cmdSeq); + return cmdSeq; + } + + private List RewriteMapPutValue(CallCmd callCmd) + { + var cmdSeq = new List(); + var path = callCmd.Ins[0]; + var k = callCmd.Ins[1]; + var v = callCmd.Ins[2]; + + var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); + var domain = instantiation["K"]; + var range = instantiation["V"]; + 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, k)), attribute)); + cmdSeq.Add( + CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, k, v))); + + ResolveAndTypecheck(options, cmdSeq); + return cmdSeq; + } + private void ResolveAndTypecheck(CoreOptions options, IEnumerable absys) { var rc = new ResolutionContext(null, options); diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index e17df72a7..36a6e93f2 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -462,6 +462,10 @@ public override Cmd VisitAssignCmd(AssignCmd node) { Error(rhs, $"linear variable {rhs.Decl.Name} can occur at most once as the source of an assignment"); } + else if (InvalidAssignmentWithKeyCollection(lhs.DeepAssignedVariable, rhs.Decl)) + { + Error(rhs, $"Mismatch in key collection between source and target"); + } else { rhsVars.Add(rhs.Decl); @@ -486,6 +490,10 @@ public override Cmd VisitAssignCmd(AssignCmd node) { Error(arg, $"linear variable {ie.Decl.Name} can occur at most once as the source of an assignment"); } + else if (InvalidAssignmentWithKeyCollection(field, ie.Decl)) + { + Error(arg, $"Mismatch in key collection between source and target"); + } else { rhsVars.Add(ie.Decl); @@ -568,6 +576,11 @@ public override Cmd VisitCallCmd(CallCmd node) Error(node, $"linear variable {actual.Decl.Name} can occur only once as an input parameter"); continue; } + if (!isPrimitive && InvalidAssignmentWithKeyCollection(formal, actual.Decl)) + { + Error(node, $"Mismatch in key collection between source and target"); + continue; + } inVars.Add(actual.Decl); if (actual.Decl is GlobalVariable && actualKind == LinearKind.LINEAR_IN) { @@ -590,6 +603,11 @@ public override Cmd VisitCallCmd(CallCmd node) Error(node, $"only linear parameter can be assigned to a linear variable: {formal}"); continue; } + if (!isPrimitive && InvalidAssignmentWithKeyCollection(actual.Decl, formal)) + { + Error(node, $"Mismatch in key collection between source and target"); + continue; + } } var globalOutVars = node.Outs.Select(ie => ie.Decl).ToHashSet(); @@ -598,6 +616,8 @@ public override Cmd VisitCallCmd(CallCmd node) Error(node, $"global variable passed as input to pure call but not received as output: {v}"); }); + var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(node.Proc); + if (isPrimitive) { var modifiedArgument = CivlPrimitives.ModifiedArgument(node)?.Decl; @@ -612,17 +632,48 @@ public override Cmd VisitCallCmd(CallCmd node) Error(node, $"primitive assigns to input variable that is also an output variable: {modifiedArgument}"); } else if (modifiedArgument is GlobalVariable && - enclosingProc is not YieldProcedureDecl && - enclosingProc.Modifies.All(v => v.Decl != modifiedArgument)) + enclosingProc is not YieldProcedureDecl && + enclosingProc.Modifies.All(v => v.Decl != modifiedArgument)) { var str = enclosingProc is ActionDecl ? "action's" : "procedure's"; Error(node, $"primitive assigns to a global variable that is not in the enclosing {str} modifies clause: {modifiedArgument}"); } + + if (originalProc.Name == "Map_Split") + { + if (InvalidAssignmentWithKeyCollection(node.Outs[0].Decl, modifiedArgument)) + { + Error(node, $"Mismatch in key collection between source and target"); + } + } + else if (originalProc.Name == "Map_Join") + { + if (node.Ins[1] is IdentifierExpr ie) + { + if (InvalidAssignmentWithKeyCollection(modifiedArgument, ie.Decl)) + { + Error(node, $"Mismatch in key collection between source and target"); + } + } + } + else if (originalProc.Name == "Map_Get" || originalProc.Name == "Map_Put") + { + if (!AreKeysCollected(modifiedArgument)) + { + Error(node, $"Keys must be collected"); + } + } + else if (originalProc.Name == "Map_GetValue" || originalProc.Name == "Map_PutValue") + { + if (AreKeysCollected(modifiedArgument)) + { + Error(node, $"Keys must not be collected"); + } + } } } - var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(node.Proc); if (originalProc.Name == "create_multi_asyncs" || originalProc.Name == "create_asyncs") { var actionDecl = GetActionDeclFromCreateAsyncs(node); @@ -749,6 +800,25 @@ public override Variable VisitVariable(Variable node) return node; } + private bool AreKeysCollected(Variable v) + { + var attr = QKeyValue.FindAttribute(v.Attributes, x => x.Key == "linear"); + var attrParams = attr == null ? new List() : attr.Params; + foreach (var param in attrParams) + { + if (param is string s && s == "no_collect_keys") + { + return false; + } + } + return true; + } + + private bool InvalidAssignmentWithKeyCollection(Variable target, Variable source) + { + return AreKeysCollected(target) && !AreKeysCollected(source); + } + private void CheckLinearStoreAccessInGuards() { program.Implementations.ForEach(impl => { diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index b8667e0f5..3e3ff4bc5 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -218,7 +218,8 @@ public static class CivlPrimitives public static HashSet LinearPrimitives = new() { "Loc_New", "KeyedLocSet_New", - "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join", "Map_Get", "Map_Put", "Map_Assume", + "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join", + "Map_Get", "Map_Put", "Map_GetValue", "Map_PutValue", "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" }; @@ -248,7 +249,6 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) case "Map_MakeEmpty": case "Map_Pack": case "Map_Unpack": - case "Map_Assume": return null; default: return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index cd3d482ea..5185f5a43 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -319,17 +319,15 @@ pure procedure {:inline 1} Map_Pack({:linear_in} dom: Set K, val: [K]V) ret } pure procedure {:inline 1} Map_Unpack({:linear_in} m: Map K V) returns ({:linear} dom: Set K, val: [K]V) { - dom := m->dom; - val := m->val; + dom := m->dom; + val := m->val; } pure procedure Map_Split({:linear} path: Map K V, s: Set K) returns ({:linear} m: Map K V); pure procedure Map_Join({:linear} path: Map K V, {:linear_in} m: Map K 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 {:inline 1} Map_Assume({:linear} src: Map K V, {:linear} dst: Map K V) -{ - assume Set_IsDisjoint(src->dom, dst->dom); -} +pure procedure Map_GetValue({:linear} path: Map K V, k: K) returns ({:linear} v: V); +pure procedure Map_PutValue({:linear} path: Map K V, k: K, {:linear_in} v: V); type Loc; diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 4db45658e..b9a03d881 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -14,7 +14,7 @@ datatype Treiber { Treiber(top: Option LocTreiberNode, {:linear} stack: Stack 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 0, 4} {:linear "no_collect_keys"} ts: Map Loc (Treiber X); /// Yield invariants @@ -61,31 +61,31 @@ invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !Betw /// Layered implementation -atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc) +atomic action {:layer 5} AtomicAlloc() returns ({:linear} one_loc_t: One Loc) modifies Stack; { - var {:linear} one_loc_t: One Loc; + var loc_t: 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()); } -yield procedure {:layer 4} Alloc() returns (loc_t: Loc) +yield procedure {:layer 4} Alloc() returns ({:linear} one_loc_t: One Loc) refines AtomicAlloc; preserves call StackDom(); { var top: Option LocTreiberNode; var {:linear} stack: StackMap X; var {:linear} treiber: Treiber X; - var {:linear} one_loc_t: One Loc; + var loc_t: Loc; top := None(); call stack := Map_MakeEmpty(); treiber := Treiber(top, stack); call one_loc_t := Loc_New(); loc_t := one_loc_t->val; - call AllocTreiber#0(one_loc_t, treiber); + call AllocTreiber#0(loc_t, treiber); call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty())); call {:layer 4} AbsLemma(treiber); } @@ -161,7 +161,6 @@ atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc, x: X) modifies ts; asserts Map_Contains(ts, loc_t); { - var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; var top: Option LocTreiberNode; var {:linear} stack: StackMap X; @@ -169,7 +168,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 treiber := Map_GetValue(ts, 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 +177,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_PutValue(ts, 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) @@ -201,7 +200,6 @@ refines AtomicAllocNode#3; atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc) returns (success: bool, x_opt: Option X) modifies ts; { - var {:linear} one_loc_t: One Loc; var loc_n: Option LocTreiberNode; var {:linear} treiber: Treiber X; var top: Option LocTreiberNode; @@ -210,12 +208,12 @@ modifies ts; assert Map_Contains(ts, loc_t); if (*) { - call one_loc_t, treiber := Map_Get(ts, loc_t); + call treiber := Map_GetValue(ts, 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_PutValue(ts, loc_t, treiber); x_opt := Some(x); success := true; } @@ -293,18 +291,17 @@ atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) ret modifies ts; refines AtomicLoadNode#1; { - var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; var top: Option LocTreiberNode; var {:linear} stack: StackMap X; var {:linear} one_loc_n: One LocTreiberNode; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call treiber := Map_GetValue(ts, 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_PutValue(ts, loc_t, treiber); } yield procedure {:layer 0} LoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) returns (node: StackElem X); refines AtomicLoadNode#0; @@ -312,12 +309,11 @@ refines AtomicLoadNode#0; atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode) modifies ts; { - var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call treiber := Map_GetValue(ts, loc_t); loc_n := treiber->top; - call Map_Put(ts, one_loc_t, treiber); + call Map_PutValue(ts, loc_t, treiber); } yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode); refines AtomicReadTopOfStack#0; @@ -327,16 +323,15 @@ atomic action {:layer 1,4} AtomicWriteTopOfStack#0( modifies ts; { var {:linear} treiber: Treiber X; - var {:linear} one_loc_t: One Loc; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call treiber := Map_GetValue(ts, 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_PutValue(ts, 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); @@ -345,22 +340,21 @@ refines AtomicWriteTopOfStack#0; atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X) modifies ts; { - var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call one_loc_t, treiber := Map_Get(ts, loc_t); + call treiber := Map_GetValue(ts, loc_t); call Map_Put(treiber->stack, loc_piece, node); - call Map_Put(ts, one_loc_t, treiber); + call Map_PutValue(ts, 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) +atomic action {:layer 1,4} AtomicAllocTreiber#0(loc_t: Loc, {:linear_in} treiber: Treiber X) modifies ts; { - call Map_Put(ts, one_loc_t, treiber); + call Map_PutValue(ts, loc_t, treiber); } -yield procedure {:layer 0} AllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X); +yield procedure {:layer 0} AllocTreiber#0(loc_t: Loc, {:linear_in} treiber: Treiber X); refines AtomicAllocTreiber#0; /// Proof of abstraction with a manual encoding of termination From b0e37024f0506cf489c4cc837162dcaec1175598 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 1 Oct 2024 14:51:49 -0700 Subject: [PATCH 08/10] do not collect keys fix --- Source/Concurrency/LinearTypeChecker.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 36a6e93f2..f575db40d 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -1045,6 +1045,7 @@ private IEnumerable FilterVariables(LinearDomain domain, IEnumerable FindLinearKind(v) != LinearKind.ORDINARY && + AreKeysCollected(v) && collectors.ContainsKey(v.TypedIdent.Type) && collectors[v.TypedIdent.Type].ContainsKey(domain.permissionType)); } From 4b609cd9ee0084ddd9d735a306a8869ff499a0c0 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Wed, 2 Oct 2024 10:31:17 -0700 Subject: [PATCH 09/10] rolled back no_collect_keys --- Source/Concurrency/LinearRewriter.cs | 2 -- Test/civl/samples/treiber-stack.bpl | 48 ++++++++++++++++------------ 2 files changed, 27 insertions(+), 23 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index d7b41a311..b7669f65e 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -519,8 +519,6 @@ private List RewriteMapPutValue(CallCmd callCmd) var range = instantiation["V"]; 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, k)), attribute)); cmdSeq.Add( CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, k, v))); diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index b9a03d881..44008baa2 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -14,7 +14,7 @@ datatype Treiber { Treiber(top: Option LocTreiberNode, {:linear} stack: Stack type X; // module type parameter var {:layer 4, 5} Stack: Map Loc (Vec X); -var {:layer 0, 4} {:linear "no_collect_keys"} ts: Map Loc (Treiber X); +var {:layer 0, 4} {:linear} ts: Map Loc (Treiber X); /// Yield invariants @@ -61,31 +61,31 @@ invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !Betw /// Layered implementation -atomic action {:layer 5} AtomicAlloc() returns ({:linear} one_loc_t: One Loc) +atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc) modifies Stack; { - var loc_t: Loc; + 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()); } -yield procedure {:layer 4} Alloc() returns ({:linear} one_loc_t: One Loc) +yield procedure {:layer 4} Alloc() returns (loc_t: Loc) refines AtomicAlloc; preserves call StackDom(); { var top: Option LocTreiberNode; var {:linear} stack: StackMap X; var {:linear} treiber: Treiber X; - var loc_t: Loc; + var {:linear} one_loc_t: One Loc; top := None(); call stack := Map_MakeEmpty(); treiber := Treiber(top, stack); call one_loc_t := Loc_New(); loc_t := one_loc_t->val; - call AllocTreiber#0(loc_t, treiber); + call AllocTreiber#0(one_loc_t, treiber); call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty())); call {:layer 4} AbsLemma(treiber); } @@ -161,6 +161,7 @@ atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc, x: X) modifies ts; asserts Map_Contains(ts, loc_t); { + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; var top: Option LocTreiberNode; var {:linear} stack: StackMap X; @@ -168,7 +169,7 @@ asserts Map_Contains(ts, loc_t); var {:linear} loc_pieces: Set LocTreiberNode; var {:linear} left_loc_piece: One LocTreiberNode; - call treiber := Map_GetValue(ts, loc_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); Treiber(top, stack) := treiber; assume loc_n is None || Map_Contains(stack, loc_n->t); call loc, loc_pieces := KeyedLocSet_New(AllLocPieces()); @@ -177,7 +178,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_PutValue(ts, loc_t, treiber); + call Map_Put(ts, 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) @@ -200,6 +201,7 @@ refines AtomicAllocNode#3; atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc) returns (success: bool, x_opt: Option X) modifies ts; { + var {:linear} one_loc_t: One Loc; var loc_n: Option LocTreiberNode; var {:linear} treiber: Treiber X; var top: Option LocTreiberNode; @@ -208,12 +210,12 @@ modifies ts; assert Map_Contains(ts, loc_t); if (*) { - call treiber := Map_GetValue(ts, loc_t); + call one_loc_t, treiber := Map_Get(ts, 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_PutValue(ts, loc_t, treiber); + call Map_Put(ts, one_loc_t, treiber); x_opt := Some(x); success := true; } @@ -291,17 +293,18 @@ atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) ret modifies ts; refines AtomicLoadNode#1; { + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; var top: Option LocTreiberNode; var {:linear} stack: StackMap X; var {:linear} one_loc_n: One LocTreiberNode; - call treiber := Map_GetValue(ts, loc_t); + call one_loc_t, treiber := Map_Get(ts, 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_PutValue(ts, loc_t, treiber); + call Map_Put(ts, one_loc_t, treiber); } yield procedure {:layer 0} LoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) returns (node: StackElem X); refines AtomicLoadNode#0; @@ -309,11 +312,12 @@ refines AtomicLoadNode#0; atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode) modifies ts; { + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call treiber := Map_GetValue(ts, loc_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); loc_n := treiber->top; - call Map_PutValue(ts, loc_t, treiber); + call Map_Put(ts, one_loc_t, treiber); } yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode); refines AtomicReadTopOfStack#0; @@ -322,16 +326,17 @@ 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; { + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call treiber := Map_GetValue(ts, loc_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); if (old_loc_n == treiber->top) { treiber->top := new_loc_n; success := true; } else { success := false; } - call Map_PutValue(ts, loc_t, treiber); + call Map_Put(ts, 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); @@ -340,21 +345,22 @@ refines AtomicWriteTopOfStack#0; atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X) modifies ts; { + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - call treiber := Map_GetValue(ts, loc_t); + call one_loc_t, treiber := Map_Get(ts, loc_t); call Map_Put(treiber->stack, loc_piece, node); - call Map_PutValue(ts, loc_t, treiber); + call Map_Put(ts, 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(loc_t: Loc, {:linear_in} treiber: Treiber X) +atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X) modifies ts; { - call Map_PutValue(ts, loc_t, treiber); + call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} AllocTreiber#0(loc_t: Loc, {:linear_in} treiber: Treiber X); +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 From 129af19ecabd2c228f0e4f2b38b6ae24d81747b3 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 7 Oct 2024 09:25:54 -0700 Subject: [PATCH 10/10] added a test --- Source/Concurrency/LinearTypeChecker.cs | 25 ++-- .../civl/regression-tests/no-collect-keys.bpl | 108 ++++++++++++++++++ .../no-collect-keys.bpl.expect | 13 +++ 3 files changed, 138 insertions(+), 8 deletions(-) create mode 100644 Test/civl/regression-tests/no-collect-keys.bpl create mode 100644 Test/civl/regression-tests/no-collect-keys.bpl.expect diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index f575db40d..812616bf8 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -515,9 +515,14 @@ public override Cmd VisitUnpackCmd(UnpackCmd node) continue; } isLinearUnpack = true; - if (FindLinearKind(node.Constructor.InParams[j]) == LinearKind.ORDINARY) + var field = node.Constructor.InParams[j]; + if (FindLinearKind(field) == LinearKind.ORDINARY) { - Error(unpackedLhs[j], $"source of unpack must be linear field: {node.Constructor.InParams[j]}"); + Error(unpackedLhs[j], $"source of unpack must be linear field: {field}"); + } + else if (InvalidAssignmentWithKeyCollection(unpackedLhs[j].Decl, field)) + { + Error(unpackedLhs[j], $"Mismatch in key collection between source and target"); } } if (isLinearUnpack) @@ -644,17 +649,14 @@ enclosingProc is not YieldProcedureDecl && { if (InvalidAssignmentWithKeyCollection(node.Outs[0].Decl, modifiedArgument)) { - Error(node, $"Mismatch in key collection between source and target"); + Error(node.Outs[0], $"Mismatch in key collection between source and target"); } } else if (originalProc.Name == "Map_Join") { - if (node.Ins[1] is IdentifierExpr ie) + if (node.Ins[1] is IdentifierExpr ie && InvalidAssignmentWithKeyCollection(modifiedArgument, ie.Decl)) { - if (InvalidAssignmentWithKeyCollection(modifiedArgument, ie.Decl)) - { - Error(node, $"Mismatch in key collection between source and target"); - } + Error(node.Ins[1], $"Mismatch in key collection between source and target"); } } else if (originalProc.Name == "Map_Get" || originalProc.Name == "Map_Put") @@ -672,6 +674,13 @@ enclosingProc is not YieldProcedureDecl && } } } + else if (originalProc.Name == "Map_Unpack") + { + if (node.Ins[0] is IdentifierExpr ie && !AreKeysCollected(ie.Decl)) + { + Error(node.Ins[0], $"Mismatch in key collection between source and target"); + } + } } if (originalProc.Name == "create_multi_asyncs" || originalProc.Name == "create_asyncs") diff --git a/Test/civl/regression-tests/no-collect-keys.bpl b/Test/civl/regression-tests/no-collect-keys.bpl new file mode 100644 index 000000000..99986c6df --- /dev/null +++ b/Test/civl/regression-tests/no-collect-keys.bpl @@ -0,0 +1,108 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var {:linear "no_collect_keys"} {:layer 0,1} g: Map int int; +var {:linear} {:layer 0,1} h: Map int int; + +atomic action {:layer 1} A() +modifies g, h; +{ + var {:linear} l: Map int int; + var {:linear "no_collect_keys"} m: Map int int; + l := h; + h := l; + m := g; + g := m; +} + +atomic action {:layer 1} B() { + var {:linear} l: Map int int; + var {:linear "no_collect_keys"} m: Map int int; + l := g; + m := h; +} + +atomic action {:layer 1} X1({:linear "no_collect_keys"} a: Map int int) +{ + +} + +atomic action {:layer 1} Y1() +{ + var {:linear} l: Map int int; + call l := Map_MakeEmpty(); + call X1(l); +} + +atomic action {:layer 1} X2({:linear } a: Map int int) +{ + +} + +atomic action {:layer 1} Y2() +{ + var {:linear "no_collect_keys"} l: Map int int; + call l := Map_MakeEmpty(); + call X2(l); +} + +atomic action {:layer 1} X3() returns ({:linear "no_collect_keys"} a: Map int int) +{ + call a := Map_MakeEmpty(); +} + +atomic action {:layer 1} Y3() +{ + var {:linear} l: Map int int; + call l := X3(); +} + +atomic action {:layer 1} X4() returns ({:linear} a: Map int int) +{ + call a := Map_MakeEmpty(); +} + +datatype D { D({:linear "no_collect_keys"} d: Map int int) } + +datatype E { E({:linear} e: Map int int) } + +atomic action {:layer 1} Y4() +{ + var {:linear "no_collect_keys"} l: Map int int; + var {:linear} l': Map int int; + var {:linear} d: D; + var {:linear "no_collect_keys"} e: E; + + call l := X4(); + d := D(l); + D(l) := d; + + call l' := Map_MakeEmpty(); + d := D(l'); + D(l') := d; + + e := E(l'); + e := E(l); +} + +atomic action {:layer 1} C() { + var {:linear "no_collect_keys"} l: Map int int; + var {:linear} l': Map int int; + var {:linear} s: Set int; + var m: [int]int; + var {:linear} one_int: One int; + var i: int; + + call l := Map_MakeEmpty(); + call l' := Map_MakeEmpty(); + + call s, m := Map_Unpack(l); + call one_int, i := Map_Get(l, 0); + call Map_Put(l, one_int, i); + call i := Map_GetValue(l', 0); + call Map_PutValue(l', 0, i); + call l' := Map_Split(l, s); + call Map_Join(l', l); + call l := Map_Split(l', s); + call Map_Join(l, l'); +} \ No newline at end of file diff --git a/Test/civl/regression-tests/no-collect-keys.bpl.expect b/Test/civl/regression-tests/no-collect-keys.bpl.expect new file mode 100644 index 000000000..30a20fa2d --- /dev/null +++ b/Test/civl/regression-tests/no-collect-keys.bpl.expect @@ -0,0 +1,13 @@ +no-collect-keys.bpl(21,9): Error: Mismatch in key collection between source and target +no-collect-keys.bpl(46,4): Error: Mismatch in key collection between source and target +no-collect-keys.bpl(57,4): Error: Mismatch in key collection between source and target +no-collect-keys.bpl(82,6): Error: Mismatch in key collection between source and target +no-collect-keys.bpl(85,11): Error: Mismatch in key collection between source and target +no-collect-keys.bpl(99,28): Error: Mismatch in key collection between source and target +no-collect-keys.bpl(100,4): Error: Keys must be collected +no-collect-keys.bpl(101,4): Error: Keys must be collected +no-collect-keys.bpl(102,4): Error: Keys must not be collected +no-collect-keys.bpl(103,4): Error: Keys must not be collected +no-collect-keys.bpl(104,9): Error: Mismatch in key collection between source and target +no-collect-keys.bpl(105,22): Error: Mismatch in key collection between source and target +12 type checking errors detected in no-collect-keys.bpl