From f75e5ba707885666ead81d7c5ec1653e7a09f3ff Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 17 Jan 2016 19:11:04 -0800 Subject: updated the example to implement the allocation of thread identifiers; this example provides another illustration of abstracting ordinary variables by linear variables --- Test/civl/Program4.bpl | 119 +++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 95 insertions(+), 24 deletions(-) (limited to 'Test/civl/Program4.bpl') diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index 68c2a5f3..a6dfcb2a 100644 --- a/Test/civl/Program4.bpl +++ b/Test/civl/Program4.bpl @@ -1,67 +1,138 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type Tid; -var {:layer 0,1} a:[Tid]int; +var {:layer 0,2} a:[int]int; +var {:layer 0,1} count: int; +var {:layer 1,1} {:linear "tid"} unallocated:[int]bool; -procedure {:yields} {:layer 1} main() { - var {:linear "tid"} tid:Tid; +procedure {:yields} {:layer 2} main() +requires {:layer 1} AllocInv(count, unallocated); +{ + var {:layer 1} {:linear "tid"} tid:int; + var i: int; yield; - while (true) { - call tid := Allocate(); - async call P(tid); + assert {:layer 1} AllocInv(count, unallocated); + while (true) + invariant {:layer 1} AllocInv(count, unallocated); + { + call tid, i := Allocate(); + async call P(tid, i); yield; + assert {:layer 1} AllocInv(count, unallocated); } yield; } -procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) -ensures {:layer 1} a[tid] == old(a)[tid] + 1; +procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); +ensures {:layer 2} a[tid] == old(a)[tid] + 1; { var t:int; yield; - assert {:layer 1} a[tid] == old(a)[tid]; - call t := Read(tid); + assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 2} a[tid] == old(a)[tid]; + call t := Read(tid, i); yield; - assert {:layer 1} a[tid] == t; - call Write(tid, t + 1); + assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 2} a[tid] == t; + call Write(tid, i, t + 1); yield; - assert {:layer 1} a[tid] == t + 1; + assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 2} a[tid] == t + 1; } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid) +procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int) +requires {:layer 1} AllocInv(count, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); +ensures {:layer 1} tid == i; +ensures {:atomic} +|{A: + return true; +}|; { yield; - call tid := AllocateLow(); + assert {:layer 1} AllocInv(count, unallocated); + call i := AllocateLow(); + call tid := MakeLinear(i); yield; + assert {:layer 1} AllocInv(count, unallocated); } -procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int); +procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); ensures {:atomic} |{A: val := a[tid]; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, unallocated); + call val := ReadLow(i); + yield; + assert {:layer 1} AllocInv(count, unallocated); +} -procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int); +procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); ensures {:atomic} |{A: a[tid] := val; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, unallocated); + call WriteLow(i, val); + yield; + assert {:layer 1} AllocInv(count, unallocated); +} -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); -ensures {:atomic} |{ A: return true; }|; +function {:inline} AllocInv(count: int, unallocated:[int]bool): (bool) +{ + (forall x: int :: count <= x ==> unallocated[x]) +} + +procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int); +ensures {:atomic} +|{A: + val := a[i]; return true; +}|; + +procedure {:yields} {:layer 0,1} WriteLow(i: int, val: int); +ensures {:atomic} +|{A: + a[i] := val; return true; +}|; +procedure {:yields} {:layer 0,1} AllocateLow() returns (i: int); +ensures {:atomic} +|{A: + i := count; + count := i + 1; + return true; +}|; +// We can prove that this primitive procedure preserves the permission invariant locally. +// We only need to using its specification and the definitions of TidCollector and TidSetCollector. +procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int); +requires unallocated[i]; +modifies unallocated; +ensures tid == i && unallocated == old(unallocated)[i := false]; -function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; -function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; +function {:builtin "MapConst"} MapConstBool(bool): [int]bool; +function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool { MapConstBool(false)[x := true] } -function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool +function {:inline} {:linear "tid"} TidSetCollector(x: [int]bool) : [int]bool { x } -- cgit v1.2.3 From 4d9ec68b4b038ff2e4fe91eec2e82b1d613ee3b0 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 21 Jan 2016 21:28:00 -0800 Subject: improved some of the annotations --- Test/civl/Program4.bpl | 54 ++++++++++++++++++++++----------------------- Test/civl/treiber-stack.bpl | 4 ++-- 2 files changed, 29 insertions(+), 29 deletions(-) (limited to 'Test/civl/Program4.bpl') diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index a6dfcb2a..11ba8afa 100644 --- a/Test/civl/Program4.bpl +++ b/Test/civl/Program4.bpl @@ -2,51 +2,51 @@ // RUN: %diff "%s.expect" "%t" var {:layer 0,2} a:[int]int; var {:layer 0,1} count: int; -var {:layer 1,1} {:linear "tid"} unallocated:[int]bool; +var {:layer 1,1} {:linear "tid"} allocated:[int]bool; procedure {:yields} {:layer 2} main() -requires {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} allocated == MapConstBool(false); { var {:layer 1} {:linear "tid"} tid:int; var i: int; yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); while (true) - invariant {:layer 1} AllocInv(count, unallocated); + invariant {:layer 1} AllocInv(count, allocated); { call tid, i := Allocate(); async call P(tid, i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } yield; } procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int) requires {:layer 1} tid == i; -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:layer 2} a[tid] == old(a)[tid] + 1; { var t:int; yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == old(a)[tid]; call t := Read(tid, i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == t; call Write(tid, i, t + 1); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == t + 1; } procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int) -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:layer 1} tid == i; ensures {:atomic} |{A: @@ -54,48 +54,48 @@ ensures {:atomic} }|; { yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); call i := AllocateLow(); call tid := MakeLinear(i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int) requires {:layer 1} tid == i; -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:atomic} |{A: val := a[tid]; return true; }|; { yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); call val := ReadLow(i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int) requires {:layer 1} tid == i; -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:atomic} |{A: a[tid] := val; return true; }|; { yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); call WriteLow(i, val); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } -function {:inline} AllocInv(count: int, unallocated:[int]bool): (bool) +function {:inline} AllocInv(count: int, allocated:[int]bool): (bool) { - (forall x: int :: count <= x ==> unallocated[x]) + (forall x: int :: allocated[x] ==> x < count) } procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int); @@ -121,9 +121,9 @@ ensures {:atomic} // We can prove that this primitive procedure preserves the permission invariant locally. // We only need to using its specification and the definitions of TidCollector and TidSetCollector. procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int); -requires unallocated[i]; -modifies unallocated; -ensures tid == i && unallocated == old(unallocated)[i := false]; +requires !allocated[i]; +modifies allocated; +ensures tid == i && allocated == old(allocated)[i := true]; function {:builtin "MapConst"} MapConstBool(bool): [int]bool; function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool; diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index bb0201a9..64e01c99 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -1,7 +1,7 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -const unique null: int; +const null: int; type lmap; function {:linear "Node"} dom(lmap): [int]bool; function map(lmap): [int]int; @@ -17,7 +17,7 @@ function Remove(x: lmap, i: int): (lmap); axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int); -ensures {:right} |{ A: assume dom(Stack)[v] || Used[v]; return true; }|; +ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|; procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int); ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C; -- cgit v1.2.3