[Litmus] Test ISA-DEP-WR-ADDR failed in Litmus 7.56.3. about herdtools7 HOT 8 CLOSED

Thanks, the litmus would help me even more.

from herdtools7.

Ok I found the the test
ISA-DEP-WR-ADDR.

RISCV ISA-DEP-WR-ADDR
(* SC-W to R addr dependency through result register *)
{
0:x5=x; 0:x10=y;
1:x6=y; 1:x9=x;
}
 P0               | P1            ;
 ori x6,x0,1      | ori x5,x0,1   ;
 lr.w x7,0(x5)    | sw x5,0(x6)   ;
 sc.w x8,x6,0(x5) | fence rw,rw   ;
 xor x9,x8,x8     | lw x8,0(x9)  ;
 add x11,x10,x9   |               ;
 lw x5,0(x11)     |               ;
exists
(x=1 /\ 0:x5=0 /\ 1:x8=0)

This test confuses litmus because the register 0:x5 is used both as an address and as a scalar. It can be fixed by renaming the "scalar" x5 into x1 as follows:

RISCV ISA-DEP-WR-ADDR
(* SC-W to R addr dependency through result register *)
{
0:x5=x; 0:x10=y;
1:x6=y; 1:x9=x;
}
 P0               | P1            ;
 ori x6,x0,1      | ori x5,x0,1   ;
 lr.w x7,0(x5)    | sw x5,0(x6)   ;
 sc.w x8,x6,0(x5) | fence rw,rw   ;
 xor x9,x8,x8     | lw x8,0(x9)  ;
 add x11,x10,x9   |               ;
 lw x1,0(x11)     |               ;
exists
(x=1 /\ 0:x1=0 /\ 1:x8=0)

from herdtools7.

Notice that litmus7 could have issued a warning and even reject the test because the two underlying types (int * and int) have different sizes (64 and 32 bits).

from herdtools7.

Hi @Sevwood, thanks for your report.

Would you share the ISA-DEP-WR-ADDR test with us? This would help a lot.

from herdtools7.

Hi @Sevwood, thanks for your report.

Would you share the ISA-DEP-WR-ADDR test with us? This would help a lot.

Hi @maranget

Sure, the attached zip contains two ISA-DEP-WR-ADDR.c generated by litmus 7.56.3 and litmus 7.56.

ISA-DEP-WR-ADDR.zip

Thank you,
Sev.

from herdtools7.

Thanks, the litmus would help me even more.

Hi @maranget

Do you mean you need my litmus7 built by herdtools7?

Thank you,
Sev.

from herdtools7.

Looking at the C files, litmus 7.56.3 found that register x5 of thread P0 holds an address, while litmus 7.56 did not.

Indeed this register holds an address as P0 code includes one store and one load instruction whose effective address is 0(x5). Having the litmus test at hand would help me understand where is 0:x5 coming from. Moreover, if the test has been produced by one of herdtools generators, it may be that the generator is buggy, So having the whole story would help to understand where the problem is.

from herdtools7.

Thank you so much, I will try this solution later.

from herdtools7.