Petersen Critical Section Correctness
Correctness of Petersen Critical Section Algorithm
This example builds on techniques developed for the Alternating Bit Protocol, but the proof makes especially good
use of the product of case analyses. There are 10 binary cases splits, and
therefore 1024 cases altogether. Although many of these cases are
automatically eliminated by BOBJ because they fail to satisfy the condition of
the equation proved, the output is still very voluminous, since every case is
documented, including the failures. (The purpose of the condition in the
equation of the correctness criterion is to eliminate cases that cannot
occur.) One can also see many instances of circularities in the output,
signaled by the keyword "deduced". This example is still in an
early stage of development, and there is as yet very little explanation; it is
highly likely to become more polished in the future.
The specification and proof score are given in section 1, but only an
extract from the output is given in section 2, since it is very voluminous,
but here is a link to the full output if you want to
see it. Note that execution time is exponential in the number of cases.
Notice also that the fair streams used here differ from those in the
alternating bit protocol, since they need to be fair to each of the two
processes, instead of being fair to channel success, but not failure.
1. BOBJ Source Code
<![CDATA[
*** file: /tatami/bobj/examples/abp/pete.bob
*** correctness of petersen's critical section algorithm
bth STREAM [ X :: TRIV ] is sort Stream .
op hd_ : Stream -> Elt .
op tl_ : Stream -> Stream .
op _&_ : Elt Stream -> Stream .
var E : Elt . var S : Stream .
eq hd(E & S) = E .
eq tl(E & S) = S .
end
***> fair boolean stream (no infinite consecutive true or false)
bth FAIR-STREAM is pr STREAM[NAT] * (sort Stream to FairStream) + NAT .
op fhd_ : FairStream -> Bool .
op ftl_ : FairStream -> FairStream .
op _#_#_ : Nat Nat FairStream -> FairStream .
vars M N : Nat . var F : FairStream .
eq fhd(0 # M # F) = true .
eq ftl(0 # 0 # F) = F .
eq ftl(0 # s M # F) = 0 # M # F .
eq fhd(s M # N # F) = false .
eq ftl(s M # N # F) = M # N # F .
end
dth MACHINE is sort MState . pr NAT .
op <_,_,_> : Bool Bool Nat -> MState .
ops (idle_) (wait_) (busy_) (run_) : MState -> Bool .
op count _ : MState -> Nat .
op do_ : MState -> MState .
op init__ : Nat MState -> MState .
op begin_ : MState -> MState .
vars B D : Bool . vars M N : Nat .
eq idle <B, D, N> = not B .
eq wait <B, D, N> = B and not D .
eq busy <B, D, N> = B .
eq run <B, D, N> = D .
eq count <B, D, N> = N .
eq do <true, true, N> = <true, true, p N> if N > 0 .
eq do <true, true, 0> = <false, false, 0> .
eq do <B, D, N> = <B, D, N> if not B or not D .
eq init M <false, false, N> = <true, false, M> .
eq begin <true, false, N> = <true, true, N> .
end
dth SYSTEM-STATE is sorts SysState Flag .
pr MACHINE .
ops a b : -> Flag .
op _|_|_ : Flag MState MState -> SysState .
op eq : Flag Flag -> Bool [comm] .
var F : Flag .
eq eq(F, F) = true .
eq eq(a, b) = false .
end
bth PETERSON is pr STREAM[NAT] * (sort Stream to Request) +
STREAM[SYSTEM-STATE] * (sort Stream to Trace) + FAIR-STREAM .
op [_,_,_,_] : SysState Request Request FairStream -> Trace .
var F : Flag . vars Ma Mb : MState .
vars Ra Rb : Request . var Fs : FairStream .
eq hd [ F | Ma | Mb , Ra, Rb, Fs ] = F | Ma | Mb .
*** process A sends a request
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ b | init (hd Ra) Ma | do Mb , tl(Ra), Rb, tl(Fs) ]
if fhd(Fs) and hd(Ra) > 0 and idle Ma .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | Ma | do Mb, tl(Ra), Rb, ftl(Fs) ]
if fhd(Fs) and eq(hd(Ra), 0) and idle Ma .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | begin Ma | do Mb , Ra, Rb, ftl(Fs) ]
if fhd(Fs) and wait Ma and (eq(F, a) or not busy Mb) .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | Ma | do Mb , Ra, Rb, ftl(Fs) ]
if fhd(Fs) and wait Ma and eq(F, b) and busy Mb .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | do Ma | do Mb, Ra, Rb, ftl(Fs) ]
if fhd(Fs) and run Ma .
*** process B sends a request
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ a | do Ma | init (hd Rb) Mb , Ra, tl(Rb), ftl(Fs) ]
if not fhd(Fs) and hd(Rb) > 0 and idle Mb .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | do Ma | Mb, Ra, tl(Rb), ftl(Fs) ]
if not fhd(Fs) and eq(hd(Rb), 0) and idle Mb .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | do Ma | begin Mb, Ra, Rb, ftl(Fs) ]
if not fhd(Fs) and wait Mb and (eq(F, b) or not busy Ma ) .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | do Ma | Mb, Ra, Rb, ftl(Fs) ]
if not fhd(Fs) and wait Mb and eq(F, a) and busy Ma .
eq tl [ F | Ma | Mb , Ra, Rb, Fs ] =
[ F | do Ma | do Mb, Ra, Rb, ftl(Fs) ]
if not fhd(Fs) and run Mb .
end
***> here begins the proof ***
dth PROOF is pr STREAM[BOOL] * (sort Stream to BStream) + PETERSON .
op sys_ : Trace -> BStream .
op good_ : SysState -> Bool .
op all-true : -> BStream .
var Tr : Trace . var F : Flag . vars Ma Mb : MState .
eq hd sys Tr = good (hd Tr) .
eq tl sys Tr = sys tl Tr .
eq good ( F | Ma | Mb ) =
not (run Ma and run Mb ) and
(run Ma implies (busy Ma and (eq(F, a) or not busy Mb))) and
(run Mb implies (busy Mb and (eq(F, b) or not busy Ma))) and
(not busy Ma implies ((not run Ma) and eq(count Ma, 0))) and
(not busy Mb implies ((not run Mb) and eq(count Mb, 0))) .
eq hd all-true = true .
eq tl all-true = all-true .
end
cobasis COB from PROOF is
op hd : BStream -> Bool .
op tl : BStream -> BStream .
end
cases C1 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq F = a .
case eq F = b .
end
cases C2 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq Ba = true .
case eq Ba = false .
end
cases C3 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq Bb = true .
case eq Bb = false .
end
cases C4 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq Da = true .
case eq Da = false .
end
cases C5 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq Db = true .
case eq Db = false .
end
cases C6 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq M = 0 .
case eq M > 0 = true .
end
cases C7 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq N = 0 .
case eq N > 0 = true .
end
cases C8 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq hd(Ra) = 0 .
case eq hd(Ra) > 0 = true .
end
cases C9 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq hd(Rb) = 0 .
case eq hd(Rb) > 0 = true .
end
cases C10 for PROOF is
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
context [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] .
case eq fhd(Fs) = true .
case eq fhd(Fs) = false .
end
***> mutual exclusion property
set cred trace on .
open PROOF .
use C1 * C2 * C3 * C4 * C5 * C6 * C7 * C8 * C9 * C10 .
var F : Flag . vars M N : Nat . vars Ba Bb Da Db : Bool .
vars Ra Rb : Request . var Fs : FairStream .
set cobasis COB .
cred sys [ F | <Ba, Da, M> | <Bb, Db, N>, Ra, Rb, Fs ] == all-true
if good (F | <Ba, Da, M> | <Bb, Db, N>) .
close
*** *************************************************************
*** Liveness is not yet done
*** *************************************************************
<xmp>
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.197 built: Tue Nov 5 12:12:21 PST 2002
University of California, San Diego
Wed Nov 06 10:49:14 PST 2002
BOBJ> in pete
==========================================
bth STREAM
==========================================
***> fair boolean stream (no infinite consecutive true or false)
==========================================
bth FAIR-STREAM
==========================================
dth MACHINE
Warning: redefining module MACHINE
==========================================
dth SYSTEM-STATE
Warning: redefining module SYSTEM-STATE
==========================================
bth PETERSON
==========================================
***> here begins the proof ***
==========================================
dth PROOF
==========================================
cases C1
==========================================
cases C2
==========================================
cases C3
==========================================
cases C4
==========================================
cases C5
==========================================
cases C6
==========================================
cases C7
==========================================
cases C8
==========================================
cases C9
==========================================
cases C10
==========================================
***> mutual exclusion property
==========================================
open PROOF
==========================================
use C1 * C2 * C3 * C4 * C5 * C6 * C7 * C8 * C9 * C10
==========================================
var F : Flag
==========================================
vars M N : Nat
==========================================
vars Ba Bb Da Db : Bool
==========================================
vars Ra Rb : Request
==========================================
var Fs : FairStream
==========================================
set cobasis COB
==========================================
c-reduce in PROOF : sys ([(F | (< Ba , Da , M >) | (< Bb , Db , N >))
, Ra , Rb , Fs]) == all-true if good (F | (< Ba , Da , M >) | (<
Bb , Db , N >))
using cobasis COB for PROOF
-------------------------------------------
case analysis by C1 * C2 * C3 * C4 * C5 * C6 * C7 * C8 * C9 * C10
-------------------------------------------
introduce constant(s):
r for the variable Ra
f1 for the variable Fs
r1 for the variable Rb
-------------------------------
case (1,1,1,1,1,1,1,1,1,1) :
assume: f = a
ba = true
bb = true
da = true
db = true
m = 0
n = 0
hd r = 0
hd r1 = 0
fhd f1 = true
the condition is false: good (f | (< ba , da , m >) | (< bb ,
db , n >))
-------------------------------
case (1,1,1,1,1,1,1,1,1,2) :
assume: f = a
ba = true
bb = true
da = true
db = true
m = 0
n = 0
hd r = 0
hd r1 = 0
fhd f1 = false
the condition is false: good (f | (< ba , da , m >) | (< bb ,
db , n >))
-------------------------------
case (1,1,1,1,1,1,1,1,2,1) :
assume: f = a
ba = true
bb = true
da = true
db = true
m = 0
n = 0
hd r = 0
(hd r1) > 0 = true
fhd f1 = true
the condition is false: good (f | (< ba , da , m >) | (< bb ,
db , n >))
-------------------------------
case (1,1,1,1,1,1,1,1,2,2) :
assume: f = a
ba = true
bb = true
da = true
db = true
m = 0
n = 0
hd r = 0
(hd r1) > 0 = true
fhd f1 = false
the condition is false: good (f | (< ba , da , m >) | (< bb ,
db , n >))
-------------------------------
..............................
-------------------------------
case (2,2,2,2,2,2,2,2,2,1) :
assume: f = b
ba = false
bb = false
da = false
db = false
m > 0 = true
n > 0 = true
(hd r) > 0 = true
(hd r1) > 0 = true
fhd f1 = true
eq(m, 0) = true
eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r ,
r1 , f1])) == all-true
nf: sys ([(b | (< true , false , (hd r) >) | (< false , false
, n >)) , (tl r) , r1 , (tl f1)]) == all-true
-------------------------------
deduce to : all-true == all-true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r ,
r1 , f1])) == all-true
nf: true
-------------------------------
case (2,2,2,2,2,2,2,2,2,2) :
assume: f = b
ba = false
bb = false
da = false
db = false
m > 0 = true
n > 0 = true
(hd r) > 0 = true
(hd r1) > 0 = true
fhd f1 = false
eq(m, 0) = true
eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r ,
r1 , f1])) == all-true
nf: sys ([(a | (< false , false , m >) | (< true , false ,
(hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true
-------------------------------
deduce to : all-true == all-true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r ,
r1 , f1])) == all-true
nf: true
-----------------------------------------
analyzed 1024 cases, all cases succeeded
condition failed in 576 cases
result: true
c-rewrite time: 264391ms parse time: 96ms
==========================================
close
BOBJ> q
Bye.
awk%
]]>
To the BOBJ Examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Thu Dec 5 12:22:49 PST 2002