diff options
author | qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
---|---|---|
committer | qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
commit | 36e016acf963b7c19d59640b11b4a40f2072943e (patch) | |
tree | 31a45e868059d0ffe54fc3d212261245ff97886a /Test/og/linear-set2.bpl | |
parent | 121071b9f87d23eaeba176897b9655cd540fb694 (diff) |
checkpoint
Diffstat (limited to 'Test/og/linear-set2.bpl')
-rw-r--r-- | Test/og/linear-set2.bpl | 48 |
1 files changed, 31 insertions, 17 deletions
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index 04406609..36a8f9c7 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -18,8 +18,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool xs
}
-var x: int;
-var l: X;
+var {:phase 1} x: int;
+var {:phase 1} l: X;
const nil: X;
procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
@@ -28,8 +28,17 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); procedure Allocate() returns ({:linear "tid"} xls: X);
ensures xls != nil;
-procedure {:entrypoint} {:yields} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
-requires tidls' != nil && xls' == All();
+procedure {:yields} {:phase 0,1} Set(v: int);
+ensures {:atomic} |{A: x := v; return true; }|;
+
+procedure {:yields} {:phase 0,1} Lock(tidls: X);
+ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;
+
+procedure {:yields} {:phase 0,1} Unlock();
+ensures {:atomic} |{A: l := nil; return true; }|;
+
+procedure {:yields} {:phase 1} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+requires {:phase 1} tidls' != nil && xls' == All();
{
var {:linear "tid"} tidls: X;
var {:linear "x"} xls: [X]bool;
@@ -40,19 +49,23 @@ requires tidls' != nil && xls' == All(); tidls := tidls';
xls := xls';
- x := 42;
yield;
- assert xls == All();
- assert x == 42;
+ call Set(42);
+ yield;
+ assert {:phase 1} xls == All();
+ assert {:phase 1} x == 42;
call xls1, xls2 := Split(xls);
call lsChild := Allocate();
+ yield;
async call thread(lsChild, xls1);
call lsChild := Allocate();
+ yield;
async call thread(lsChild, xls2);
+ yield;
}
-procedure {:yields} {:stable} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
-requires tidls' != nil && xls' != None();
+procedure {:yields} {:phase 1} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+requires {:phase 1} tidls' != nil && xls' != None();
{
var {:linear "x"} xls: [X]bool;
var {:linear "tid"} tidls: X;
@@ -60,15 +73,16 @@ requires tidls' != nil && xls' != None(); tidls := tidls';
xls := xls';
- assume l == nil;
- l := tidls;
yield;
- assert tidls != nil && xls != None();
- x := 0;
+ call Lock(tidls);
+ yield;
+ assert {:phase 1} tidls != nil && xls != None();
+ call Set(0);
+ yield;
+ assert {:phase 1} tidls != nil && xls != None();
+ assert {:phase 1} x == 0;
yield;
- assert tidls != nil && xls != None();
- assert x == 0;
+ assert {:phase 1} tidls != nil && xls != None();
+ call Unlock();
yield;
- assert tidls != nil && xls != None();
- l := nil;
}
|