Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Civl] Ticket example #828

Merged
merged 1 commit into from
Dec 11, 2023
Merged

[Civl] Ticket example #828

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions Source/Concurrency/YieldingProcDuplicator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down
4 changes: 2 additions & 2 deletions Source/Core/AST/Absy.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Source/Core/AST/AbsyCmd.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Source/Core/base.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,8 +217,8 @@ function Set_Intersection<T>(a: Set T, b: Set T): Set T
Set(MapAnd(a->val, b->val))
}

function Set_Choose<T>(a: Set T): T;
axiom (forall<T> a: Set T :: {Set_Choose(a)} a == Set_Empty() || Set_Contains(a, Set_Choose(a)));
function Choice<T>(a: [T]bool): T;
axiom (forall<T> a: [T]bool :: {Choice(a)} a == MapConst(false) || a[Choice(a)]);
Comment on lines +220 to +221
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why ditch the Set_ prefix and working with the Set wrapper type?

Would it be of any use to make the return type Option<T> and return None for empty sets instead of an unconstrained T?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The earlier Set_Choose was defined on the type Set T of finite sets. In the ticket sample, I want to make a choice on the domain of an Lset which is [T]bool. So I thought I would generalize Set_Choose to Choice allowing the idea to work on any set, finite or infinite.

Would it be of any use to make the return type Option and return None for empty sets instead of an unconstrained T?

Currently, I don't see any advantage.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I did not realize that Set is for finite sets. Otherwise the domain of an Lset could have been a Set.


/// finite maps
datatype Map<T,U> {
Expand Down
2 changes: 1 addition & 1 deletion Test/civl/samples/reserve.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}

Expand Down
76 changes: 51 additions & 25 deletions Test/civl/samples/ticket.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -21,31 +21,58 @@ 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);

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;
Expand All @@ -58,22 +85,21 @@ 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;

call m := GetTicket(tid);
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();
{
Expand All @@ -87,31 +113,31 @@ 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)
{ assume m == s; }
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 ()
Expand Down
2 changes: 1 addition & 1 deletion Test/civl/samples/ticket.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Boogie program verifier finished with 11 verified, 0 errors
Boogie program verifier finished with 10 verified, 0 errors
Loading