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

*** 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