Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer committed Jan 3, 2024
1 parent ca1e3fc commit 37f081f
Show file tree
Hide file tree
Showing 5 changed files with 138 additions and 127 deletions.
59 changes: 36 additions & 23 deletions Source/Core/base.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -225,29 +225,48 @@ datatype Map<T,U> {
Map(dom: Set T, val: [T]U)
}

function {:inline} Map_Empty<T,U>(): Map T U
{
Map(Set(MapConst(false)), MapConst(Default()))
}

function {:inline} Map_Singleton<T,U>(t: T, u: U): Map T U
{
Map_Update(Map_Empty(), t, u)
}

function {:inline} Map_Contains<T,U>(a: Map T U, t: T): bool
{
Set_Contains(a->dom, t)
Set_Contains(a->dom, t)
}

function {:inline} Map_IsDisjoint<T,U>(a: Map T U, b: Map T U): bool
{
Set_IsDisjoint(a->dom, b->dom)
}

function {:inline} Map_At<T,U>(a: Map T U, t: T): U
{
a->val[t]
a->val[t]
}

function {:inline} Map_Remove<T,U>(a: Map T U, t: T): Map T U
{
Map(Set_Remove(a->dom, t), a->val[t := Default()])
Map(Set_Remove(a->dom, t), a->val[t := Default()])
}

function {:inline} Map_Update<T,U>(a: Map T U, t: T, u: U): Map T U
{
Map(Set_Add(a->dom, t), a->val[t := u])
Map(Set_Add(a->dom, t), a->val[t := u])
}

function {:inline} Map_Swap<T,U>(a: Map T U, t1: T, t2: T): Map T U
{
(var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1))
(var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1))
}

function {:inline} Map_WellFormed<K,V>(a: Map K V): bool {
a->val == MapIte(a->dom->val, a->val, MapConst(Default()))
}

/// linear maps
Expand All @@ -260,43 +279,37 @@ datatype Ref<V> {
Nil()
}

datatype Lmap<K,V> { Lmap(dom: [K]bool, val: [K]V) }
datatype Lmap<K,V> { Lmap(val: Map K V) }
type Lheap V = Lmap (Ref V) V;

function {:inline} Lmap_WellFormed<K,V>(l: Lmap K V): bool {
l->val == MapIte(l->dom, l->val, MapConst(Default()))
Map_WellFormed(l->val)
}
function {:inline} Lmap_Collector<K,V>(l: Lmap K V): [K]bool {
l->dom
}
function {:inline} Lmap_Contains<K,V>(l: Lmap K V, k: K): bool {
l->dom[k]
}
function {:inline} Lmap_Deref<K,V>(l: Lmap K V, k: K): V {
l->val[k]
l->val->dom->val
}
pure procedure {:inline 1} Lmap_Empty<K,V>() returns (l: Lmap K V) {
l := Lmap(MapConst(false), MapConst(Default()));
l := Lmap(Map_Empty());
}
pure procedure {:inline 1} Lmap_Alloc<V>(v: V) returns (k: Lval (Loc V), l: Lmap (Ref V) V) {
var r: Ref V;
r := Ref(k->val);
l := Lmap(MapOne(r), MapConst(Default())[r := v]);
l := Lmap(Map_Singleton(r, v));
}
pure procedure {:inline 1} Lmap_Create<K,V>({:linear_in} k: Lset K, val: [K]V) returns (l: Lmap K V) {
l := Lmap(k->dom, val);
l := Lmap(Map(Set(k->dom), val));
}
pure procedure {:inline 1} Lmap_Free<K,V>({:linear_in} l: Lmap K V) returns (k: Lset K) {
k := Lset(l->dom);
k := Lset(l->val->dom->val);
}
pure procedure {:inline 1} Lmap_Move<K,V>({:linear_in} src: Lmap K V, dst: Lmap K V, k: K) returns (src': Lmap K V, dst': Lmap K V) {
assert src->dom[k];
assert IsDisjoint(src->dom, dst->dom);
dst' := Lmap(dst->dom[k := true], dst->val[k := src->val[k]]);
src' := Lmap(src->dom[k := false], src->val[k := Default()]);
assert Map_Contains(src->val, k);
assert Map_IsDisjoint(src->val, dst->val);
dst' := Lmap(Map_Update(dst->val, k, Map_At(src->val, k)));
src' := Lmap(Map_Remove(src->val, k));
}
pure procedure {:inline 1} Lmap_Assume<K,V>(src: Lmap K V, dst: Lmap K V) {
assume IsDisjoint(src->dom, dst->dom);
assume Map_IsDisjoint(src->val, dst->val);
}

/// linear sets
Expand Down
26 changes: 13 additions & 13 deletions Test/civl/samples/alloc-mem.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ preserves call Yield();

yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in:Lmap int int, i:int)
preserves call Yield();
requires {:layer 1,2} Lmap_Contains(local_in, i);
requires {:layer 1,2} Map_Contains(local_in->val, i);
{
var y, o:int;
var {:layer 1,2} local:Lmap int int;
Expand Down Expand Up @@ -54,7 +54,7 @@ yield procedure {:layer 1}
Alloc() returns ({:layer 1} l:Lmap int int, i:int)
refines atomic_Alloc;
preserves call Yield();
ensures {:layer 1} Lmap_Contains(l, i);
ensures {:layer 1} Map_Contains(l->val, i);
{
call i := PickAddr();
call {:layer 1} l, pool := AllocLinear(i, pool);
Expand All @@ -64,14 +64,14 @@ left action {:layer 2} atomic_Free({:linear_in} l:Lmap int int, i:int)
modifies pool;
{
var t:Lset int;
assert Lmap_Contains(l, i);
assert Map_Contains(l->val, i);
call t := Lmap_Free(l);
call Lset_Put(pool, t);
}

yield procedure {:layer 1} Free({:layer 1} {:linear_in} l:Lmap int int, i:int)
refines atomic_Free;
requires {:layer 1} Lmap_Contains(l, i);
requires {:layer 1} Map_Contains(l->val, i);
preserves call Yield();
{
call {:layer 1} pool := FreeLinear(l, i, pool);
Expand All @@ -80,15 +80,15 @@ preserves call Yield();

both action {:layer 2} atomic_Read (l:Lmap int int, i:int) returns (o:int)
{
assert Lmap_Contains(l, i);
o := l->val[i];
assert Map_Contains(l->val, i);
o := l->val->val[i];
}

both action {:layer 2} atomic_Write ({:linear_in} l:Lmap int int, i:int, o:int) returns (l':Lmap int int)
{
assert Lmap_Contains(l, i);
assert Map_Contains(l->val, i);
l' := l;
l'->val[i] := o;
l'->val->val[i] := o;
}

yield procedure {:layer 1}
Expand All @@ -104,7 +104,7 @@ yield procedure {:layer 1}
Write ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int)
refines atomic_Write;
requires call Yield();
requires {:layer 1} Lmap_Contains(l, i);
requires {:layer 1} Map_Contains(l->val, i);
ensures call YieldMem(l', i);
{
call WriteLow(i, o);
Expand All @@ -124,25 +124,25 @@ pure action AllocLinear (i:int, {:linear_in} pool:Lset int) returns (l:Lmap int
pure action FreeLinear ({:linear_in} l:Lmap int int, i:int, {:linear_in} pool:Lset int) returns (pool':Lset int)
{
var t: Lset int;
assert Lmap_Contains(l, i);
assert Map_Contains(l->val, i);
call t := Lmap_Free(l);
pool' := pool;
call Lset_Put(pool', t);
}

pure action WriteLinear ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int)
{
assert Lmap_Contains(l, i);
assert Map_Contains(l->val, i);
l' := l;
l'->val[i] := o;
l'->val->val[i] := o;
}

yield invariant {:layer 1} Yield ();
invariant PoolInv(unallocated, pool);

yield invariant {:layer 1} YieldMem ({:layer 1} l:Lmap int int, i:int);
invariant PoolInv(unallocated, pool);
invariant Lmap_Contains(l, i) && Lmap_Deref(l, i) == mem[i];
invariant Map_Contains(l->val, i) && Map_At(l->val, i) == mem[i];

var {:layer 1, 2} pool:Lset int;
var {:layer 0, 1} mem:[int]int;
Expand Down
6 changes: 3 additions & 3 deletions Test/civl/samples/civl-paper.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ yield invariant {:layer 1} InvLock();
invariant lock != nil <==> b;

yield invariant {:layer 3} InvMem();
invariant g->dom[p] && g->dom[p+4] && g->val[p] == g->val[p+4];
invariant Map_Contains(g->val, p) && Map_Contains(g->val, p+4) && Map_At(g->val, p) == Map_At(g->val, p+4);

yield procedure {:layer 3} P(tid: Lval X)
requires {:layer 1,3} tid->val != nil;
Expand Down Expand Up @@ -130,13 +130,13 @@ yield procedure {:layer 0} TransferFromGlobal(tid: Lval X) returns (l: Lmap int
refines AtomicTransferFromGlobal;

both action {:layer 1,3} AtomicLoad(l: Lmap int int, a: int) returns (v: int)
{ v := l->val[a]; }
{ v := l->val->val[a]; }

yield procedure {:layer 0} Load(l: Lmap int int, a: int) returns (v: int);
refines AtomicLoad;

both action {:layer 1,3} AtomicStore({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int)
{ l_out := l_in; l_out->val[a] := v; }
{ l_out := l_in; l_out->val->val[a] := v; }

yield procedure {:layer 0} Store({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int);
refines AtomicStore;
Expand Down
Loading

0 comments on commit 37f081f

Please sign in to comment.