(**************************************************************** Compiled from @(#)cfs.nw 4.4 - 1998/02/19 Charles Pecheur, INRIA Rhone-Alpes - updated 2023/11/05 ****************************************************************) specification CfsSystem [cfsreq,cfsans,send,rcv,read,write] : noexit type SiteType is Boolean sorts Site opns site1(*! constructor *), site2(*! constructor *), site3(*! constructor *): -> Site _eq_ , _ne_ : Site , Site -> Bool eqns forall x , y : Site ofsort Bool x eq x = true ; x eq y = false ; x ne y = not ( x eq y ) ; endtype type ValType is Boolean sorts Val opns val1(*! constructor *), val2(*! constructor *): -> Val _eq_ , _ne_ : Val , Val -> Bool eqns forall x , y : Val ofsort Bool x eq x = true ; x eq y = false ; x ne y = not ( x eq y ) ; endtype type CfsCallType is Boolean sorts CfsCall opns read(*! constructor *), beginwrite(*! constructor *), endwrite(*! constructor *): -> CfsCall _eq_ , _ne_ : CfsCall , CfsCall -> Bool eqns forall x , y : CfsCall ofsort Bool x eq x = true ; x eq y = false ; x ne y = not ( x eq y ) ; endtype type MessageType is Boolean sorts Message opns readrq(*! constructor *), readok(*! constructor *), writerq(*! constructor *), writeok(*! constructor *), invalidate(*! constructor *), firstmaster(*! constructor *): -> Message _eq_ , _ne_ : Message , Message -> Bool eqns forall x , y : Message ofsort Bool x eq x = true ; x eq y = false ; x ne y = not ( x eq y ) ; endtype type StateType is Boolean sorts State opns master(*! constructor *), writing(*! constructor *), invalid(*! constructor *), valid(*! constructor *), waitread(*! constructor *), waitwrite(*! constructor *), flushrqs(*! constructor *), forwardrqs(*! constructor *), invalwriting(*! constructor *), invalinvalid(*! constructor *): -> State _eq_ , _ne_ : State , State -> Bool eqns forall x , y : State ofsort Bool x eq x = true ; x eq y = false ; x ne y = not ( x eq y ) ; endtype type SiteSetType is SiteType , Boolean, NaturalNumber sorts SiteSet opns cset (*! constructor *) : bool , bool , bool -> SiteSet {} : -> SiteSet insert, remove : Site , SiteSet -> SiteSet min : SiteSet -> Site butmin : SiteSet -> SiteSet _eq_, _ne_ : SiteSet , SiteSet -> Bool eqns forall x, y : SiteSet , x_1 , x_2 , x_3 , y_1 , y_2 , y_3 : Bool, x_0 : Site ofsort SiteSet {} = cset( false , false , false ) ; x_0 = site1 => insert( x_0 , cset( x_1 , x_2 , x_3 )) = cset( true , x_2 , x_3 ) ; x_0 = site2 => insert( x_0 , cset( x_1 , x_2 , x_3 )) = cset( x_1 , true , x_3 ) ; x_0 = site3 => insert( x_0 , cset( x_1 , x_2 , x_3 )) = cset( x_1 , x_2 , true ) ; x_0 = site1 => remove( x_0 , cset( x_1 , x_2 , x_3 )) = cset( false , x_2 , x_3 ) ; x_0 = site2 => remove( x_0 , cset( x_1 , x_2 , x_3 )) = cset( x_1 , false , x_3 ) ; x_0 = site3 => remove( x_0 , cset( x_1 , x_2 , x_3 )) = cset( x_1 , x_2 , false ) ; ofsort Site min(cset( true , x_2 , x_3 )) = site1 ; min(cset( false , true , x_3 )) = site2 ; min(cset( false , false , true )) = site3 ; ofsort SiteSet butmin(x) = remove(min(x), x) ; ofsort Bool cset( x_1 , x_2 , x_3 ) eq cset( y_1 , y_2 , y_3 ) = ( x_1 eq y_1 ) and ( x_2 eq y_2 ) and ( x_3 eq y_3 ) ; x ne y = not(x eq y) ; endtype type PktType is SiteType , Messagetype , Boolean sorts Pkt opns pkt(*! constructor *): Site , Message -> Pkt site : Pkt -> Site msg : Pkt -> Message _eq_ , _ne_ : Pkt , Pkt -> Bool eqns forall x , y : Pkt , x_1 , y_1 : Site , x_2 , y_2 : Message ofsort Site site ( pkt ( x_1 , x_2 ) ) = x_1 ; ofsort Message msg ( pkt ( x_1 , x_2 ) ) = x_2 ; ofsort Bool x_1 eq y_1 , x_2 eq y_2 => pkt ( x_1 , x_2 ) eq pkt ( y_1 , y_2 ) = true ; x eq y = false ; x ne y = not ( x eq y ) ; endtype type PktListType is PktType , Boolean, NaturalNumber sorts PktList (*! implementedby PKTLIST *) opns <> (*! constructor *) : -> PktList _+_ (*! constructor *) : Pkt , PktList -> PktList _+_ : PktList , Pkt -> PktList First: PktList -> Pkt ButFirst: PktList -> PktList _eq_, _ne_ : PktList , PktList -> Bool eqns forall x, y : PktList , x_1, y_1 : Pkt , x_0, y_0 : Nat, a : Bool ofsort PktList <> + x_1 = x_1 + <>; (x_1 + x) + y_1 = x_1 + (x + y_1); ofsort Bool <> of PktList eq <> of PktList = true; <> eq (x_1 + x) = false; (x_1 + x) eq <> = false; x_1 eq y_1 => (x_1 + x) eq (y_1 + y) = x eq y; x_1 ne y_1 => (x_1 + x) eq (y_1 + y) = false; x ne y = not (x eq y) ofsort Pkt First (x_1 + x) = x_1 ; ofsort PktList ButFirst (x_1 + x) = x ; endtype type ValArrayType is ValType , SiteType , Boolean, NaturalNumber sorts ValArray opns array (*! constructor *) : Val , Val , Val -> ValArray set : Site , Val , ValArray -> ValArray get : Site , ValArray -> Val eqns forall x, y : ValArray , x_1 , x_2 , x_3 , y_1 , y_2 , y_3 : Val , x_0 : Site ofsort ValArray x_0 = site1 => set( x_0 , y_1 , array( x_1 , x_2 , x_3 )) = array( y_1 , x_2 , x_3 ) ; x_0 = site2 => set( x_0 , y_2 , array( x_1 , x_2 , x_3 )) = array( x_1 , y_2 , x_3 ) ; x_0 = site3 => set( x_0 , y_3 , array( x_1 , x_2 , x_3 )) = array( x_1 , x_2 , y_3 ) ; ofsort Val x_0 = site1 => get( x_0 , array( x_1 , x_2 , x_3 )) = x_1 ; x_0 = site2 => get( x_0 , array( x_1 , x_2 , x_3 )) = x_2 ; x_0 = site3 => get( x_0 , array( x_1 , x_2 , x_3 )) = x_3 ; endtype type ConstantsType is SiteSetType, PktListType, ValArrayType opns nocopies : -> SiteSet norqs : -> PktList init : -> ValArray eqns ofsort SiteSet nocopies = {} ; ofsort PktList norqs = <> ; ofsort ValArray init = array (val1, val1, val1) ; endtype library Boolean,NaturalNumber endlib behaviour ( GeneralUser [read,write,cfsreq,cfsans] (site1) ||| GeneralUser [read,write,cfsreq,cfsans] (site2) ||| GeneralUser [read,write,cfsreq,cfsans] (site3) ) |[read,write,cfsreq,cfsans]| ( ( Initsite [cfsreq,cfsans,send,rcv] (site1) ||| Initsite [cfsreq,cfsans,send,rcv] (site2) ||| Initsite [cfsreq,cfsans,send,rcv] (site3) ) |[send,rcv]| ( ( rcv ?s1:Site !firstmaster ?s2:Site; ( OutputCell [send,rcv] (site1) ||| OutputCell [send,rcv] (site2) ||| OutputCell [send,rcv] (site3) ) ) |[send]| InitMemory [read,write,send] ) ) where process Site [cfsreq,cfsans,send,rcv] ( s : Site, state : State, copies : SiteSet, rqs : PktList ) : noexit := ( [(state eq master) or (state eq valid) or (state eq invalid)] -> cfsreq !s !read; ( [state eq master] -> cfsans !s !read; Site [cfsreq,cfsans,send,rcv] (s,master,copies,rqs) [] [state eq valid] -> cfsans !s !read; Site [cfsreq,cfsans,send,rcv] (s,valid,copies,rqs) [] [state eq invalid] -> ( send !s !readrq !s; Site [cfsreq,cfsans,send,rcv] (s,waitread,copies,rqs) [] rcv !s !firstmaster !s; cfsans !s !read; Site [cfsreq,cfsans,send,rcv] (s,master,copies,rqs) ) ) ) [] ( [(state eq master) or (state eq valid) or (state eq invalid)] -> cfsreq !s !beginwrite; ( [state eq master] -> cfsans !s !beginwrite; Site [cfsreq,cfsans,send,rcv] (s,invalwriting,copies,rqs) [] [state eq valid] -> send !s !writerq !s; Site [cfsreq,cfsans,send,rcv] (s,waitwrite,copies,rqs) [] [state eq invalid] -> ( send !s !writerq !s; Site [cfsreq,cfsans,send,rcv] (s,waitwrite,copies,rqs) [] rcv !s !firstmaster !s; cfsans !s !beginwrite; Site [cfsreq,cfsans,send,rcv] (s,writing,copies,rqs) ) ) ) [] ( [state eq writing] -> cfsreq !s !endwrite; cfsans !s !endwrite; Site [cfsreq,cfsans,send,rcv] (s,flushrqs,copies,rqs) ) [] ( [(state eq master) or (state eq writing)] -> rcv !s !readrq ?s1:Site; ( [state eq master] -> send !s !readok !s1; Site [cfsreq,cfsans,send,rcv] (s,master,insert(s1,copies),rqs) [] [state eq writing] -> Site [cfsreq,cfsans,send,rcv] (s,writing, copies, rqs+pkt(s1,readrq)) ) ) [] ( [(state eq master) or (state eq writing)] -> rcv !s !writerq ?s1:Site; ( [state eq master] -> send !s !writeok !s1; Site [cfsreq,cfsans,send,rcv] (s,invalinvalid,copies,rqs) [] [state eq writing] -> Site [cfsreq,cfsans,send,rcv] (s,writing, copies, rqs+pkt(s1,writerq)) ) ) [] ( [state eq waitread] -> rcv !s !readok !s; cfsans !s !read; Site [cfsreq,cfsans,send,rcv] (s,valid,copies,rqs) ) [] ( [state eq waitwrite] -> rcv !s !writeok !s; cfsans !s !beginwrite; Site [cfsreq,cfsans,send,rcv] (s,writing,copies,rqs) ) [] ( [ (state eq valid) or (state eq master) or (state eq writing) or (state eq waitwrite) or (state eq waitread) or (state eq invalid)] -> rcv !s !invalidate !s; ( [state eq valid] -> Site [cfsreq,cfsans,send,rcv] (s,invalid,copies,rqs) [] [state ne valid] -> Site [cfsreq,cfsans,send,rcv] (s,state,copies,rqs) ) ) [] ( [state eq flushrqs] -> ( [rqs ne norqs] -> ( [msg(first(rqs)) eq readrq] -> send !s !readok !site(first(rqs)); Site [cfsreq,cfsans,send,rcv] (s, flushrqs, insert(site(first(rqs)),copies), butfirst(rqs)) [] [msg(first(rqs)) eq writerq] -> send !s !writeok !site(first(rqs)); Site [cfsreq,cfsans,send,rcv] (s,forwardrqs,copies,butfirst(rqs)) ) [] [rqs eq norqs] -> Site [cfsreq,cfsans,send,rcv] (s,master,copies,rqs) ) ) [] ( [state eq forwardrqs] -> ( [copies ne nocopies] -> send !s !invalidate !min(copies); Site [cfsreq,cfsans,send,rcv] (s,forwardrqs,butmin(copies),rqs) [] [copies eq nocopies] -> ( [rqs ne norqs] -> send !s !msg(first(rqs)) !site(first(rqs)); Site [cfsreq,cfsans,send,rcv] (s,forwardrqs,copies,butfirst(rqs)) [] [rqs eq norqs] -> Site [cfsreq,cfsans,send,rcv] (s,invalid,copies,rqs) ) ) ) [] ( [state eq invalwriting] -> ( [copies ne nocopies] -> send !s !invalidate !min(copies); Site [cfsreq,cfsans,send,rcv] (s,invalwriting,butmin(copies),rqs) [] [copies eq nocopies] -> Site [cfsreq,cfsans,send,rcv] (s,writing,copies,rqs) ) ) [] ( [state eq invalinvalid] -> ( [copies ne nocopies] -> send !s !invalidate !min(copies); Site [cfsreq,cfsans,send,rcv] (s,invalinvalid,butmin(copies),rqs) [] [copies eq nocopies] -> Site [cfsreq,cfsans,send,rcv] (s,invalid,copies,rqs) ) ) endproc process InitSite [cfsreq,cfsans,send,rcv] ( s : Site ) : noexit := Site [cfsreq,cfsans,send,rcv] (s,invalid,nocopies,norqs) endproc process InitMaster [cfsreq,cfsans,send,rcv] ( s : Site ) : noexit := Site [cfsreq,cfsans,send,rcv] (s,master,nocopies,norqs) endproc process OutputCell [send,rcv] (s : Site) : noexit := send !s ?m:Message ?s1:Site; rcv ?dest:Site !m !s1; OutputCell [send,rcv] (s) endproc process Memory [read,write,ctrl] (mems: ValArray) : noexit := ( choice s:Site [] read !s !get(s, mems) ; Memory [read,write,ctrl] (mems) ) [] write ?s:Site ?v:Val; Memory [read,write,ctrl] (set(s, v, mems)) [] ctrl ?s1:Site ?m:Message ?s2:Site; ( [(m eq readok) or (m eq writeok)] -> Memory [read,write,ctrl] (set(s2, get(s1, mems), mems)) [] [(m ne readok) and (m ne writeok)] -> Memory [read,write,ctrl] (mems) ) endproc process InitMemory [read,write,send] : noexit := Memory [read,write,send] (init of ValArray) endproc process MasterSiteProxy [send,rcv] (s:Site) : noexit := send !s !readrq !s; MasterSiteProxy [send,rcv] (s) [] send !s !writerq !s; MasterSiteProxy [send,rcv] (s) [] rcv !s !readok !s; MasterSiteProxy [send,rcv] (s) [] rcv !s !writeok !s; MasterSiteProxy [send,rcv] (s) [] rcv !s !invalidate !s; MasterSiteProxy [send,rcv] (s) [] (* unreachable branch to prevent CAESAR's warnings about deadlocks; *) (* these warnings correspond to the initial phase of the CFS protocol, *) (* which is not covered in the model generated *) [s ne s (* i.e., false *)] -> rcv !s !firstmaster !s; MasterSiteProxy [send,rcv] (s) endproc process SlaveSiteProxy [send,rcv] (s:Site, other:Site) : noexit := rcv !s !readrq !other; ( send !s !readok !other; SlaveSiteProxy [send,rcv] (s,other) [] send !s !readrq !other; SlaveSiteProxy [send,rcv] (s,other) ) [] rcv !s !writerq !other; ( send !s !writeok !other; SlaveSiteProxy [send,rcv] (s,other) [] send !s !writerq !other; SlaveSiteProxy [send,rcv] (s,other) ) [] send !s !invalidate !other; SlaveSiteProxy [send,rcv] (s,other) endproc process Site3Proxy [send,rcv] (s:Site, other1:Site, other2:Site) : noexit := MasterSiteProxy [send,rcv] (s) ||| SlaveSiteProxy [send,rcv] (s,other1) ||| SlaveSiteProxy [send,rcv] (s,other2) endproc process SlaveSendProxy [send] (s:Site) : noexit := send !s !readrq !s; SlaveSendProxy [send] (s) [] send !s !writerq !s; SlaveSendProxy [send] (s) endproc process MasterSendProxy [send] (s:Site, other:Site) : noexit := send !s !readok !other; MasterSendProxy [send] (s,other) [] send !s !writeok !other; MasterSendProxy [send] (s,other) [] send !s !readrq !other; MasterSendProxy [send] (s,other) [] send !s !writerq !other; MasterSendProxy [send] (s,other) [] send !s !invalidate !other; MasterSendProxy [send] (s,other) endproc process RcvProxy [rcv] (s:Site, other:Site) : noexit := rcv !other !readrq ?z:site; RcvProxy [rcv] (s,other) [] rcv !other !writerq ?z:site; RcvProxy [rcv] (s,other) [] rcv !other !readok !other; RcvProxy [rcv] (s,other) [] rcv !other !writeok !other; RcvProxy [rcv] (s,other) [] rcv !other !readrq !other; RcvProxy [rcv] (s,other) [] rcv !other !writerq !other; RcvProxy [rcv] (s,other) [] rcv !other !invalidate !other; RcvProxy [rcv] (s,other) endproc process Channel3Proxy [send,rcv] (s:Site, other1:Site, other2:Site) : noexit := SlaveSendProxy [send] (s) ||| MasterSendProxy [send] (s,other1) ||| MasterSendProxy [send] (s,other2) ||| RcvProxy [rcv] (s,other1) ||| RcvProxy [rcv] (s,other2) endproc process GeneralUser [read,write,cfsreq,cfsans] (s:Site) : noexit := cfsreq !s !read; cfsans !s !read; ReadingUser [read,write,cfsreq,cfsans] (s) [] cfsreq !s !beginwrite; cfsans !s !beginwrite; WritingUser [read,write,cfsreq,cfsans] (s) endproc process ReadingUser [read,write,cfsreq,cfsans] (s:Site) : noexit := read !s ?v:Val; ReadingUser [read,write,cfsreq,cfsans] (s) [] GeneralUser [read,write,cfsreq,cfsans] (s) endproc process WritingUser [read,write,cfsreq,cfsans] (s:Site) : noexit := read !s ?v:Val; WritingUser [read,write,cfsreq,cfsans] (s) [] write !s ?v:Val; WritingUser [read,write,cfsreq,cfsans] (s) [] cfsreq !s !endwrite; cfsans !s !endwrite; GeneralUser [read,write,cfsreq,cfsans] (s) endproc process Site2with13 [cfsreq,cfsans,send,rcv] : noexit := InitSite [cfsreq,cfsans,send,rcv] (site2) |[send,rcv]| Site3Proxy [send,rcv] (site2,site1,site3) endproc process Site3with12 [cfsreq,cfsans,send,rcv] : noexit := InitSite [cfsreq,cfsans,send,rcv] (site3) |[send,rcv]| Site3Proxy [send,rcv] (site3,site1,site2) endproc process Master1with23 [cfsreq,cfsans,send,rcv] : noexit := InitMaster [cfsreq,cfsans,send,rcv] (site1) |[send,rcv]| Site3Proxy [send,rcv] (site1,site2,site3) endproc process OutputCell1with23 [send,rcv] : noexit := OutputCell [send,rcv] (site1) |[send,rcv]| Channel3Proxy [send,rcv] (site1,site2,site3) endproc process OutputCell2with13 [send,rcv] : noexit := OutputCell [send,rcv] (site2) |[send,rcv]| Channel3Proxy [send,rcv] (site2,site1,site3) endproc process OutputCell3with12 [send,rcv] : noexit := OutputCell [send,rcv] (site3) |[send,rcv]| Channel3Proxy [send,rcv] (site3,site1,site2) endproc endspec