--- BERKELEY CACHE COHERENCE PROTOCOL --- Last version: May 16, 2000 var invalid,unowned,nonexclusive,exclusive: discrete; p : parameter; automaton p synclabs : ; initially ss & True; loc ss : while invalid >= 0 & exclusive >=0 & nonexclusive >= 0 & unowned >=0 wait {} -- -- READ HIT -- when exclusive+nonexclusive+unowned >= 1 do {} goto ss; -- -- READ MISS -- when invalid >= 1 do { invalid'=invalid-1, unowned'=unowned+1, nonexclusive'=nonexclusive+exclusive, exclusive'=0 } goto ss; -- -- WRITE HIT -- when nonexclusive+unowned >=1 do { nonexclusive'=0, unowned'=0, invalid'=unowned+invalid+nonexclusive-1, exclusive'=exclusive+1 } goto ss; -- -- WRITE MISS -- when invalid >= 1 do { invalid'=invalid+unowned+exclusive+nonexclusive-1, unowned'=0, nonexclusive'=0, exclusive'=1 } goto ss; -- -- REPLACEMENT -- when exclusive >=1 do { invalid'=invalid+1,exclusive'=exclusive-1 } goto ss; when nonexclusive >= 1 do { invalid'=invalid+1,nonexclusive'=nonexclusive-1 } goto ss; when unowned >=1 do { invalid'=invalid+1,unowned'=unowned-1 } goto ss; end var init_reg, final_reg, final_reg1, final_reg2, final_reg3, final_reg4, reached: region; init_reg := invalid >=1 & nonexclusive=0 & unowned = 0 & exclusive = 0; final_reg1 := exclusive >= 2; final_reg2 := unowned+nonexclusive >= 1 & exclusive >= 1 ; final_reg := final_reg1 | final_reg2; reached:= reach backward from final_reg endreach; if empty(reached & init_reg) then print reached; prints "=================================== "; prints "SAFETY HOLD!"; prints "=================================== "; else print reached; prints " "; prints "SAFETY DOES NOT HOLD!"; endif;