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