[herd]Modeling the X relation and how the Lr instruction is represented in riscv.cat

[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 added two PPOs: r14 = [R];po;[X], r15 = [X];po;[W] and tested it using the following litmus test.

RISCV ISA03+SIMPLE
(* ISA V2.3, Fig 1.3, spinlock, adapt, test mutual exclusion *)
{
0:a0=lock; 0:a5=a;
1:a0=lock; 1:a5=a;
}
 P0                      | P1                      ;
 li t0,1                 | li t0,1                 ;
 amoswap.w.aq t0,t0,(a0) | amoswap.w.aq t0,t0,(a0) ;
 lw t1,0(a5)             | lw t1,0(a5)             ;
 addi t1,t1,1            | addi t1,t1,1            ;
 sw t1,0(a5)             | sw t1,0(a5)             ;
 amoswap.w.rl x0,x0,(a0) | amoswap.w.rl x0,x0,(a0) ;

filter (0:t0=0 /\ 1:t0=0)
forall (a=2)

The results are as follows

Test ISA03+SB02 Allowed
States 3
0:x7=0; 1:x7=0;
0:x7=0; 1:x7=1;
0:x7=1; 1:x7=0;

But when I change r14 = [R];po;[Sc], r15 = [Sc];po;[W] the result is as follows

Test ISA03+SB02 Allowed
States 4
0:x7=0; 1:x7=0;
0:x7=0; 1:x7=1;
0:x7=1; 1:x7=0;
0:x7=1; 1:x7=1;

I don't understand the difference between X and Sc, and I'm also confused about why X would react to AMO instructions?And when I replace X with Sc, it seems that it no longer recognizes the Sc instruction either?
I would like to know where I can find the relations that can be used in RISC-V. Also, how is the Lr instruction represented in riscv.cat?
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. Something looks wrong in your message: the executed test (ISA03+SB02) is not the test that is presented (ISA03+SIMPLE).

[curious-whq]

@maranget
I'm very sorry for the mistakes in my question, which led to some typos. In fact, I was referring to ISA03+SB02.litmus. Here is my supplement.
ISA03+SB02.litmus

RISCV ISA03+SB02

(* ISA V2.3, Fig 1.3, spinlock, adapt, test non-SC SB *)

{
0:a0=z; 0:a1=x; 0:a2=y;
1:a0=z; 1:a1=x; 1:a2=y;
}
 P0                      | P1                      ;
 li t0,1                 | li t0,1                 ;
 amoswap.w    t0,t0,(a0) | amoswap.w    t0,t0,(a0) ;
 li t1,1                 | li t1,1                 ;
 sw t1,0(a1)             | sw t1,0(a2)             ;
 lw t2,0(a2)             | lw t2,0(a1)             ;
 amoswap.w    x0,x0,(a0) | amoswap.w    x0,x0,(a0) ;


filter (0:t0=0 /\ 1:t0=0)
exists (0:t2=0 /\ 1:t2=0)

I sincerely apologize for any confusion I have caused, but I still genuinely hope to receive your guidance. Thank you in advance once again!
Yours sincerely,
Haoqi

[maranget]

Hi @curious-whq . To answer your questions:

• X is the set of "atomic" accesses, that is the read. write or RMW (read-modify-write, generated by AMO instructions). Atomic reads are also generated by the load-reserve instruction and atomic writes by the store conditional instruction.
• Sc is the set of accesses with Sc semantics. At the moment, **herd7** does not implement instructions that generate such accesses. Hence the Sc` set is always empty.

This should explain your results. Notice that your test ISA03+SB02 is a SB test where the code of each thread is intended to be in a (simplified) critical section. the amoswap.w instructions acting either as some kind of lock or unlock primitive. However the lacks memory order annotations. As a consequence code sequences somehow mix and the sequences are not serialised. To restrict execution to "all P0 first; then all P1" or "all P1 first; then all P0" one can use the "AcqRel" memory order., by adding the annotation aqrl to the amoswap.w instructions. Namely:

RISCV SB+LOCKED

(* ISA V2.3, Fig 1.3, spinlock, adapt, test SC SB *)

{
0:a0=z; 0:a1=x; 0:a2=y;
1:a0=z; 1:a1=x; 1:a2=y;
}
 P0                           | P1                           ;
 li t0,1                      | li t0,1                      ;
 amoswap.w.aqrl    t0,t0,(a0) | amoswap.w.aqrl    t0,t0,(a0) ;
 li t1,1                      | li t1,1                      ;
 sw t1,0(a1)                  | sw t1,0(a2)                  ;
 lw t2,0(a2)                  | lw t2,0(a1)                  ;
 amoswap.w.aqrl    x0,x0,(a0) | amoswap.w.aqrl    x0,x0,(a0) ;


filter (0:t0=0 /\ 1:t0=0)
exists (0:t2=0 /\ 1:t2=0)

This is how herd7 is operating. I am not completely comfortable about how this use of the aqrl annotation relates to the memory order specifications of the ISA. PR #576 may be worth looking at.

[maranget]

Notice that PR #576 is still not merged yet.