summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2015-03-29 15:25:20 -0700
committerGravatar qadeer <qadeer@microsoft.com>2015-03-29 15:25:20 -0700
commitdeca4eb05615d2b4bfba797a91b2f031cd1ac925 (patch)
treec24eb0706c58bd3c74a56864144acaa3ba504857
parentacf480577d80670bec476852190f3d27fca62657 (diff)
updated the example to include atomic specifications (sent by Suha)
-rw-r--r--Test/og/wsq.bpl19
1 files changed, 18 insertions, 1 deletions
diff --git a/Test/og/wsq.bpl b/Test/og/wsq.bpl
index 291cd31b..9cb6a19b 100644
--- a/Test/og/wsq.bpl
+++ b/Test/og/wsq.bpl
@@ -14,7 +14,7 @@ function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
var {:layer 0,3} H: int;
var {:layer 0,3} T: int;
var {:layer 0,3} items: [int]int;
-var {:layer 0,3} status: [int]bool;
+var {:layer 0} status: [int]bool;
var {:layer 0,3} take_in_cs: bool;
var {:layer 0,3} put_in_cs: bool;
var {:layer 0,3} steal_in_cs: [Tid]bool;
@@ -61,6 +61,11 @@ function {:inline} queueInv(steal_in_cs:[Tid]bool,
( (forall i:int :: (_H <= i && i <= _T) ==> (status[i] == IN_Q && items[i] != EMPTY)) )
}
+function {:inline} emptyInv(put_in_cs:bool, take_in_cs:bool, items:[int]int, status:[int]bool, T:int):(bool)
+{
+ (forall i:int :: (i>=T && !put_in_cs && !take_in_cs) ==> status[i] == NOT_IN_Q && items[i] == EMPTY)
+}
+
function {:inline} putInv(items:[int]int, status: [int]bool, H:int, T:int):(bool)
{
(forall i:int :: (H <= i && i < T) ==> (status[i] == IN_Q && items[i] != EMPTY))
@@ -77,8 +82,11 @@ function {:inline} takeInv(items:[int]int, status: [int]bool, H:int, T:int, t:in
procedure {:yields} {:layer 3} put({:linear "tid"} tid:Tid, task: int)
requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && task != EMPTY && !take_in_cs && !put_in_cs;
requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+requires {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
ensures {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
+ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
{
var t: int;
var {:aux} oldH:int;
@@ -92,6 +100,7 @@ ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs,
assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
assert {:layer 3} oldH <= H && oldT == T;
+ assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
call t := readT_put(tid);
@@ -102,6 +111,7 @@ ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs,
assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
assert {:layer 3} tid == ptTid && t == T;
assert {:layer 3} oldH <= H && oldT == T;
+ assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);
call writeItems_put(tid,t, task);
@@ -113,6 +123,8 @@ ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs,
assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
assert {:layer 3} items[t] == task;
assert {:layer 3} oldH <= H && oldT == T;
+ assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);
+
call writeT_put(tid, t+1);
@@ -123,6 +135,7 @@ ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs,
assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
assert {:layer 3} T == t + 1;
assert {:layer 3} oldH <= H && oldT == T;
+ assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
}
procedure {:yields} {:layer 3} take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool)
@@ -130,6 +143,7 @@ requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, s
requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs && (task != EMPTY ==> taskstatus == IN_Q);
ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|;
{
var h, t: int;
var chk: bool;
@@ -296,6 +310,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
}
+
procedure {:yields}{:layer 3} steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool)
requires {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && stealerTid(tid) &&
!steal_in_cs[tid];
@@ -303,6 +318,7 @@ requires {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in
ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) &&
!steal_in_cs[tid] && (task != EMPTY ==> taskstatus == IN_Q);
ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|;
{
var h, t: int;
var chk: bool;
@@ -388,6 +404,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
assert {:layer 3} oldH <= H;
assert {:layer 3} oldH == H && H == h && h_ss[tid] == h ==> task != EMPTY;
assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T);
+ assert {:layer 3} h == H ==> status[H] == IN_Q;
call chk := CAS_H_steal(tid, h,h+1);