diff options
| author |  qadeer <unknown> | 2014-07-12 15:31:40 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-07-12 15:31:40 -0700 |
| commit | 85a60be8a0a7ef1438908364b7997dddc4524ed1 (patch) | |
| tree | 356d1801d0338ae1ec91d22909b88ea589cbad11 /Test/og/Program5.bpl | |
| parent | 5ef33fad3a4d6438d7e3c38388639eff7f08533d (diff) | |
added tests
Diffstat (limited to 'Test/og/Program5.bpl')
| -rw-r--r-- | Test/og/Program5.bpl | 97 |
1 files changed, 97 insertions, 0 deletions
diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl new file mode 100644 index 00000000..845bf1a4 --- /dev/null +++ b/Test/og/Program5.bpl @@ -0,0 +1,97 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type Tid;
+const unique nil: Tid;
+function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
+function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
+
+var {:phase 0,3} Color:int;
+var {:phase 0,3} lock:Tid;
+
+function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+{
+ MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
+{
+ x
+}
+
+function {:inline} UNALLOC():int { 0 }
+function {:inline} WHITE():int { 1 }
+function {:inline} GRAY():int { 2 }
+function {:inline} BLACK():int { 3 }
+function {:inline} Unalloc(i:int) returns(bool) { i <= 0 }
+function {:inline} White(i:int) returns(bool) { i == 1 }
+function {:inline} Gray(i:int) returns(bool) { i == 2 }
+function {:inline} Black(i:int) returns(bool) { i >= 3 }
+
+procedure {:yields} {:phase 0,1} AcquireLock({:cnst "tid"} tid: Tid);
+ ensures {:right} |{ A: assert tid != nil;
+ assume lock == nil;
+ lock := tid;
+ return true; }|;
+
+procedure {:yields} {:phase 0,1} ReleaseLock({:cnst "tid"} tid: Tid);
+ ensures {:left} |{ A: assert tid != nil;
+ assert lock == tid;
+ lock := nil;
+ return true; }|;
+
+procedure {:yields} {:phase 0,1} SetColorLocked({:cnst "tid"} tid:Tid, newCol:int);
+ ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|;
+
+procedure {:yields} {:phase 0,1} GetColorLocked({:cnst "tid"} tid:Tid) returns (col:int);
+ ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;
+
+procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);
+ ensures {:atomic} |{A: col := Color; return true;}|;
+
+procedure {:yields} {:phase 2} YieldColorOnlyGetsDarker()
+ensures {:phase 2} Color >= old(Color);
+{
+ yield;
+ assert {:phase 2} Color >= old(Color);
+}
+
+
+procedure {:yields} {:phase 2,3} TopWriteBarrier({:cnst "tid"} tid:Tid)
+ensures {:atomic} |{ A: assert tid != nil;
+ goto B, C;
+ B: assume White(Color);
+ Color := GRAY();
+ return true;
+ C: return true;}|;
+{
+ var colorLocal:int;
+
+ yield;
+
+ call colorLocal := GetColorNoLock();
+ call YieldColorOnlyGetsDarker();
+ if (White(colorLocal)) {
+ call MidWriteBarrier(tid);
+ }
+
+ yield;
+}
+
+procedure {:yields} {:phase 1,2} MidWriteBarrier({:cnst "tid"} tid:Tid)
+ensures {:atomic} |{ A: assert tid != nil;
+ goto B, C;
+ B: assume White(Color);
+ Color := GRAY();
+ return true;
+ C: return true;}|;
+{
+ var colorLocal:int;
+
+ yield;
+ call AcquireLock(tid);
+ call colorLocal := GetColorLocked(tid);
+ if (White(colorLocal)) {
+ call SetColorLocked(tid, GRAY());
+ }
+ call ReleaseLock(tid);
+ yield;
+}
\ No newline at end of file |