Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Civl] Eliminate type parameter of Loc #954

Merged
merged 4 commits into from
Sep 30, 2024
Merged

[Civl] Eliminate type parameter of Loc #954

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8fdbf37
first commit
shazqadeer Sep 28, 2024
2ac8979
updates
shazqadeer Sep 28, 2024
84cae94
removed a lambda
shazqadeer Sep 28, 2024
0b67dec
update
shazqadeer Sep 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlTypeChecker.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -298,8 +298,8 @@ private void InlineAtomicActions(HashSet<ActionDecl> actionDecls)
{
var primitiveImpls = program.TopLevelDeclarations.OfType<Implementation>().Where(impl =>
{
var originalDecl = impl.Proc.OriginalDeclWithFormals;
return originalDecl != null && CivlPrimitives.LinearPrimitives.Contains(originalDecl.Name);
var originalDecl = Monomorphizer.GetOriginalDecl(impl);
return CivlPrimitives.LinearPrimitives.Contains(originalDecl.Name);
});
primitiveImpls.ForEach(impl => {
impl.OriginalBlocks = impl.Blocks;
Expand Down
4 changes: 2 additions & 2 deletions Source/Core/base.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -358,9 +358,9 @@ pure procedure {:inline 1} Map_Assume<K,V>({:linear} src: Map K V, {:linear} dst
assume Set_IsDisjoint(src->dom, dst->dom);
}

type Loc _;
type Loc;

pure procedure {:inline 1} One_New<V>() returns ({:linear} {:pool "One_New"} l: One (Loc V))
pure procedure {:inline 1} One_New() returns ({:linear} {:pool "One_New"} l: One Loc)
{
assume {:add_to_pool "One_New", l} true;
}
Expand Down
70 changes: 40 additions & 30 deletions Test/civl/inductive-sequentialization/distributed-snapshot.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %parallel-boogie "%s" > "%t"
// RUN: %parallel-boogie /vcsSplitOnEveryAssert "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

type Value;
Expand All @@ -10,7 +10,7 @@ datatype StampedValue {
}

type Channel; // Send + Receive
type ChannelPiece = Fraction (Loc Channel) ChannelOp; // Send or Receive piece
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;
Expand All @@ -37,53 +37,61 @@ function {:inline} IsSendSecond(piece: ChannelPiece): bool {
piece == Fraction(piece->val, SendSecond(), ChannelOps())
}

function {:inline} ToReceive(loc_channel: Loc Channel): ChannelPiece {
function {:inline} ToReceive(loc_channel: Loc): ChannelPiece {
Fraction(loc_channel, Receive(), ChannelOps())
}

function {:inline} ToSendFirst(loc_channel: Loc Channel): ChannelPiece {
function {:inline} ToSendFirst(loc_channel: Loc): ChannelPiece {
Fraction(loc_channel, SendFirst(), ChannelOps())
}

function {:inline} ToSendSecond(loc_channel: Loc Channel): ChannelPiece {
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))
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} MemIndices(): Set int {
Set((lambda {:pool "MemIndices"} x: int :: 1 <= x && x <= NumMemIndices))
}

function {:inline} IsValidMemIndexPiece(piece: MemIndexPiece): bool {
Set_Contains(piece->ids, piece->id) &&
piece->ids == MemIndices()
piece->ids == MemIndices
}

function {:inline} MemIndexPiece(cp: ChannelPiece, i: int): MemIndexPiece
{
Fraction(cp, i, MemIndices())
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({:linear_in} one_loc_channel: One (Loc Channel)) returns (snapshot: [int]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({:linear_in} one_loc_channel: One (Loc Channel)) returns (snapshot: [int]StampedValue)
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;
Expand All @@ -92,12 +100,13 @@ refines GetSnapshot;
var {:linear} sps_second: Set MemIndexPiece;
var snapshot': Snapshot;

call one_loc_channel := One_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());
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;
Expand Down Expand Up @@ -135,7 +144,7 @@ asserts 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())]);
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;
Expand All @@ -155,7 +164,7 @@ asserts IsSendFirst(s) || IsSendSecond(s);
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())]);
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;
Expand All @@ -179,7 +188,7 @@ asserts sps == AllMemIndexPieces(s);
var {:linear} map: Map MemIndexPiece StampedValue;

assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true;
assume (forall i: int :: 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i]));
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);
}
Expand All @@ -193,7 +202,7 @@ 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((lambda pa: read_f :: Set_Contains(sps, pa->perm->val)));
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;
Expand Down Expand Up @@ -231,18 +240,18 @@ asserts sps == AllMemIndexPieces(s);
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 i: int :: 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i]));

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())));
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((lambda {:pool "Read_PAs"} pa: read_f :: Set_Contains(sps', pa->perm->val)));
call {:linear sps'} create_asyncs((Read_f_asyncs(sps')));
}
}

Expand All @@ -257,7 +266,7 @@ asserts sps == AllMemIndexPieces(s);
var {:linear} map: Map MemIndexPiece StampedValue;

assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true;
assume (forall i: int :: 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i]));
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);
}
Expand All @@ -271,7 +280,7 @@ 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((lambda pa: read_s :: Set_Contains(sps, pa->perm->val)));
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;
Expand Down Expand Up @@ -307,17 +316,18 @@ asserts sps == AllMemIndexPieces(s);
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 i: int :: 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i]));
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())));
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((lambda {:pool "Read_PAs"} pa: read_s :: Set_Contains(sps', pa->perm->val)));
call {:linear sps'} create_asyncs(Read_s_asyncs(sps'));
}
}
}
33 changes: 0 additions & 33 deletions Test/civl/regression-tests/is2-attributes.bpl
View file
Open in desktop

This file was deleted.

2 changes: 0 additions & 2 deletions Test/civl/regression-tests/is2-attributes.bpl.expect
View file
Open in desktop

This file was deleted.

2 changes: 1 addition & 1 deletion Test/civl/regression-tests/pa-noninterference-check.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
pa-noninterference-check.bpl(26,1): Error: Non-interference check failed
Execution trace:
pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Entry
(0,0): init
pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0
pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return

Expand Down
2 changes: 1 addition & 1 deletion Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed
Execution trace:
pending-async-noninterference-fail.bpl(9,32): inline$A$0$Entry
(0,0): init
pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0
pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return

Expand Down
Loading
Loading