deleted the free assume about gates after parallel calls

1 files changed, 91 insertions, 54 deletions

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index eadf81e3..be519470 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -15,86 +15,123 @@ function map(lmap): [int]int;
 function cons([int]bool, [int]int) : lmap;

 axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);

 

-var {:phase 2} {:linear "mem"} g: lmap;

+var {:phase 3} {:linear "mem"} g: lmap;

+var {:phase 3} lock: X;

+var {:phase 1} b: bool;

 

 const p: int;

 

-procedure {:yields} {:phase 1,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

-ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

+procedure {:yields} {:phase 1} Yield1()

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

+{

+    yield;

+    assert {:phase 1} InvLock(lock, b);

+}

 

-procedure {:yields} {:phase 1,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

-ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+function {:inline} InvLock(lock: X, b: bool) : bool

+{

+    lock != nil <==> b

+}

 

-procedure {:yields} {:phase 1} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

-ensures {:both} |{ A: v := map(l)[a]; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+procedure {:yields} {:phase 2} Yield2()

+{

+    yield;

+}

 

-procedure {:yields} {:phase 1} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

-ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+procedure {:yields} {:phase 3} Yield3()

+requires {:phase 3} Inv(g);

+ensures {:phase 3} Inv(g);

+{

+    yield;

+    assert {:phase 3} Inv(g);

+}

 

-procedure {:yields} {:phase 2} P({:linear "tid"} tid: X)

-requires {:phase 1} InvLock(lock, b);

+function {:inline} Inv(g: lmap) : bool

+{

+    dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

+}

+

+procedure {:yields} {:phase 3} P({:linear "tid"} tid: X)

+requires {:phase 1} tid != nil && InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

-requires {:phase 2} tid != nil && Inv(g);

-ensures {:phase 2} Inv(g);

+requires {:phase 3} tid != nil && Inv(g);

+ensures {:phase 3} Inv(g);

 {

     var t: int;

     var {:linear "mem"} l: lmap;

 

-    par Yield() | YieldLock();

-    call Acquire(tid);

-    call l := TransferFromGlobal(tid);

+    par Yield3() | Yield1();

+    call AcquireProtected(tid);

+    call l := TransferFromGlobalProtected(tid);

     call t := Load(l, p);

     call l := Store(l, p, t+1);

     call t := Load(l, p+4);

     call l := Store(l, p+4, t+1);

-    call TransferToGlobal(tid, l);

-    call Release(tid);

-    par Yield() | YieldLock();

+    call TransferToGlobalProtected(tid, l);

+    call ReleaseProtected(tid);

+    par Yield3() | Yield1();

 }

 

-procedure {:yields} {:phase 2} Yield()

-requires {:phase 2} Inv(g);

-ensures {:phase 2} Inv(g);

+

+procedure {:yields} {:phase 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)

+ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

 {

-    yield;

-    assert {:phase 2} Inv(g);

+  par Yield1() | Yield2();

+  call TransferToGlobal(tid, l);

+  par Yield1() | Yield2();

 }

 

-function {:inline} Inv(g: lmap) : bool

+procedure {:yields} {:phase 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)

+ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

 {

-    dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

+  par Yield1() | Yield2();

+  call l := TransferFromGlobal(tid);

+  par Yield1() | Yield2();

 }

 

+procedure {:yields} {:phase 2,3} AcquireProtected({:linear "tid"} tid: X)

+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

+requires {:phase 1} tid != nil && InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

+{

+  par Yield1() | Yield2();

+  call Acquire(tid);

+  par Yield1() | Yield2();

+}

 

-var {:phase 1} b: bool;

-var {:phase 2} lock: X;

+procedure {:yields} {:phase 2,3} ReleaseProtected({:linear "tid"} tid: X)

+ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|;

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

+{

+  par Yield1() | Yield2();

+  call Release(tid);

+  par Yield1() | Yield2();

+}

 

 procedure {:yields} {:phase 1,2} Acquire({:linear "tid"} tid: X)

-requires {:phase 1} InvLock(lock, b);

+requires {:phase 1} tid != nil && InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

-ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

+ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;

 {

     var status: bool;

     var tmp: X;

 

-    par YieldLock();

+    par Yield1();

     L: 

 	assert {:phase 1} InvLock(lock, b);

         call status := CAS(tid, false, true);

-	par YieldLock();

+	par Yield1();

         goto A, B;

 

     A: 

         assume status;

-	par YieldLock();	

+	par Yield1();	

 	return;

 

     B:

@@ -103,15 +140,27 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur
 }

 

 procedure {:yields} {:phase 1,2} Release({:linear "tid"} tid: X)

-ensures {:left} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;

+ensures {:atomic} |{ A: lock := nil; return true; }|;

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

 {

-    par YieldLock();

+    par Yield1();

     call CLEAR(tid, false);

-    par YieldLock();

+    par Yield1();

 }

 

+procedure {:yields} {:phase 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

+ensures {:atomic} |{ A: g := l; return true; }|;

+

+procedure {:yields} {:phase 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

+ensures {:atomic} |{ A: l := g; return true; }|;

+

+procedure {:yields} {:phase 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

+ensures {:both} |{ A: v := map(l)[a]; return true; }|;

+

+procedure {:yields} {:phase 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

+ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

+

 procedure {:yields} {:phase 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

 ensures {:atomic} |{ 

 A: goto B, C; 

@@ -124,15 +173,3 @@ ensures {:atomic} |{
 A: b := next; lock := nil; return true; 

 }|;

 

-procedure {:yields} {:phase 1} YieldLock()

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

-{

-    yield;

-    assert {:phase 1} InvLock(lock, b);

-}

-

-function {:inline} InvLock(lock: X, b: bool) : bool

-{

-    lock != nil <==> b

-}