Maybe wrong fr edge in litmus sample?

[GTwhy]

In the provided litmus test sample, the edge c -fr-> a indicates that event c precedes a. However, a is not a co-successor of c, and c reads the value 1 from a within this example.

Could this be a mistake, or is there a logical explanation for this apparent inconsistency?

Thanks! @wmat

[wmat]

@Andrew Waterman @.***> can you comment here? This litmus test image is copied directly from the published version of the spec.

On Tue, Mar 19, 2024 at 3:27 AM Hengyu Wang 王恒宇 @.***> wrote:

In the provided litmus test sample https://github.com/riscv/riscv-isa-manual/blob/riscv-isa-release-157641b-2024-03-12/src/images/graphviz/litmus_sample.png, the edge c -fr-> a indicates that event c precedes a. However, a is not a co-successor of c, and c reads the value 1 from a within this example.

Could this be a mistake, or is there a logical explanation for this apparent inconsistency?

Thanks! @wmat https://github.com/wmat

image.png (view on web) https://github.com/riscv/riscv-isa-manual/assets/32484423/b3717ea1-b83b-47ea-b59a-ea9bb779cba1

— Reply to this email directly, view it on GitHub https://github.com/riscv/riscv-isa-manual/issues/1269, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAN6ZGGG3IWQWHKW5CHJFDYY7SFHAVCNFSM6AAAAABE47STN2VHI2DSMVQWIX3LMV43ASLTON2WKOZSGE4TIMRSHEZTSMY . You are receiving this because you were mentioned.Message ID: @.***>

[aswaterman]

I'll leave it to the memory-model folks lurking on this list to explain the conventions here.