[herd]Modeling of R and W event by AMO instruction in Riscv

[curious-whq]

Dear Authors,
Sorry for interrupting you here. I am a newcomer to Herd, I'm encountering some puzzling errors while using herd7 to test litmus tests. I would like to present for your help:
I modified the riscv.cat file and tested it using litmus test.
For riscv.cat, I deleted r3 in ppo and tested it using the following litmus test.

RISCV test
 {0:x5=x; 0:x11=y; 1:x6=y; 1:x8=x; }
          P0           |      P1       ;
ori x7, x0, 2          | ori x5, x0, 2 ;
amoswap.w x6, x7, (x5) | sw x5, 0(x6)  ;
lw x8, 0(x5)           | fence rw, rw  ;
xor x9, x8, x8         | ori x7, x0, 1 ;
ori x10, x0, 1         | sw x7, 0(x8)  ;
add x12, x11, x9       |               ;
sw x10, 0(x12)         |               ;
lw x13, 0(x11)         |               ;

exists (0:x13=2 /\ 0:x6=1 /\ 0:x8=2)

The results are as follows

States 5
0:x6=0; 0:x8=1; 0:x13=1;
0:x6=0; 0:x8=2; 0:x13=1;
0:x6=0; 0:x8=2; 0:x13=2;
0:x6=1; 0:x8=2; 0:x13=1;
0:x6=1; 0:x8=2; 0:x13=2;

But when I also change po-loc-no-w to let po-loc-no-w = po-loc \ (po-loc; [W]; po-loc), the result is as follows

States 4
0:x6=0; 0:x8=1; 0:x13=1;
0:x6=0; 0:x8=2; 0:x13=1;
0:x6=0; 0:x8=2; 0:x13=2;
0:x6=1; 0:x8=2; 0:x13=1;

I express a difference to this result, I think it may be that the R and W events in AMO do not model the po-loc relationship.
I'm also confused when I change po-loc-no-w to let po-loc-no-w = po-loc \ (po-loc; [W]; po-loc) \ (rmw; [W]; po-loc), the result is still four states.
It would be sincerely appreciated if any comments or guidance could be provided. Thank you in advance for your time and great patience!
Yours sincerely,
Haoqi

[maranget]

Hi @curious-whq. Thank you for your interest in herd.

The amoswap instruction generates a RMW event. Such an event is both a read and write, as visible on this diagram (event a:, on the left of image)
A.pdf

Thus, with the original definition of po-loc-no-w as po-loc \ (po-loc?;[W];po-loc) the relation from event a: to event b: is not part of r2 and thus is not part of ppo. With your modification, let po-loc-no-w = po-loc \ (po-loc;[W];po-loc), relation from a: to b: is now part of r2.

Consider that an AMO effect is both a member if the R and W set. As a consequence , "the R and the W events in AMO" cannot be part of po-loc, because this would make po-loc a cyclic relation, which would contradict po-loc being a partial order.

For a better understanding of herd, you can draw execution diagrams, as described in herd manual.