checkpoint

1 files changed, 24 insertions, 23 deletions

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 953230e7..ea08dcb5 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -6,10 +6,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:qed} t: int;

-var {:qed} s: int;

-var {:qed} cs: X;

-var {:qed} T: [int]bool;

+var {:phase 3} t: int;

+var {:phase 3} s: int;

+var {:phase 3} cs: X;

+var {:phase 3} T: [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -34,7 +34,7 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
 procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

 ensures {:phase 1} {:phase 2} xl != nil;

 

-procedure {:yields} {:entrypoint} main({:linear "tid"} xls':[X]bool)

+procedure {:yields} {:phase 3} main({:linear "tid"} xls':[X]bool)

 requires {:phase 3} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

@@ -50,12 +50,15 @@ requires {:phase 3} xls' == mapconstbool(true);
     invariant {:phase 1} Inv1(T, t);

     invariant {:phase 2} Inv2(T, s, cs);

     {

+	par Yield1() | Yield2() | Yield();

         call xls, tid := Allocate(xls);

         async call Customer(tid);

+    	par Yield1() | Yield2() | Yield();

+

     }

 }

 

-procedure {:yields} {:stable} Customer({:linear "tid"} tid': X)

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

 requires {:phase 1} Inv1(T, t);

 requires {:phase 2} tid' != nil && Inv2(T, s, cs);

 requires {:phase 3} true;

@@ -75,12 +78,12 @@ requires {:phase 3} true;
     }

 }

 

-procedure {:yields} Enter({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

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

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T,t);

 requires {:phase 2} tid' != nil && Inv2(T, s, cs);

 ensures {:phase 2} tid != nil && Inv2(T, s, cs);

-ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

+ensures {:right} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

 {

     var m: int;

 

@@ -92,10 +95,10 @@ ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil
     par Yield1() | Yield2();

 }

 

-procedure {:yields} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)

+procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T, t);

-ensures {:right 1,2} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

+ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

     tid := tid';

@@ -103,33 +106,31 @@ ensures {:right 1,2} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true;
     par Yield1();

 }

 

-procedure {:yields} {:stable} Yield()

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

 {

 }

 

-procedure {:yields} {:stable} Yield2()

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

 requires {:phase 2} Inv2(T, s, cs);

 ensures {:phase 2} Inv2(T, s, cs);

-ensures {:both 2} |{ A: return true; }|;

 {

 }

 

-procedure {:yields} {:stable} Yield1()

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

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T,t);

-ensures {:both 1} |{ A: return true; }|;

 {

 }

 

-procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

-ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

+procedure {:yields} {:phase 0,3} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

+ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

-procedure {:yields} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

-ensures {:atomic 0,1} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;

+procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

+ensures {:atomic} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;

 

-procedure {:yields} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0,2} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;

+procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;

 

-procedure {:yields} Leave({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;

+procedure {:yields} {:phase 0,3} Leave({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;