diff options
author | qadeer <unknown> | 2014-07-15 02:26:38 -0700 |
---|---|---|
committer | qadeer <unknown> | 2014-07-15 02:26:38 -0700 |
commit | 7395870356fb83f1b7cab70c95523d1c9f5738d4 (patch) | |
tree | b8677cada625458aacba867081549e4a784c453d /Test/og/ticket.bpl | |
parent | 85a60be8a0a7ef1438908364b7997dddc4524ed1 (diff) |
simplified yield type chcking and added treiber stack (not fully done)
Diffstat (limited to 'Test/og/ticket.bpl')
-rw-r--r-- | Test/og/ticket.bpl | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index d532c5a2..02341e91 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -52,12 +52,11 @@ 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();
-
}
+ par Yield1() | Yield2() | Yield();
}
procedure {:yields} {:phase 3} Customer({:linear "tid"} tid': X)
@@ -73,12 +72,12 @@ requires {:phase 3} true; invariant {:phase 1} Inv1(T, t);
invariant {:phase 2} tid != nil && Inv2(T, s, cs);
{
- par Yield1() | Yield2() | Yield();
call tid := Enter(tid);
par Yield1() | Yield2();
call tid := Leave(tid);
par Yield1() | Yield2() | Yield();
}
+ par Yield1() | Yield2() | Yield();
}
procedure {:yields} {:phase 2,3} Enter({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
|