herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
228 stars 65 forks source link

[gen] allow address dependencies landing on code location #1031

Closed hugookeeffe closed 1 week ago

hugookeeffe commented 3 weeks ago

This PR allows address dependencies to land on code locations when DC's or IC's are present only. This is necessary to allow tests such as the following to be generated:

AArch64 MP.RF+dmb.st+addr-dc.cvau-dsb.ish-ic.ivau-dsb.ish-isb
Variant=ifetch
{
  0:X0=instr:"NOP";
  0:X1=P1:L0; 1:X1=P1:L0;
  0:X3=y; 1:X3=y;
  1:X9=0;
}
 P0          | P1                ;
 STR W0,[X1] | LDR W2,[X3]       ;
 DMB ST      | EOR W6,W2,W2      ;
 MOV W2,#1   | ADD X1,X1,W6,SXTW ;
 STR W2,[X3] | DC CVAU,X1        ;
             | DSB ISH           ;
             | IC IVAU,X1        ;
             | DSB ISH           ;
             | ISB               ;
             |L0:                ;
             | B over            ;
             | MOV W9,#1         ;
             |over:              ;
exists 1:X2=1 /\ 1:X9=0

This PR allows a very similar test to be generated, with the following command and output: diyone7 -arch AArch64 -variant self -moreedges true "DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB FreIP"

AArch64 A
"DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB FreIP"
Generator=diyone7 (version 7.57+1)
Com=Rf Fr
Orig=DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB FreIP
{
0:X0=instr:"NOP"; 0:X1=P1:Lself00; 0:X3=x;
1:X0=x; 1:X3=P1:Lself00;
}
 P0          | P1                ;
 STR W0,[X1] | LDR W1,[X0]       ;
 DMB ISH     | EOR W2,W1,W1      ;
 MOV W2,#1   | ADD X3,X3,W2,SXTW ;
 STR W2,[X3] | DC CVAU,X3        ;
             | DSB ISH           ;
             | IC IVAU,X3        ;
             | DSB ISH           ;
             | ISB               ;
             | Lself00:          ;
             | B .+12            ;
             | MOV W4,#2         ;
             | B .+8             ;
             | MOV W4,#1         ;
exists (1:X1=1 /\ 1:X4=1)

an important note here is the change in the code to make the first two registers of the Add instruction point to the code location, this is necessary to create forbidden tests.

hugookeeffe commented 3 weeks ago

this PR has been tested by running diy7 with forbidden_ifetch.conf in gen/libdir/ which succesfully generated desired tests such as the one mentioned above. Furthermore the tests were ran through herd7, with the following PR cherrypicked https://github.com/herd/herdtools7/pull/952, showing all tests as forbidden. It was important to use this PR as it necessary to forbid tests where dependencies land on DC/IC

artkhyzha commented 3 weeks ago

Thank you for writing up the explanations, Hugo. If I understand correctly, this increases the number of forbidden tests the previous PR generates. Looks good to me!

hugookeeffe commented 3 weeks ago

@maranget do you have any thoughts on this PR? From the generated tests I looked at, I couldn't see anything wrong but perhaps I missed something

relokin commented 3 weeks ago

Thanks Hugo. The code looks good to me. I only have on comment how does diyone7 respond if I change DC.CVAUn to DC.CVAUp, like so:

diyone7 -arch AArch64 -variant self -moreedges true "DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUp DSB.ISH IC.IVAUp DSB.ISH ISB FreIP

I would expect this to produce an error.

hugookeeffe commented 3 weeks ago

thank you @relokin for pointing that out. Indeed this wouldn't produce an error when it should. I have just pushed a new commit that makes sure the error is thrown when DC.CVAU is pointing to the previous register

maranget commented 3 weeks ago

Hi @hugookeeffe, @artkhyzha and @relokin. Code is fine, with minimal intervention :).

Out of curiosity, I had the idea to have one p and one n...

% diyone7 -arch AArch64 -variant self -moreedges true "DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUn DSB.ISH IC.IVAUp DSB.ISH ISB FreIP"
AArch64 A
"DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUn DSB.ISH IC.IVAUp DSB.ISH ISB FreIP"
Generator=diyone7 (version 7.57+1)
Com=Rf Fr
Orig=DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUn DSB.ISH IC.IVAUp DSB.ISH ISB FreIP
{
0:X0=instr:"NOP"; 0:X1=P1:Lself00; 0:X3=x;
1:X0=x; 1:X3=P1:Lself00;
}
 P0          | P1                ;
 STR W0,[X1] | LDR W1,[X0]       ;
 DMB ISH     | EOR W2,W1,W1      ;
 MOV W2,#1   | ADD X3,X3,W2,SXTW ;
 STR W2,[X3] | DC CVAU,X3        ;
             | DSB ISH           ;
             | IC IVAU,X0        ;
             | DSB ISH           ;
             | ISB               ;
             | Lself00:          ;
             | B .+12            ;
             | MOV W4,#2         ;
             | B .+8             ;
             | MOV W4,#1         ;
exists (1:X1=1 /\ 1:X4=1)

That is, success, while swapping p and n yields a failure:

% diyone7 -arch AArch64 -variant self -moreedges true "DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUp DSB.ISH IC.IVAUn DSB.ISH ISB FreIP"
diyone7: Fatal error: Test A [DMB.ISHdWW Rfe DpAddrdRPI DC.CVAUp DSB.ISH IC.IVAUn DSB.ISH ISB FreIP] failed:
can't create address dependency for a code location without DC.CVAU or IC.IVAU

(I notice that the error message does not help to fix the problem)

Is this the intended behaviour? Maybe there is nothing to worry about anyway.

hugookeeffe commented 3 weeks ago

thank you @maranget for having a look! thank you for spotting that. Indeed that is not the intended behaviour and after discussing with @artkhyzha it seems we don't want to allow DC/IC to the previous register at all in this case (atleast for now). I have just pushed a commit that addresses this problem. It does unfortunately require traversing the nodes, so the code is not very pretty but I believe it should work. Let me know if you have any suggestions on how to better write this.

hugookeeffe commented 1 week ago

@relokin @maranget I have just squashed commits and rebased on top of master. Is there anything you still want me to do with regards to this?

maranget commented 1 week ago

As far as I am concerned, thie PR can be merged.

relokin commented 1 week ago

Thanks @hugookeeffe! Thanks @artkhyzha and @maranget for the reviews!