About the counter-intuitive herd7 simulation result for CoRW1+fence.rw.rwspx.litmus

[DehengYang]

Hi,
Sorry for interrupting here. I have encountered a counter-intuitive issue when running herd7 on two litmus tests:

For SC-FAIL.litmus, herd7 simulated only one state, i.e., it infers that the sc.w instruction must fail. This is understandable as the lr.w reads the value of address x2 rather than address x3.

RISCV SC-FAIL
(* lr and sc are to different addresses, Forbid *)
{
0:x2=x; 0:x3=y;
}
 P0               ;
 ori x6,x0,1      ;
 lr.w x7,0(x2)    ;
 sc.w x8,x6,0(x3) ;
forall (y=0 /\ 0:x8=1)

However, for CoRW1+fence.rw.rwspx, herd7 simulated two states, where it assumes the sc.w may succeed or fail.
I cannot understand why the sc.w could fail, because lr.w reads the same address of sc.w and there is not other threads corrupting the data of x6. So this seems a bit counter-intuitive. It would be greatly appreciated if any guidance or comments could be provided to help me understand this case. Thank you!

RISCV CoRW1+fence.rw.rwspx
"Fence.rw.rwsRWPX RfeXP"
Cycle=Fence.rw.rwsRWPX RfeXP
Relax=Fence.rw.rwsRWPX
Safe=Rfe
Generator=diy7 (version 7.51+4(dev))
Prefetch=
Com=Rf
Orig=Fence.rw.rwsRWPX RfeXP
{
0:x6=x; 0:x7=1;
}
 P0               ;
 lw x5,0(x6)      ;
 fence rw,rw      ;
 lr.w x8,0(x6)    ;
 sc.w x9,x7,0(x6) ;
exists (0:x5=0 /\ 0:x8=0 /\ 0:x9=1 /\ x=0)

Thank you in advance for the great help and support. Wish you a nice day:)

Yours sincerely,
Deheng

[maranget]

Hi @DehengYang. I do not know about specific behaviour guarantee for this RISCV.

However, generally speaking, store conditional may fail for just any reason. Here is a naive scenario:

The running thread is scheduled out just after the load-reserve instruction has been executed. In such a case, the reservation is likely to be cancelled.

The scenario is naive. If (1) the store conditional instruction immediately follows the load reserve instruction and (2) that the reserved memory it is certain not to be accessed that any other thread, then it may be the case that the store conditional will always succeed. Yet, I doubt that official documentation would say that. Moreover, would it be the case, I am not sure we would implement such a particular case.

Hope it helps.

[DehengYang]

Hi @maranget ,

Thank you so much for the detailed explanation and analysis that perfectly solves my confusion.

Many thanks and wish you a great week!

Yours sincerely,
Deheng