--- SYNAPSE CACHE COHERENCE PROTOCOL --- Last version: May 16, 2000 var invalid,valid,dirty: discrete; automaton p synclabs : ; initially ss & True; loc ss : while invalid >= 0 & dirty >=0 & valid >= 0 wait {} -- -- READ HIT -- when dirty+valid >=1 do {} goto ss; -- -- READ MISS -- when invalid >= 1 do { invalid'=invalid+dirty-1, valid'=valid+1, dirty'=0 } goto ss; -- -- WRITE HIT -- when valid >=1 do { dirty'=1, valid'=0, invalid'=invalid+dirty+valid-1 } goto ss; when dirty >=1 do {} goto ss; -- -- WRITE MISS -- when invalid >=1 do { dirty'=1, valid'=0, invalid'=invalid+dirty+valid-1 } goto ss; -- -- REPLACEMENT -- when dirty >=1 do { invalid'=invalid+1,dirty'=dirty-1 } goto ss; when valid >=1 do { invalid'=invalid+1,valid'=valid-1 } goto ss; end var init_reg, final_reg1, final_reg2, final_reg, reached : region; init_reg := invalid >=1 & valid = 0 & dirty = 0; final_reg1 := dirty >= 2; final_reg2 := valid >= 1 & dirty >= 1 ; final_reg := final_reg1 | final_reg2; reached:= reach backward from final_reg endreach; if empty(reached & init_reg) then prints "Target not reached (safety hold!)"; print reached; else prints "Target reached (safety does not hold!)"; endif;