{"model":"lrsc_atomic_increment_retry","trace":[{"attempt":1,"op":"lr","hart":"T0","read":0,"intended_sc_value":1},{"attempt":1,"op":"interfering_atomic_rmw","hart":"T1","read":0,"write":1,"invalidates_t0_reservation":true},{"attempt":1,"op":"sc","hart":"T0","success":false,"observed_value":1},{"attempt":2,"op":"lr","hart":"T0","read":1,"intended_sc_value":2},{"attempt":2,"op":"sc","hart":"T0","success":true,"write":2}],"final":{"value":2,"attempts":2,"successful_t0_increment":true},"no_retry_counterexample":{"initial":0,"t0_lr_read":0,"t1_atomic_rmw_write":1,"t0_sc_success":false,"final_without_retry":1,"lost_t0_increment":true},"claim":"The retry loop preserves the intended increment after one interfering atomic RMW; this finite success does not prove lock-free progress for arbitrary executions.","boundaries":["SC failure after interference is allowed and must be retried when the operation is meant to complete.","Atomicity of the increment comes from the successful LR/SC pair or an AMO/CAS-style read-modify-write, not from a plain load followed by a plain store.","Ordering and forward-progress guarantees are separate from this single-location atomicity case."]}
