--- BERKELEY CACHE COHERENCE PROTOCOL --- [Delzanno 2003] --- VS 10/7/2007 - MP 22/11/2007 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 MISS -- rm when invalid >= 1 do { invalid'=invalid-1, unowned'=unowned+1, nonexclusive'=nonexclusive+exclusive, exclusive'=0 } goto ss; -- -- READ HIT -- rh when exclusive + nonexclusive + unowned >= 1 do { } goto ss; -- -- WRITE MISS -- wm when invalid >= 1 do { invalid'=invalid+unowned+exclusive+nonexclusive-1, unowned'=0, nonexclusive'=0, exclusive'=1 } goto ss; -- -- WRITE HIT -- rh1 when nonexclusive+unowned >=1 do { nonexclusive'=0, unowned'=0, invalid'=unowned+invalid+nonexclusive-1, exclusive'=exclusive+1 } goto ss; -- rh2 when exclusive >= 1 do { } 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 := unowned+nonexclusive >= 1 & exclusive >= 1 ; final_reg2 := exclusive >= 2; final_reg := final_reg1 | final_reg2; reached:= reach backward from final_reg endreach; if empty(reached & init_reg) then prints "Target not reached (safety holds!)"; print reached; else prints "Target reached (safety does not hold!)"; endif; -- reached:= reach forward from init_reg endreach; -- if empty(reached & final_reg) -- then prints "Target not reached (safety holds!)"; -- print reached; -- else prints "Target reached (safety does not hold!)"; -- endif;