From 1633ca623581325c8688e9c86a7859aed347f988 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 28 Nov 2023 19:11:21 -0800 Subject: [PATCH] [Civl] Cleaned up the ticket sample (#818) --- Test/civl/samples/ticket.bpl | 119 ++++++++++------------------ Test/civl/samples/ticket.bpl.expect | 2 +- 2 files changed, 41 insertions(+), 80 deletions(-) diff --git a/Test/civl/samples/ticket.bpl b/Test/civl/samples/ticket.bpl index 320310063..2b832990a 100644 --- a/Test/civl/samples/ticket.bpl +++ b/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,7 +58,7 @@ 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); @@ -91,70 +66,56 @@ 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; diff --git a/Test/civl/samples/ticket.bpl.expect b/Test/civl/samples/ticket.bpl.expect index 2a89032b4..cccffe05d 100644 --- a/Test/civl/samples/ticket.bpl.expect +++ b/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