From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/civl/StoreBuffer.bpl | 187 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 187 insertions(+) create mode 100644 Test/civl/StoreBuffer.bpl (limited to 'Test/civl/StoreBuffer.bpl') 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; }|; -- cgit v1.2.3