summaryrefslogtreecommitdiff
path: root/Test/civl
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2015-06-17 20:46:44 -0700
committerGravatar qadeer <qadeer@microsoft.com>2015-06-17 20:46:44 -0700
commitd0f2ef8050f0fa2ed6315bc6fd448ee558420d75 (patch)
tree61f62f827e871592418960093d75d9b61398250b /Test/civl
parent56a3836f3606fe035362be14428a412792de371b (diff)
added another sample
Diffstat (limited to 'Test/civl')
-rw-r--r--Test/civl/StoreBuffer.bpl187
-rw-r--r--Test/civl/StoreBuffer.bpl.expect2
2 files changed, 189 insertions, 0 deletions
diff --git a/Test/civl/StoreBuffer.bpl b/Test/civl/StoreBuffer.bpl
new file mode 100644
index 00000000..d2d27ef9
--- /dev/null
+++ b/Test/civl/StoreBuffer.bpl
@@ -0,0 +1,187 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
+{
+ MapConstBool(false)[x := true]
+}
+
+function {:inline} {:linear "addr"} AddrCollector(x: int) : [int]bool
+{
+ MapConstBool(false)[x := true]
+}
+
+const numMutators: int;
+axiom 0 < numMutators;
+function {:inline} mutatorTid(i: int) : bool { 1 <= i && i <= numMutators }
+
+const GcTid: int;
+axiom numMutators < GcTid;
+function {:inline} mutatorOrGcTid(i: int) : bool { (1 <= i && i <= numMutators) || i == GcTid }
+
+const lockAddr: int;
+axiom 0 < lockAddr;
+const collectorPhaseAddr: int;
+axiom lockAddr < collectorPhaseAddr;
+
+var {:layer 0,1} Mem: [int]int;
+var {:layer 0,1} StoreBufferVal: [int][int]int;
+var {:layer 0,1} StoreBufferPresent: [int][int]bool;
+
+var {:layer 0} lock: int;
+var {:layer 0} collectorPhase: int;
+var {:layer 0} collectorPhaseDelayed: int;
+
+function {:inline} LockInv(StoreBufferPresent:[int][int]bool, StoreBufferVal:[int][int]int, Mem:[int]int, lock:int, collectorPhase:int, collectorPhaseDelayed:int): bool
+{
+ (Mem[lockAddr] == 0 <==> lock == 0) &&
+ (forall i:int :: mutatorOrGcTid(i) && StoreBufferPresent[i][lockAddr] ==> StoreBufferVal[i][lockAddr] == 0) &&
+ (forall i:int :: mutatorOrGcTid(i) ==> lock == i || StoreBufferPresent[i] == MapConstBool(false)) &&
+ (Mem[collectorPhaseAddr] == collectorPhase || (exists i:int :: mutatorOrGcTid(i) && StoreBufferPresent[i][collectorPhaseAddr])) &&
+ (forall i:int :: mutatorOrGcTid(i) && StoreBufferPresent[i][collectorPhaseAddr] ==> StoreBufferVal[i][collectorPhaseAddr] == collectorPhase) &&
+ collectorPhaseDelayed == Mem[collectorPhaseAddr]
+}
+
+// Layer 1
+procedure {:yields} {:layer 1} YieldLock()
+requires {:expand} {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+{
+ yield;
+ assert {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+}
+
+procedure {:yields} {:layer 1} YieldStoreBufferLockAddrPresent({:linear "tid"} tid:int)
+requires {:layer 1} StoreBufferPresent[tid][lockAddr];
+ensures {:layer 1} StoreBufferPresent[tid][lockAddr];
+{
+ yield;
+ assert {:layer 1} StoreBufferPresent[tid][lockAddr];
+}
+
+procedure {:yields} {:layer 1} YieldStoreBufferLockAddrAbsent({:linear "tid"} tid:int)
+requires {:layer 1} !StoreBufferPresent[tid][lockAddr];
+ensures {:layer 1} !StoreBufferPresent[tid][lockAddr];
+{
+ yield;
+ assert {:layer 1} !StoreBufferPresent[tid][lockAddr];
+}
+
+procedure {:yields} {:layer 1} LockAcquire({:linear "tid"} tid: int)
+requires {:layer 1} mutatorOrGcTid(tid);
+requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:right} |{ A: assert mutatorOrGcTid(tid); assume lock == 0; lock := tid; return true; }|;
+{
+ var status:bool;
+ call YieldLock();
+ while (true)
+ invariant {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ {
+ call status := LockCAS(tid);
+ if (status)
+ {
+ call YieldLock();
+ return;
+ }
+ call YieldLock();
+ }
+ call YieldLock();
+}
+
+procedure {:yields} {:layer 1} LockRelease({:linear "tid"} tid:int)
+requires {:layer 1} mutatorOrGcTid(tid);
+requires {:layer 1} !StoreBufferPresent[tid][lockAddr];
+requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} !StoreBufferPresent[tid][lockAddr];
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; lock := 0; return true; }|;
+{
+ par YieldLock() | YieldStoreBufferLockAddrAbsent(tid);
+ call LockZero(tid);
+ par YieldLock() | YieldStoreBufferLockAddrPresent(tid);
+ call FlushStoreBufferEntryForLock(tid);
+ par YieldLock() | YieldStoreBufferLockAddrAbsent(tid);
+}
+
+procedure {:yields} {:layer 1} ReadCollectorPhaseLocked({:linear "tid"} tid: int) returns (phase: int)
+requires {:layer 1} mutatorOrGcTid(tid);
+requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; phase := collectorPhase; return true; }|;
+{
+ call YieldLock();
+ call phase := PrimitiveRead(tid, collectorPhaseAddr);
+ call YieldLock();
+}
+
+procedure {:yields} {:layer 1} ReadCollectorPhaseUnlocked({:linear "tid"} tid: int) returns (phase: int)
+requires {:layer 1} mutatorOrGcTid(tid);
+requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock != tid; phase := collectorPhaseDelayed; return true; }|;
+{
+ call YieldLock();
+ call phase := PrimitiveRead(tid, collectorPhaseAddr);
+ call YieldLock();
+}
+
+procedure {:yields} {:layer 1} SetCollectorPhase({:linear "tid"} tid: int, phase: int)
+requires {:layer 1} mutatorOrGcTid(tid);
+requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; assert collectorPhase == collectorPhaseDelayed; collectorPhase := phase; return true; }|;
+{
+ call YieldLock();
+ call PrimitiveSetCollectorPhase(tid, phase);
+ call YieldLock();
+}
+
+procedure {:yields} {:layer 1} SyncCollectorPhase({:linear "tid"} tid: int)
+requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:atomic} |{ A: collectorPhaseDelayed := collectorPhase; return true; }|;
+{
+ call YieldLock();
+ call FlushStoreBufferEntryForCollectorPhase();
+ call YieldLock();
+}
+
+procedure {:yields} {:layer 1} Barrier({:linear "tid"} tid: int)
+requires {:layer 1} mutatorOrGcTid(tid);
+requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed);
+ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; assume collectorPhase == collectorPhaseDelayed; return true; }|;
+{
+ call YieldLock();
+ call WaitForFlush(tid);
+ call YieldLock();
+}
+
+// Layer 0
+procedure {:yields} {:layer 0,1} LockCAS(tid: int) returns (status: bool);
+ensures {:atomic} |{ A: goto B, C;
+ B: assume Mem[lockAddr] == 0; Mem[lockAddr] := 1; lock := tid; status := true; return true;
+ C: status := false; return true;
+ }|;
+
+procedure {:yields} {:layer 0,1} LockZero(tid: int);
+ensures {:atomic} |{ A: assert !StoreBufferPresent[tid][lockAddr]; StoreBufferPresent[tid][lockAddr] := true; StoreBufferVal[tid][lockAddr] := 0; return true; }|;
+
+procedure {:yields} {:layer 0,1} FlushStoreBufferEntryForLock(tid: int);
+ensures {:atomic} |{ A: assert StoreBufferPresent[tid][lockAddr]; assume StoreBufferPresent[tid] == MapConstBool(false)[lockAddr := true]; Mem[lockAddr] := StoreBufferVal[tid][lockAddr]; StoreBufferPresent[tid][lockAddr] := false; lock := 0; return true; }|;
+
+procedure {:yields} {:layer 0,1} PrimitiveRead(tid: int, addr: int) returns (val: int);
+ensures {:atomic} |{ A: goto B, C;
+ B: assume StoreBufferPresent[tid][addr]; val := StoreBufferVal[tid][addr]; return true;
+ C: assume !StoreBufferPresent[tid][addr]; val := Mem[addr]; return true; }|;
+
+procedure {:yields} {:layer 0,1} PrimitiveSetCollectorPhase(tid: int, phase:int);
+ensures {:atomic} |{ A: StoreBufferPresent[tid][collectorPhaseAddr] := true; StoreBufferVal[tid][collectorPhaseAddr] := phase; collectorPhase := phase; return true; }|;
+
+procedure {:yields} {:layer 0,1} FlushStoreBufferEntryForCollectorPhase();
+ensures {:atomic} |{ var tid:int; A: assume mutatorOrGcTid(tid) && StoreBufferPresent[tid][collectorPhaseAddr]; Mem[collectorPhaseAddr] := StoreBufferVal[tid][collectorPhaseAddr]; StoreBufferPresent[tid][collectorPhaseAddr] := false; collectorPhaseDelayed := Mem[collectorPhaseAddr]; return true; }|;
+
+procedure {:yields} {:layer 0,1} WaitForFlush(tid: int);
+ensures {:atomic} |{ A: assume StoreBufferPresent[tid] == MapConstBool(false); return true; }|;
diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect
new file mode 100644
index 00000000..8c74fe2e
--- /dev/null
+++ b/Test/civl/StoreBuffer.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 17 verified, 0 errors