LR/SC reservation is based on virtual addresses not physical

[Timmmm]

Currently LR/SC reservation is done using virtual addresses:

        if match_reservation(vaddr) == false then {

And there is this comment:

/* We could set load-reservations on physical or virtual addresses.
 * For now we set them on virtual addresses, since it makes the
 * sequential model of SC a bit simpler, at the cost of an explicit
 * call to load_reservation in LR and cancel_reservation in SC.
 */

However I don't think this is correct. The spec says:

Following this model, in systems with memory translation, an SC is allowed to succeed if
the earlier LR reserved the same location using an alias with a different virtual address,
but is also allowed to fail if the virtual address is different.

However just matching on virtual addresses means that in theory you can get a successful SC for a physical address that was never reserved:

1. LR 0x100 (physical address 0x500)
2. Change memory mapping
3. SC 0x100 (physical address 0x900) - this will succeed!

I think the model may be saved by the fact that the reservation is cancelled on all exceptions and traps, so the page fault from changing the memory map would clear the reservation. But it's very implicit and frankly seems like it just works through chance.

IMO it should switch to using physical addresses. This be necessary anyway so that RsrvNone memory regions can cause an access fault (though helpfully the spec does not say anything at all about how RsrvNone is supposed to work).

[jrtc27]

My understanding is the spec permits the behaviour you believe to be a problem.

[Alasdair]

The paragraph you cite seems to only talk about what happens when you switch the VA but keep the same PA, whereas your example is switching the PA keeping the same VA.

There is currently (as far as I am aware) no formal semantics for how the memory model interacts with virtual memory in RISC-V, so as soon as you change the memory mapping (without manually invalidating the LR beforehand) I suspect all bets are likely off. We did create such a model for Arm, and you can see it in all it's gory detail here if you are interested: https://arxiv.org/abs/2203.00642

For our RVWMO axiomatic concurrency modelling, note that load_reservation and cancel_reservation are no-ops, and match_reservation is just non-deterministic choice. As such they do not use the vaddr argument, which makes sense as I think the spec is being intentionally vague about how you implement the reservation set in hardware to allow both physical and virtual addresses, and the axiomatic model has access to everything it needs to know about the LR/SC pairs from the memory events anyway. I'm not familiar enough with the operational model to know why these functions were added and use specifically virtual addresses.

[Timmmm]

Update based on the discussion in the last meeting:

1. Multicore doesn't really work if you use virtual addresses.
2. It's unlikely that any real cores are using virtual addresses.
3. Because the Sail model uses virtual addresses it calls cancel_reservation() in a few places where the spec doesn't require it to (WFI, traps, xRET). This complicates verification of LR/SC. In our testing we assume the Sail model SC always succeeds if it should be able to, but because of the extra cancellations that isn't quite true.

Therefore it probably makes sense to switch to physical addresses. We will implement this. If it isn't too painful we'll add a flag so you can choose. Also @allenjbaum said he was going to ask some people about it but I'm afraid I forgot who.

[allenjbaum]

Ah, thanks for the reminder. I was going to ask some Rivos and Ventana people. I think one of them has a virtually indexed cache, though I could be mistaken. I'm not sure I believe multicore simply doesn't work. It might not be cheap to make it work (e.g. duplicate tags: one used for outgoing requests, one used of incoming snoops, which is what would trigger reservation loss) but I think it works.

…

On Thu, Jan 11, 2024 at 5:32 AM Tim Hutt ***@***.***> wrote: Update based on the discussion in the last meeting: 1. Multicore doesn't really work if you use virtual addresses. 2. It's unlikely that any real cores are using virtual addresses. 3. Because the Sail model uses virtual addresses it calls cancel_reservation() in a few places where the spec doesn't require it to (WFI, traps, xRET). This complicates verification of LR/SC. In our testing we assume the Sail model SC always succeeds if it should be able to, but because of the extra cancellations that isn't quite true. Therefore it probably makes sense to switch to physical addresses. We will implement this. If it isn't too painful we'll add a flag so you can choose. Also @allenjbaum <https://github.com/allenjbaum> said he was going to ask some people about it but I'm afraid I forgot who. — Reply to this email directly, view it on GitHub <#360 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJXZ77U5VBANDPSOMRLYN7SXVAVCNFSM6AAAAAA7ZMI3JOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQOBXGE3TCOBRHA> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[allenjbaum]

The answer is: Architecturally the reservation is in terms of a PA, just like the memory model itself (and cannot be in terms of a VA - which would lead to aliasing issues). A virtually-indexed cache can work just fine if the point of coherency is at an outer level that is physically indexed (and where the reservation is maintained) On Fri, Jan 12, 2024 at 12:01 AM Allen Baum ***@***.***> wrote:

…

Ah, thanks for the reminder. I was going to ask some Rivos and Ventana people. I think one of them has a virtually indexed cache, though I could be mistaken. I'm not sure I believe multicore simply doesn't work. It might not be cheap to make it work (e.g. duplicate tags: one used for outgoing requests, one used of incoming snoops, which is what would trigger reservation loss) but I think it works. On Thu, Jan 11, 2024 at 5:32 AM Tim Hutt ***@***.***> wrote: > Update based on the discussion in the last meeting: > > 1. Multicore doesn't really work if you use virtual addresses. > 2. It's unlikely that any real cores are using virtual addresses. > 3. Because the Sail model uses virtual addresses it calls > cancel_reservation() in a few places where the spec doesn't require > it to (WFI, traps, xRET). This complicates verification of LR/SC. In our > testing we assume the Sail model SC always succeeds if it should be able > to, but because of the extra cancellations that isn't quite true. > > Therefore it probably makes sense to switch to physical addresses. We > will implement this. If it isn't too painful we'll add a flag so you can > choose. Also @allenjbaum <https://github.com/allenjbaum> said he was > going to ask some people about it but I'm afraid I forgot who. > > — > Reply to this email directly, view it on GitHub > <#360 (comment)>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AHPXVJXZ77U5VBANDPSOMRLYN7SXVAVCNFSM6AAAAAA7ZMI3JOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQOBXGE3TCOBRHA> > . > You are receiving this because you were mentioned.Message ID: > ***@***.***> >

[Timmmm]

Thanks Allan! Is that answer on a mailing list somewhere we can link to for posterity?

[allenjbaum]

As noted, in an email to me. Note in this specific case, the L1 cache is physically indexed, but reservations are still PAs.

…

On Saturday, January 13, 2024, Tim Hutt ***@***.***> wrote: Thanks Allan! Is that answer on a mailing list somewhere we can link to for posterity? — Reply to this email directly, view it on GitHub <#360 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJXKUHGH345MSLTWF33YOKLMRAVCNFSM6AAAAAA7ZMI3JOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQOJQGQ3TINBWGY> . You are receiving this because you were mentioned.Message ID: ***@***.***>