bug fix in handling of parallel call

1 files changed, 29 insertions, 38 deletions

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 707688a6..6e87d8f3 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -1,48 +1,39 @@
 type Node;

 type lmap;

-function dom(lmap): [Node]bool;

+function {:linear "Node"} dom(lmap): [Node]bool;

 function map(lmap): [Node]Node;

 

-function {:builtin "MapConst"} MapConst(bool) : [Node]bool;

-function {:builtin "MapOr"} MapOr([Node]bool, [Node]bool) : [Node]bool;

+procedure {:yields} Load(i:Node) returns(v:Node);

+requires dom(stack)[i];

+ensures {:atomic 0} v == map(stack)[i];

 

-procedure Load(i:Node) returns(v:Node);

-  requires dom(stack)[i];

-  ensures  v == map(stack)[i];

+procedure {:yields} Store({:linear "Node"} l_in:lmap, i:Node, v:Node) returns({:linear "Node"} l_out:lmap);

+requires dom(l_in)[i];

+ensures {:atomic 0} dom(l_out) == dom(l_in) && map(l_out) == map(l_in)[i := v];

 

-procedure Store({:linear "Node"} l_in:lmap, i:Node, v:Node) returns({:linear "Node"} l_out:lmap);

-  requires dom(l_in)[i];

-  ensures  dom(l_out) == dom(l_in);

-  ensures  map(l_out) == map(l_in)[i := v];

+procedure {:yields} TransferToStack(oldVal: Node, newVal: Node, {:linear "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

+requires dom(l_in)[newVal];

+modifies stack, TOP;

+ensures {:atomic 0} if oldVal == old(TOP)

+		    then newVal == TOP && dom(stack) == dom(old(stack))[newVal := true] && map(stack) == map(old(stack))[newVal := map(l_in)[newVal]]

+                    else TOP == old(TOP) && stack == old(stack) && l_out == l_in;

 

-procedure TransferIn({:linear "Node"} l1_in:lmap, d:Node);

-  requires dom(l1_in)[d];

-  modifies stack;

-  ensures  dom(stack) == dom(old(stack))[d := true];

-  ensures  map(stack) == map(old(stack))[d := map(l1_in)[d]];

+procedure {:yields} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool, {:linear "Node"} l_out:lmap);

+requires dom(stack)[oldVal];

+modifies stack, TOP;

+ensures {:atomic 0} if oldVal == old(TOP)

+		    then dom(stack) == dom(old(stack))[oldVal := false] && map(stack) == map(old(stack)) && dom(l_out)[oldVal] && map(l_out)[oldVal] == map(old(stack))[oldVal]

+		    else TOP == old(TOP) && stack == old(stack);

 

-procedure TransferOut(d:Node);

-  requires dom(stack)[d];

-  modifies stack;

-  ensures  dom(stack) == dom(old(stack))[d := false];

-  ensures  map(stack) == map(old(stack));

-

-procedure New() returns ({:linear "Node"} l: lmap, d: Node);

+procedure Alloc() returns (d: Node, {:linear "Node"} l: lmap);

 ensures dom(l)[d];

 

-const unique null: Node;

+procedure Free(d: Node, {:linear "Node"} l: lmap);

 

-var TOP: Node;

-var {:linear "Node"} stack: lmap;

+const unique null: Node;

 

-procedure {:yields} CAS(oldVal: Node, newVal: Node)

-returns (r: bool)

-{

-  r := (TOP == oldVal);

-  if (r) {

-    TOP := newVal;

-  }

-}

+var {:qed} TOP: Node;

+var {:qed} {:linear "Node"} stack: lmap;

 

 procedure {:yields} push()

 {

@@ -50,15 +41,14 @@ procedure {:yields} push()
   var g: bool;

   var {:linear "Node"} x_lmap: lmap;

 

-  call x_lmap, x := New();

+  call x, x_lmap := Alloc();

 

   while(true)

   {

     t := TOP;		

     call x_lmap := Store(x_lmap, x, t);

-    call g := CAS(t, x); 

+    call g, x_lmap := TransferToStack(t, x, x_lmap); 

     if (g) { 

-      call TransferIn(x_lmap, x);

       break; 

     }

   }

@@ -68,6 +58,7 @@ procedure {:yields} pop()
 {

   var t, x: Node;

   var g: bool;

+  var {:linear "Node"} t_lmap: lmap;

 

   while(true)

   {

@@ -77,9 +68,9 @@ procedure {:yields} pop()
       return;

     }

     call x := Load(t);

-    call g := CAS(t, x); 

+    call g, t_lmap := TransferFromStack(t, x); 

     if (g) { 

-      call TransferOut(t);

+      call Free(t, t_lmap);

       break; 

     }

   }