From 2d839554a676e3030c4b31c2b13ba8887a89a558 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 11 Dec 2023 13:14:44 -0800 Subject: [PATCH] [Civl] Ticket example (#828) - add test driver back - remove nil in favor of Option - use Lval and Lset --- Source/Concurrency/YieldingProcDuplicator.cs | 9 ++- Source/Core/AST/Absy.cs | 4 +- Source/Core/AST/AbsyCmd.cs | 2 +- Source/Core/base.bpl | 4 +- Test/civl/samples/reserve.bpl | 2 +- Test/civl/samples/ticket.bpl | 76 +++++++++++++------- Test/civl/samples/ticket.bpl.expect | 2 +- 7 files changed, 62 insertions(+), 37 deletions(-) diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index d0811a142..61a20c07d 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -188,32 +188,31 @@ public override Implementation VisitImplementation(Implementation impl) public override Block VisitBlock(Block node) { - Block block = base.VisitBlock(node); + var block = base.VisitBlock(node); absyMap[block] = node; return block; } public override Cmd VisitAssertCmd(AssertCmd node) { - AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); + var assertCmd = (AssertCmd) base.VisitAssertCmd(node); if (!node.Layers.Contains(layerNum)) { assertCmd.Expr = Expr.True; } - return assertCmd; } public override Cmd VisitCallCmd(CallCmd call) { - CallCmd newCall = (CallCmd) base.VisitCallCmd(call); + var newCall = (CallCmd) base.VisitCallCmd(call); absyMap[newCall] = call; return newCall; } public override Cmd VisitParCallCmd(ParCallCmd parCall) { - ParCallCmd newParCall = (ParCallCmd) base.VisitParCallCmd(parCall); + var newParCall = (ParCallCmd) base.VisitParCallCmd(parCall); absyMap[newParCall] = parCall; foreach (var newCall in newParCall.CallCmds) { diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index e7a44037f..70e683001 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -2480,7 +2480,7 @@ public override void Resolve(ResolutionContext rc) public override void Typecheck(TypecheckingContext tc) { - tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]); + tc.ExpectedLayerRange = Layers?.Count > 0 ? new LayerRange(Layers[0], Layers[^1]) : null; this.Condition.Typecheck(tc); tc.ExpectedLayerRange = null; Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck @@ -2604,7 +2604,7 @@ public override void Resolve(ResolutionContext rc) public override void Typecheck(TypecheckingContext tc) { - tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]); + tc.ExpectedLayerRange = Layers?.Count > 0 ?new LayerRange(Layers[0], Layers[^1]) : null; this.Condition.Typecheck(tc); tc.ExpectedLayerRange = null; Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 12a681e1b..b878d870e 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -4389,7 +4389,7 @@ public override void Emit(TokenTextWriter stream, int level) public override void Typecheck(TypecheckingContext tc) { (this as ICarriesAttributes).TypecheckAttributes(tc); - tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]); + tc.ExpectedLayerRange = Layers?.Count > 0 ? new LayerRange(Layers[0], Layers[^1]) : null; Expr.Typecheck(tc); tc.ExpectedLayerRange = null; Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 6fc422b59..db5a54328 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -217,8 +217,8 @@ function Set_Intersection(a: Set T, b: Set T): Set T Set(MapAnd(a->val, b->val)) } -function Set_Choose(a: Set T): T; -axiom (forall a: Set T :: {Set_Choose(a)} a == Set_Empty() || Set_Contains(a, Set_Choose(a))); +function Choice(a: [T]bool): T; +axiom (forall a: [T]bool :: {Choice(a)} a == MapConst(false) || a[Choice(a)]); /// finite maps datatype Map { diff --git a/Test/civl/samples/reserve.bpl b/Test/civl/samples/reserve.bpl index ad42492d6..b187fd1ec 100644 --- a/Test/civl/samples/reserve.bpl +++ b/Test/civl/samples/reserve.bpl @@ -100,7 +100,7 @@ pure action PreAlloc({:linear "tid"} tid: Tid, set: Set int, allocMap: Bijection { var ptr: int; assert set != Set_Empty(); - ptr := Set_Choose(set); + ptr := Choice(set->val); allocMap' := Bijection(Map_Update(allocMap->tidToPtr, tid, ptr), Map_Update(allocMap->ptrToTid, ptr, tid)); } diff --git a/Test/civl/samples/ticket.bpl b/Test/civl/samples/ticket.bpl index 2b832990a..9bbcd6b12 100644 --- a/Test/civl/samples/ticket.bpl +++ b/Test/civl/samples/ticket.bpl @@ -6,12 +6,12 @@ function RightClosed (n: int) : [int]bool; axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x); axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); -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 1,2} cs: X; // current thread in critical section -var {:layer 1,2} T: [int]bool; // set of issued tickets +type Tid; + +var {:layer 0,1} t: int; // next ticket to issue +var {:layer 0,2} s: int; // current ticket permitted to critical section +var {:layer 1,2} cs: Option Tid; // current thread in critical section +var {:layer 1,2} T: [int]bool; // set of issued tickets // ########################################################################### // Invariants @@ -21,17 +21,17 @@ function {:inline} Inv1 (tickets: [int]bool, ticket: int): (bool) tickets == RightOpen(ticket) } -function {:inline} Inv2 (tickets: [int]bool, ticket: int, lock: X): (bool) +function {:inline} Inv2 (tickets: [int]bool, ticket: int, lock: Option Tid): (bool) { - if (lock == nil) then tickets == RightOpen(ticket) - else tickets == RightClosed(ticket) + if (lock is None) then tickets == RightOpen(ticket) + else tickets == RightClosed(ticket) } // ########################################################################### // Yield invariants -yield invariant {:layer 2} YieldSpec ({:linear "tid"} tid: X); -invariant tid != nil && cs == tid; +yield invariant {:layer 2} YieldSpec (tid: Lval Tid); +invariant cs is Some && cs->t == tid->val; yield invariant {:layer 1} Yield1 (); invariant Inv1(T, t); @@ -39,13 +39,40 @@ invariant Inv1(T, t); yield invariant {:layer 2} Yield2 (); invariant Inv2(T, s, cs); +// ########################################################################### +// Test driver + +yield procedure {:layer 2} main ({:layer 1,2} {:linear_in} _tids: Lset Tid) +requires call Yield1(); +requires call Yield2(); +{ + var {:layer 1,2} tid: Lval Tid; + var {:layer 1,2} tids: Lset Tid; + + tids := _tids; + while (*) + invariant {:yields} true; + invariant call Yield1(); + invariant call Yield2(); + { + call {:layer 1,2} tid, tids := Allocate(tids); + async call Customer(tid); + } +} + +pure procedure {:inline 1} Allocate({:linear_in} _tids: Lset Tid) returns (tid: Lval Tid, tids: Lset Tid) +{ + tids := _tids; + assume {:layer 1,2} tids->dom != MapConst(false); + call {:layer 1,2} tid := Lval_Get(tids, Choice(tids->dom)); +} + // ########################################################################### // Procedures and actions -yield procedure {:layer 2} Customer ({:layer 1,2} {:linear_in "tid"} tid: X) +yield procedure {:layer 2} Customer ({:layer 1,2} tid: Lval Tid) requires call Yield1(); requires call Yield2(); -requires {:layer 2} tid != nil; { while (*) invariant {:yields} true; @@ -58,11 +85,10 @@ requires {:layer 2} tid != nil; } } -yield procedure {:layer 2} Enter ({:layer 1,2} {:linear "tid"} tid: X) +yield procedure {:layer 2} Enter ({:layer 1,2} tid: Lval Tid) preserves call Yield1(); preserves call Yield2(); ensures call YieldSpec(tid); -requires {:layer 2} tid != nil; { var m: int; @@ -70,10 +96,10 @@ requires {:layer 2} tid != nil; call WaitAndEnter(tid, m); } -right action {:layer 2} AtomicGetTicket ({:linear "tid"} tid: X) returns (m: int) +right action {:layer 2} AtomicGetTicket (tid: Lval Tid) returns (m: int) modifies T; { assume !T[m]; T[m] := true; } -yield procedure {:layer 1} GetTicket ({:layer 1} {:linear "tid"} tid: X) returns (m: int) +yield procedure {:layer 1} GetTicket ({:layer 1} tid: Lval Tid) returns (m: int) refines AtomicGetTicket; preserves call Yield1(); { @@ -87,15 +113,15 @@ modifies t; yield procedure {:layer 0} GetTicket#0 () returns (m: int); refines AtomicGetTicket#0; -atomic action {:layer 2} AtomicWaitAndEnter ({:linear "tid"} tid: X, m:int) +atomic action {:layer 2} AtomicWaitAndEnter (tid: Lval Tid, m:int) modifies cs; -{ assume m == s; cs := tid; } -yield procedure {:layer 1} WaitAndEnter ({:layer 1} {:linear "tid"} tid: X, m:int) +{ assume m == s; cs := Some(tid->val); } +yield procedure {:layer 1} WaitAndEnter ({:layer 1} tid: Lval Tid, m:int) refines AtomicWaitAndEnter; preserves call Yield1(); { call WaitAndEnter#0(m); - call {:layer 1} cs := Copy(tid); + call {:layer 1} cs := Copy(Some(tid->val)); } atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int) @@ -103,15 +129,15 @@ atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int) yield procedure {:layer 0} WaitAndEnter#0 (m:int); refines AtomicWaitAndEnter#0; -atomic action {:layer 2} AtomicLeave ({:linear "tid"} tid: X) +atomic action {:layer 2} AtomicLeave (tid: Lval Tid) modifies cs, s; -{ assert cs == tid; s := s + 1; cs := nil; } -yield procedure {:layer 1} Leave ({:layer 1} {:linear "tid"} tid: X) +{ assert cs == Some(tid->val); s := s + 1; cs := None(); } +yield procedure {:layer 1} Leave ({:layer 1} tid: Lval Tid) refines AtomicLeave; preserves call Yield1(); { call Leave#0(); - call {:layer 1} cs := Copy(nil); + call {:layer 1} cs := Copy(None()); } atomic action {:layer 1} AtomicLeave#0 () diff --git a/Test/civl/samples/ticket.bpl.expect b/Test/civl/samples/ticket.bpl.expect index cccffe05d..12041afe1 100644 --- a/Test/civl/samples/ticket.bpl.expect +++ b/Test/civl/samples/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 11 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors