--- IEEE FUTUREBUS+ CACHE COHERENCE PROTOCOL var invalid, sharedU, exclusiveU, exclusiveM, pendingR, pendingW, pendingEMR, pendingEMW, pendingSU: discrete; automaton p synclabs : ; initially ss & True; loc ss: while invalid >= 0 & sharedU >=0 & exclusiveU >= 0 & exclusiveM >=0 & pendingR >= 0 & pendingW >= 0 & pendingEMR >= 0 & pendingEMW >= 0 & pendingSU >= 0 wait {} when sharedU+exclusiveU+exclusiveM>=1 do {} goto ss; when invalid >= 1 & pendingW=0 do { invalid'=invalid-1, sharedU'=0, exclusiveU'=0, exclusiveM'=0, pendingR'=pendingR+1, pendingEMR'=pendingEMR+exclusiveM, pendingSU'=pendingSU+sharedU+exclusiveU } goto ss; when pendingEMR >=1 do { pendingR'=0, pendingEMR'=pendingEMR-1, sharedU'=sharedU+pendingR+1 } goto ss; when pendingSU>=1 do { pendingR'=0, sharedU'=sharedU+pendingR+pendingSU, pendingSU'=0 } goto ss; when pendingR >= 2 & pendingSU=0 & pendingEMR=0 do { pendingR'=0, sharedU'=sharedU+pendingR } goto ss; when pendingR = 1 & pendingSU=0 & pendingEMR=0 do { pendingR'=0, exclusiveU'=exclusiveU+1 } goto ss; --- --- WRITE MISS --- --- pendingW=0 is optional --- when invalid >= 1 & pendingW=0 do { invalid'=invalid+exclusiveU+sharedU+pendingSU+pendingR+pendingEMW+pendingEMR-1, pendingW' = 1, pendingEMW' = exclusiveM, sharedU' = 0, exclusiveU' = 0, exclusiveM' = 0, pendingR' = 0, pendingEMR' = 0, pendingSU' = 0 } goto ss; when pendingEMW >=1 do { pendingW'=0, exclusiveM'=exclusiveM+pendingW, invalid'=invalid+1, pendingEMW'=pendingEMW-1 } goto ss; when pendingW >= 1 & pendingEMW =0 do { exclusiveM'=exclusiveM+pendingW, pendingW'=0 } goto ss; --- --- WRITE HITS --- --- when exclusiveM>=1 do { } goto ss; when exclusiveU>=1 do { exclusiveU'=exclusiveU-1, exclusiveM'=exclusiveM+1 } goto ss; when sharedU>=1 do { invalid'=invalid+sharedU-1, sharedU'=0, exclusiveM'=exclusiveM+1 } goto ss; end var init_reg, final_reg, final_reg1, reached, old, new, Aux : region; init_reg := loc[p]=ss & invalid >= 1 & sharedU = 0 & exclusiveU = 0 & exclusiveM = 0 & pendingR = 0 & pendingW = 0 & pendingEMR = 0 & pendingEMW = 0 & pendingSU = 0; final_reg := invalid >= 0 & sharedU >= 1 & exclusiveU+exclusiveM >= 1 & pendingR >= 0 & pendingW >= 0 & pendingEMR >= 0 & pendingEMW >= 0 & pendingSU >= 0 | invalid >= 0 & sharedU >= 0 & exclusiveU+exclusiveM >= 2 & pendingR >= 0 & pendingW >= 0 & pendingEMR >= 0 & pendingEMW >= 0 & pendingSU >= 0; final_reg1 := invalid >= 0 & sharedU >= 0 & exclusiveU >= 0 & exclusiveM >= 0 & pendingR >= 1 & pendingW >= 1 & pendingEMR >= 0 & pendingEMW >= 0 & pendingSU >= 0 | invalid >= 0 & sharedU >= 0 & exclusiveU >= 0 & exclusiveM >= 0 & pendingR >= 0 & pendingW >= 2 & pendingEMR >= 0 & pendingEMW >= 0 & pendingSU >= 0 ; reached:= reach backward from final_reg endreach; print reached; prints " "; prints " "; if empty(reached & init_reg) then prints "SAFE!"; else prints "WARNING: UNSAFE!"; endif;