[Civl] Cleaned up the ticket sample (#818)

Test/civl/samples/ticket.bpl

@@ -10,8 +10,8 @@ type {:linear "tid"} X;
 const nil: X;
 var {:layer 0,1} t: int;       // next ticket to issue
 var {:layer 0,2} s: int;       // current ticket permitted to critical section
-var {:layer 0,2} cs: X;        // current thread in critical section
-var {:layer 0,2} T: [int]bool; // set of issued tickets
+var {:layer 1,2} cs: X;        // current thread in critical section
+var {:layer 1,2} T: [int]bool; // set of issued tickets
 
 // ###########################################################################
 // Invariants
@@ -40,34 +40,9 @@ yield invariant {:layer 2} Yield2 ();
 invariant Inv2(T, s, cs);
 
 // ###########################################################################
-// Main program
+// Procedures and actions
 
-yield procedure {:layer 2} main ({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == MapConst(true);
-{
-  var {:linear "tid"} tid: X;
-  var {:linear "tid"} xls: [X]bool;
-
-  call InitAbstract(xls');
-  xls := xls';
-
-  while (*)
-  invariant {:yields} true;
-  invariant call Yield1();
-  invariant call Yield2();
-  {
-    par xls, tid := Allocate(xls) | Yield1() | Yield2();
-    async call Customer(tid);
-  }
-}
-
-yield procedure {:layer 2} Allocate ({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X)
-ensures {:layer 1,2} xl != nil;
-{
-  call xls, xl := AllocateLow(xls');
-}
-
-yield procedure {:layer 2} Customer ({:linear_in "tid"} tid: X)
+yield procedure {:layer 2} Customer ({:layer 1,2} {:linear_in "tid"} tid: X)
 requires call Yield1();
 requires call Yield2();
 requires {:layer 2} tid != nil;
@@ -83,78 +58,64 @@ requires {:layer 2} tid != nil;
   }
 }
 
-yield procedure {:layer 2} Enter ({:linear "tid"} tid: X)
+yield procedure {:layer 2} Enter ({:layer 1,2} {:linear "tid"} tid: X)
 preserves call Yield1();
 preserves call Yield2();
 ensures   call YieldSpec(tid);
 requires {:layer 2} tid != nil;
 {
   var m: int;
 
-  call m := GetTicketAbstract(tid);
+  call m := GetTicket(tid);
   call WaitAndEnter(tid, m);
 }
 
-// ###########################################################################
-// Abstractions of primitive atomic actions
-
-// Note how GetTicketAbstract becomes a right mover
-
-atomic action {:layer 2} AtomicInitAbstract ({:linear "tid"} xls:[X]bool)
-modifies cs, s, T;
-{ assert xls == MapConst(true); cs := nil; s := 0; T := RightOpen(0); }
-
-yield procedure {:layer 1} InitAbstract ({:linear "tid"} xls:[X]bool)
-refines AtomicInitAbstract;
-ensures call Yield1();
-{
-  call Init(xls);
-}
-
-right action {:layer 2} AtomicGetTicketAbstract ({:linear "tid"} tid: X) returns (m: int)
+right action {:layer 2} AtomicGetTicket ({:linear "tid"} tid: X) returns (m: int)
 modifies T;
 { assume !T[m]; T[m] := true; }
-
-yield procedure {:layer 1} GetTicketAbstract ({:linear "tid"} tid: X) returns (m: int)
-refines AtomicGetTicketAbstract;
+yield procedure {:layer 1} GetTicket ({:layer 1} {:linear "tid"} tid: X) returns (m: int)
+refines AtomicGetTicket;
 preserves call Yield1();
 {
-  call m := GetTicket(tid);
+  call m := GetTicket#0();
+  call {:layer 1} T := Copy(T[m := true]);
 }
 
-// ###########################################################################
-// Primitive atomic actions
-
-atomic action {:layer 1} AtomicInit ({:linear "tid"} xls:[X]bool)
-modifies cs, t, s, T;
-{ assert xls == MapConst(true); cs := nil; t := 0; s := 0; T := RightOpen(0); }
-
-yield procedure {:layer 0} Init ({:linear "tid"} xls:[X]bool);
-refines AtomicInit;
-
-atomic action {:layer 1} AtomicGetTicket ({:linear "tid"} tid: X) returns (m: int)
-modifies t, T;
-{ m := t; t := t + 1; T[m] := true; }
-
-yield procedure {:layer 0} GetTicket ({:linear "tid"} tid: X) returns (m: int);
-refines AtomicGetTicket;
+atomic action {:layer 1} AtomicGetTicket#0 () returns (m: int)
+modifies t;
+{ m := t; t := t + 1; }
+yield procedure {:layer 0} GetTicket#0 () returns (m: int);
+refines AtomicGetTicket#0;
 
-atomic action {:layer 1,2} AtomicWaitAndEnter ({:linear "tid"} tid: X, m:int)
+atomic action {:layer 2} AtomicWaitAndEnter ({:linear "tid"} tid: X, m:int)
 modifies cs;
 { assume m == s; cs := tid; }
-
-yield procedure {:layer 0} WaitAndEnter ({:linear "tid"} tid: X, m:int);
+yield procedure {:layer 1} WaitAndEnter ({:layer 1} {:linear "tid"} tid: X, m:int)
 refines AtomicWaitAndEnter;
+preserves call Yield1();
+{
+  call WaitAndEnter#0(m);
+  call {:layer 1} cs := Copy(tid);
+}
+
+atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int)
+{ assume m == s; }
+yield procedure {:layer 0} WaitAndEnter#0 (m:int);
+refines AtomicWaitAndEnter#0;
 
-atomic action {:layer 1,2} AtomicLeave ({:linear "tid"} tid: X)
+atomic action {:layer 2} AtomicLeave ({:linear "tid"} tid: X)
 modifies cs, s;
 { assert cs == tid; s := s + 1; cs := nil; }
-
-yield procedure {:layer 0} Leave ({:linear "tid"} tid: X);
+yield procedure {:layer 1} Leave ({:layer 1} {:linear "tid"} tid: X)
 refines AtomicLeave;
+preserves call Yield1();
+{
+  call Leave#0();
+  call {:layer 1} cs := Copy(nil);
+}
 
-atomic action {:layer 1,2} AtomicAllocateLow ({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X)
-{ assume xl != nil && xls'[xl]; xls := xls'[xl := false]; }
-
-yield procedure {:layer 0} AllocateLow ({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
-refines AtomicAllocateLow;
+atomic action {:layer 1} AtomicLeave#0 ()
+modifies s;
+{ s := s + 1; }
+yield procedure {:layer 0} Leave#0 ();
+refines AtomicLeave#0;

Test/civl/samples/ticket.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 19 verified, 0 errors
+Boogie program verifier finished with 11 verified, 0 errors