Untitled

{"model":"release_acquire_event_graph","program":"producer: payload=42; store_release(flag,1) / consumer: r=load_acquire(flag); if r==1 read payload","cases":[{"name":"acquire_reads_initial_flag","flag_source":"flag_init","flag_value":0,"payload_atomic":false,"events":{"payload_init":{"thread":"init","op":"plain_write","object":"payload","value":0},"flag_init":{"thread":"init","op":"write","object":"flag","value":0},"payload_store_42":{"thread":"producer","op":"plain_write","object":"payload","value":42},"flag_store_release_1":{"thread":"producer","op":"release_store","object":"flag","value":1},"flag_load_acquire":{"thread":"consumer","op":"acquire_load","object":"flag"}},"po":[["payload_store_42","flag_store_release_1"]],"rf":[["flag_init","flag_load_acquire"]],"sw":[],"hb":[["payload_store_42","flag_store_release_1"]],"payload_read":"not_executed","payload_store_happens_before_payload_load":false,"data_race_if_plain_payload":false},{"name":"acquire_reads_release_flag","flag_source":"flag_store_release_1","flag_value":1,"payload_atomic":false,"events":{"payload_init":{"thread":"init","op":"plain_write","object":"payload","value":0},"flag_init":{"thread":"init","op":"write","object":"flag","value":0},"payload_store_42":{"thread":"producer","op":"plain_write","object":"payload","value":42},"flag_store_release_1":{"thread":"producer","op":"release_store","object":"flag","value":1},"flag_load_acquire":{"thread":"consumer","op":"acquire_load","object":"flag"},"payload_load":{"thread":"consumer","op":"plain_read","object":"payload"}},"po":[["flag_load_acquire","payload_load"],["payload_store_42","flag_store_release_1"]],"rf":[["flag_store_release_1","flag_load_acquire"]],"sw":[["flag_store_release_1","flag_load_acquire"]],"hb":[["flag_load_acquire","payload_load"],["flag_store_release_1","flag_load_acquire"],["flag_store_release_1","payload_load"],["payload_store_42","flag_load_acquire"],["payload_store_42","flag_store_release_1"],["payload_store_42","payload_load"]],"payload_read":42,"payload_store_happens_before_payload_load":true,"data_race_if_plain_payload":false}],"counterexamples":[{"name":"delete_synchronizes_with_edge_for_plain_payload","case":{"flag_source":"flag_store_release_1","flag_value":1,"payload_atomic":false,"events":{"payload_init":{"thread":"init","op":"plain_write","object":"payload","value":0},"flag_init":{"thread":"init","op":"write","object":"flag","value":0},"payload_store_42":{"thread":"producer","op":"plain_write","object":"payload","value":42},"flag_store_release_1":{"thread":"producer","op":"release_store","object":"flag","value":1},"flag_load_acquire":{"thread":"consumer","op":"acquire_load","object":"flag"},"payload_load":{"thread":"consumer","op":"plain_read","object":"payload"}},"po":[["flag_load_acquire","payload_load"],["payload_store_42","flag_store_release_1"]],"rf":[["flag_store_release_1","flag_load_acquire"]],"sw":[],"hb":[["flag_load_acquire","payload_load"],["payload_store_42","flag_store_release_1"]],"payload_read":"undefined_data_race_if_plain_payload","payload_store_happens_before_payload_load":false,"data_race_if_plain_payload":true},"expected_check":"plain payload read must be ordered by happens-before to avoid a C data race","result":"FAILS as intended: this is undefined, not a legal stale-value case"},{"name":"initial_flag_does_not_read_payload","wrong_claim":"payload_read is 0 when flag load reads the initial 0","actual":"not_executed","result":"FAILS as intended"}],"variant_boundary":{"if_payload_were_an_independent_atomic_relaxed_load_without_sw":{"case":{"flag_source":"flag_store_release_1","flag_value":1,"payload_atomic":true,"events":{"payload_init":{"thread":"init","op":"atomic_relaxed_write","object":"payload","value":0},"flag_init":{"thread":"init","op":"write","object":"flag","value":0},"payload_store_42":{"thread":"producer","op":"atomic_relaxed_write","object":"payload","value":42},"flag_store_release_1":{"thread":"producer","op":"release_store","object":"flag","value":1},"flag_load_acquire":{"thread":"consumer","op":"acquire_load","object":"flag"},"payload_load":{"thread":"consumer","op":"atomic_relaxed_read","object":"payload"}},"po":[["flag_load_acquire","payload_load"],["payload_store_42","flag_store_release_1"]],"rf":[["flag_store_release_1","flag_load_acquire"]],"sw":[],"hb":[["flag_load_acquire","payload_load"],["payload_store_42","flag_store_release_1"]],"payload_read":[0,42],"payload_store_happens_before_payload_load":false,"data_race_if_plain_payload":false},"allowed_payload_values":[0,42],"reason":"atomic relaxed removes the C data race but still has no synchronizes-with edge ordering producer payload before the consumer read"}},"claim":"The acquire load carries a plain producer payload write to the consumer only when it reads from the release store and creates sw; without sw the plain-payload example is a data race, while a separate atomic-relaxed payload variant may read either value without ordering."}