{"model":"explicit_store_buffer","allowed_outcome":{"r0":0,"r1":0},"trace":["T0: buffer x=1","T1: buffer y=1","T0: r0=load memory y->0","T1: r1=load memory x->0","T0: flush x=1","T1: flush y=1"],"note":"Shows coherence per location does not imply cross-address sequential consistency."}
