simplified yield type chcking and added treiber stack (not fully done)

1 files changed, 5 insertions, 11 deletions

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 87538a20..354821e7 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -7,12 +7,10 @@ procedure {:yields} {:phase 2} main()
     yield;

     while (*)

     {

-        yield;

-

         async call Customer();

-

         yield;

     }

+    yield;

 }

 

 procedure {:yields} {:phase 2} Customer()

@@ -20,16 +18,12 @@ procedure {:yields} {:phase 2} Customer()
     yield;

     while (*) 

     {

-    	yield;

-

         call Enter();

-

     	yield;

-

     	call Leave();

-

         yield;

     }

+    yield;

 }

 

 procedure {:yields} {:phase 1,2} Enter() 

@@ -38,21 +32,21 @@ ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;
     var _old, curr: int;

     yield;

     while (true) { 

-    	yield;

         call _old := CAS(0, 1);

 	yield;

         if (_old == 0) {

-	    return;

+	    break;

 	}

 	while (true) {

-	    yield;

 	    call curr := Read();

 	    yield;

 	    if (curr == 0) {

 	        break;

 	    }

 	}

+	yield;

     }

+    yield;

 }

 

 procedure {:yields} {:phase 0,2} Read() returns (val: int);