[herd] RISC-V: Enable RCsc ordering for load/store operations

[patrick-rivos]

The Herd7 RISC-V model has support for L{b|h|w|d} S{b|h|w|d} with acq/rel annotations (.aq/.rl/.aqrl) but restricts the RCsc constraint (PPO rule 7 in the ISA manual[1]) to LR/SC/AMO ops. This patch removes that restriction.

This can be seen using the following litmus test:

RISCV rcsc-load-store-issue

{
0:x7=a; 0:x8=b;
1:x7=a; 1:x8=b;
}

 P0               | P1             ;
 ori x1,x0,1      | ori x1,x0,1    ;
 sw.rl x1,0(x8)   | sw.rl x1,0(x7) ;
 lw.aq x2,0(x7)   | lw.aq x5,0(x8) ;

~exists (0:x2=0 /\ 1:x5=0)

Dan Lustig (@daniellustig) noticed the issue and Andrea Parri (@aparri) suggested the fix present in this PR.

Since ZTSO is defined as a delta from RVWMO[2], I changed that model as well.

This issue is becoming more relevant since the RISC-V load/store acquire/release instructions are being proposed by Hans Boehm[3].

[1] https://github.com/riscv/riscv-isa-manual/blob/c9a172ff2245824b0c55b234a3bb45664394d038/src/rvwmo.tex#L132-L140C3
[2] https://github.com/riscv/riscv-isa-manual/blob/c9a172ff2245824b0c55b234a3bb45664394d038/src/ztso.tex#LL5C1-L5C39
[3] https://lists.riscv.org/g/tech-unprivileged/message/382

[maranget]

Hi @patrick-rivos. As I understand the PR, lw.aq and sw.rl are now RCsc. As a consequence the RCpc semantics disappears. However, the memory model text suggests that loads and stores can carry RCpc annotations.

Hence I am a bit confused , why select the RCsc semantics for lw.aq and sw.rl in place of RCpc. Is the choice described in some official document?

[patrick-rivos]

As you pointed out, RVWMO specifies the possibility of loads/stores carrying RCsc or RCpc annotations.
It does not specify what those annotations look like in asm.

So previously Herd7 arbitrarily chose lw.aq and sw.rl to represent RCpc annotations. This was unspecified AFAIK.

The most official document we have at this time is Hans' proposal which specifies lw.aq and sw.rl as RCsc on page 1 under Why load-acquire and store-release are important[3].

I understand if you would prefer to wait for a more official document but the discussion around using RCsc for lw.aq and sw.rl appears unlikely to change.

There is more discussion about lw.aq and sw.rl here[4].

[3] https://lists.riscv.org/g/tech-unprivileged/message/382
[4] https://lists.riscv.org/g/tech-unprivileged/topic/92916241