how does the flat model enforce coherence on reads

[aa755]

Is it possible that in thread 1, the register x2 has value 2 and x1 has value 4? if not, how does the flat model (the operation model as described in  Section 6.2-6.5 of the paper Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8) rule it out? The description there of reading from memory seems simple:

[bensimner]

Flat indeed allows you to satisfy the two reads out-of-order, and this is required e.g. for the RSW test. If the out-of-order satisfaction would violate coherence, because the earlier load was satisfied second with a newer write, then this is fixed on the satisfaction of the first load by the 'Satisfy memory read' transition's second action ("restart any speculative instructions ...") which will restart any overlapping po-later instructions which have not yet finished (e.g. because po-earlier instructions are still in-flight) but have already satisfied from an earlier write, and their dependents.

So the trace of transitions is roughly:

1. Fetch i1 = "load reg x1 from addr 1000"
2. Fetch i2 = "load reg x2 from addr 1000"
3. Satisfy memory read of i2, with value 2
4. [Thread 2] Propagate write of 4 to addr 1000
5. Satisfy memory read of i1, with value 4 (forcing restart of i2)
6. Satisfy memory read of i2, with value 4
7. Finish i1
8. Finish i2

Hence, x2=2 and x1=4 is forbidden. See also the CoRR0 and RDW litmus tests.

[PeterSewell]

You should be able to see that trace in rmem ( https://www.cl.cam.ac.uk/~sf502/regressions/rmem/).

On Wed, 10 Jan 2024 at 17:17, Ben Simner @.***> wrote:

Flat indeed allows you to satisfy the two reads out-of-order, and this is required e.g. for the RSW test. If the out-of-order satisfaction would violate coherence, because the earlier load was satisfied second with a newer write, then this is fixed on the satisfaction of the first load by the 'Satisfy memory read' transition's second action ("restart any speculative instructions ...") which will restart any overlapping po-later instructions which have not yet finished (e.g. because po-earlier instructions are still in-flight) but have already satisfied from an earlier write, and their dependents.

So the trace of transitions is roughly:

1. Fetch i1 = "load reg x1 from addr 1000"
2. Fetch i2 = "load reg x2 from addr 1000"
3. Satisfy memory read of i2, with value 2
4. [Thread 2] Propagate write of 4 to addr 1000
5. Satisfy memory read of i1, with value 4 (forcing restart of i2)
6. Satisfy memory read of i2, with value 4
7. Finish i1
8. Finish i2

Hence, x2=2 and x1=4 is forbidden. See also the CoRR0 and RDW litmus tests.

— Reply to this email directly, view it on GitHub https://github.com/rems-project/rmem/issues/25#issuecomment-1885270894, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZVNGS3SLKPN46D2GNDYN3EL3AVCNFSM6AAAAABBUZWVBWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQOBVGI3TAOBZGQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>