[gen]DC CVAU and IC IVAU relaxations #707

hugookeeffe · 2023-10-26T14:34:18Z

This pull request implements the ability to generate DC CVAU and IC IVAU instructions as a fence instruction. This allows the user to implement these instructions with more fine-grain control into litmus tests.

This PR also implements the ability for dependencies to be generated before Insert relaxations.

The relaxations for DC CVAU and IC IVAU are:

DC.CVAU<n/p>
IC.IVAU<n/p>

where n and p allow the user to choose whether DC/IC act on the previous location or the next location

examples that couldn't be generated previously:

diyone7 -moreedges true -arch AArch64 -variant self "PodWW DC.CVAUp DMB.ISH Rfe PodRR DSB.ISH IC.IVAUn DSB.ISH ISB Ifre"
AArch64 A
"PodWW DC.CVAUp DMB.ISH Rfe PodRR DSB.ISH IC.IVAUn DSB.ISH ISB Ifre"
Generator=diyone7 (version 7.56+03)
Com=Rf Ifr
Orig=PodWW DC.CVAUp DMB.ISH Rfe PodRR DSB.ISH IC.IVAUn DSB.ISH ISB Ifre
{
0:X0=NOP; 0:X1=P1:Lself00; 0:X3=x;
1:X0=x; 1:X2=P1:Lself00;
}
 P0          | P1          ;
 STR W0,[X1] | LDR W1,[X0] ;
 DC CVAU,X1  | DSB ISH     ;
 DMB ISH     | IC IVAU,X2  ;
 MOV W2,#1   | DSB ISH     ;
 STR W2,[X3] | ISB         ;
             | Lself00:    ;
             | B L00       ;
             | MOV W3,#2   ;
             | B L01       ;
             | L00:        ;
             | MOV W3,#1   ;
             | L01:        ;
exists (1:X1=1 /\ 1:X3=1)

diyone7 -moreedges true -arch AArch64 -variant self "[DpCtrlIsbdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre] DMB.ISHdWW Rfe"
AArch64 A
"DpCtrlIsbdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre DMB.ISHdWW Rfe"
Generator=diyone7 (version 7.56+03)
Com=Ifr Rf
Orig=DpCtrlIsbdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre DMB.ISHdWW Rfe
{
0:X0=x; 0:X2=P0:Lself00;
1:X0=NOP; 1:X1=P0:Lself00; 1:X3=x;
}
 P0           | P1          ;
 LDR W1,[X0]  | STR W0,[X1] ;
 CBNZ W1,LC00 | DMB ISH     ;
 LC00:        | MOV W2,#1   ;
 ISB          | STR W2,[X3] ;
 DC CVAU,X2   |             ;
 DSB ISH      |             ;
 IC IVAU,X2   |             ;
 DSB ISH      |             ;
 ISB          |             ;
 Lself00:     |             ;
 B L01        |             ;
 MOV W3,#2    |             ;
 B L02        |             ;
 L01:         |             ;
 MOV W3,#1    |             ;
 L02:         |             ;
exists (0:X1=1 /\ 0:X3=1)

hugookeeffe · 2023-11-01T13:31:48Z

This PR has also been tested using the following configuration file. This generates 500 tests for me and scanning through the tests I haven't been able to see anything clearly wrong.

Note that this conf file uses -stdout true in order not to generate files, make sure to remove this line if you desire for litmus test files to be generated instead of output to stdout.

-arch AArch64
-variant self
-safe DC.CVAUn DC.CVAUp IC.IVAUn IC.IVAUp DSB.ISHd** DpAddrdR DpAddrsR Ifre Rfe DpCtrlIsbdR PodWW PodRR PodRW PodWR PosRR PosWW PosWR PosRW [DC.CVAUn, Ifre, PodWW, DSB.ISH, IC.IVAUp] [Ifre PodW* DC.CVAUp DSB.ISH IC.IVAUp DSB.ISH ISB] [Ifre PosW* DC.CVAUp DSB.ISH IC.IVAUp DSB.ISH ISB] [ Pod*R DSB.ISH DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre] [ DpCtrlIsbdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre] [ Pod*R DSB.ISH IC.IVAUn DSB.ISH ISB Ifre PodW* DC.CVAUp DSB.ISH] [PodRR Ifre PodW* DC.CVAUp DSB.ISH IC.IVAUp DSB.ISH]
-moreedges true
-stdout true
-ins 10
-nprocs 2

murzinv · 2023-11-03T10:10:24Z

Hi @hugookeeffe
Thanks a lot for your work and example config file. I noticed that generated litmus test uses specialized syntax for NOP like 0:X0=NOP; can it be changed to unified syntax for instructions like 0:X0=instr:"NOP";?

hugookeeffe · 2023-11-06T09:13:17Z

Hi @murzinv

Thanks a lot for your work and example config file. I noticed that generated litmus test uses specialized syntax for NOP like 0:X0=NOP; can it be changed to unified syntax for instructions like 0:X0=instr:"NOP";?

I completely agree, I have another PR open at the moment, #703, where I have made the change for this.

artkhyzha

LGTM! Specifically, I looked through the code, the examples and some of the generated tests, which all seemed good.

gen/AArch64Arch_gen.ml

gen/AArch64Compile_gen.ml

gen/AArch64Arch_gen.ml

relokin · 2024-01-23T22:53:59Z

gen/AArch64Compile_gen.ml

+      | D.CTRL ->
+        let c,st = emit_ctrl_gen csel st vdep r1 in
+        let init,cs,st = emit_fence st p init n f in
+        None,init,insert_isb false c cs,st
+      | D.CTRLISYNC ->
+        let c,st = emit_ctrl_gen csel st vdep r1 in
+        let init,cs,st = emit_fence st p init n f in
+        None,init,insert_isb true c cs,st


This two cases can be merged into one like so:

Suggested change

| D.CTRL ->

let c,st = emit_ctrl_gen csel st vdep r1 in

let init,cs,st = emit_fence st p init n f in

None,init,insert_isb false c cs,st

| D.CTRLISYNC ->

let c,st = emit_ctrl_gen csel st vdep r1 in

let init,cs,st = emit_fence st p init n f in

None,init,insert_isb true c cs,st

| D.CTRL | D.CTRLISYNC ->

let c,st = emit_ctrl_gen csel st vdep r1 in

let init,cs,st = emit_fence st p init n f in

None,init,insert_isb (is_ctrlisync dp) c cs,st

What do you think?

Although, I think CTRLISYNC is redundant (one can insert an ISB pseudo relation as well).

Thank you for the suggestion! I have implemented the change

relokin · 2024-01-23T23:08:25Z

gen/AArch64Compile_gen.ml

+      let vdep = node2vdep n1 in
+      match dp with
+      | D.ADDR
+      | D.DATA -> let init,cs, st = emit_fence st p init n f in


I tried generating some examples with DpAddr and DpCtrl but I didn't get what I was expecting. For example:

$> diyone7 -moreedges true -arch AArch64 -variant self "DMB.ISHdWW Rfe [DpAddrdR ISB DC.CVAUp DSB.ISH IC.IVAUp DSB.ISH ISB Ifre]"

Throws an error that there can't be an address dependency to code. Which makes sense. But then I think I don't know how to use DpAddr.

Hmm, that is strange, what behaviour would you expect here? Ctrl does seem to work, but not Addr. should we expect both to work or neither?

I am not sure what are the meaningful tests we can produce with DpAddr*R then. For example, if we ignore the address dependency to code location:

$> diyone7 -moreedges true -arch AArch64 -variant self "DMB.ISHdWW Rfe [DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB] Fre" AArch64 A "DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Fre" Generator=diyone7 (version 7.56+03) Com=Rf Fr Orig=DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Fre { 0:X1=x; 0:X3=y; 1:X0=y; 1:X2=x; } P0 | P1 ; MOV W0,#1 | LDR W1,[X0] ; STR W0,[X1] | DC CVAU,X2 ; DMB ISH | DSB ISH ; MOV W2,#1 | IC IVAU,X2 ; STR W2,[X3] | DSB ISH ; | ISB ; | EOR W3,W1,W1 ; | LDR W4,[X2,W3,SXTW] ; exists (1:X1=1 /\ 1:X4=0)

The DC doesn't have an address dependency from the 1st LDR in P1.

Ignoring ifetch for a minute:

$> diyone7 -moreedges true -arch AArch64 -variant self "DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Fre" AArch64 A "DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Fre" Generator=diyone7 (version 7.56+03) Com=Rf Fr Orig=DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Fre { 0:X1=x; 0:X3=y; 1:X0=y; 1:X2=x; } P0 | P1 ; MOV W0,#1 | LDR W1,[X0] ; STR W0,[X1] | DC CVAU,X2 ; DMB ISH | DSB ISH ; MOV W2,#1 | IC IVAU,X2 ; STR W2,[X3] | DSB ISH ; | ISB ; | EOR W3,W1,W1 ; | LDR W4,[X2,W3,SXTW] ; exists (1:X1=1 /\ 1:X4=0)

But I would expect:

AArch64 A "DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Fre" Generator=diyone7 (version 7.56+03) Com=Rf Fr Orig=DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Fre { 0:X1=x; 0:X3=y; 1:X0=y; 1:X2=x; } P0 | P1 ; MOV W0,#1 | LDR W1,[X0] ; | EOR W3,W1,W1 ; | ADD X5,X2,W3,SXTW ; STR W0,[X1] | DC CVAU,X5 ; DMB ISH | DSB ISH ; MOV W2,#1 | IC IVAU,X5 ; STR W2,[X3] | DSB ISH ; | ISB ; | LDR W4,[X5] ; exists (1:X1=1 /\ 1:X4=0)

And if it won't be too hard, I think for ifetch we should get this test:

diyone7 -moreedges true -arch AArch64 -variant self "DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre" AArch64 A "DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre" Generator=diyone7 (version 7.56+03) Com=Rf Ifr Orig=DMB.ISHdWW Rfe DpAddrdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB Ifre { 0:X0=NOP; 0:X1=P1:Lself00; 0:X3=x; 1:X0=x; 1:X2=P1:Lself00; } P0 | P1 ; STR W0,[X1] | LDR W1,[X0] ; | EOR W4,W1,W1 ; | ADD X3,X2,W4,SXTW ; DMB ISH | DC CVAU,X3 ; MOV W2,#1 | DSB ISH ; STR W2,[X3] | IC IVAU,X3 ; | DSB ISH ; | ISB ; | Lself00: ; | B L00 ; | MOV W3,#2 ; | B L01 ; | L00: ; | MOV W3,#1 ; | L01: ; exists (1:X1=1 /\ 1:X3=1)

Hi Nikos, I have implemented this change now for the normal case without ifetch, however the case with ifetch is a littl more complicated so for now I am throwing an error. Let me know if it is now doing what you expect it to.

I will now also rebase the patch on top of master

The PR has now been rebased. let me know if there is anything else you would like me to do for this

This change implements the ability to generate DC CVAU and IC IVAU instructions as a fence instruction. This allows the user to implement these instructions with more fine-grain control into litmus tests. The relaxations for DC CVAU and IC IVAU are: DC.CVAU<n/p> IC.IVAU<n/p> where n and p allow the user to choose whether the DC/IC instruction will use the previous location or the next location. Examples that couldn't be generated previously: $> diyone7 -moreedges true -arch AArch64 -variant self "PodWW DC.CVAUp DMB.ISH Rfe PodRR DSB.ISH IC.IVAUn DSB.ISH ISB FrePI" AArch64 A "PodWWIP DC.CVAUp DMB.ISH Rfe PodRR DSB.ISH IC.IVAUn DSB.ISH ISB FrePI" Generator=diyone7 (version 7.56+03) Com=Rf Fr Orig=PodWWIP DC.CVAUp DMB.ISH Rfe PodRR DSB.ISH IC.IVAUn DSB.ISH ISB FrePI { 0:X0=instr:"NOP"; 0:X1=P1:Lself00; 0:X3=x; 1:X0=x; 1:X2=P1:Lself00; } P0 | P1 ; STR W0,[X1] | LDR W1,[X0] ; DC CVAU,X1 | DSB ISH ; DMB ISH | IC IVAU,X2 ; MOV W2,herd#1 | DSB ISH ; STR W2,[X3] | ISB ; | Lself00: ; | B .+12 ; | MOV W3,herd#2 ; | B .+8 ; | MOV W3,herd#1 ; exists (1:X1=1 /\ 1:X3=1) $> diyone7 -moreedges true -arch AArch64 -variant self "DMB.ISHdWW Rfe DpCtrlIsbdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB FrePI" AArch64 A "DMB.ISHdWWIP Rfe DpCtrlIsbdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB FrePI" Generator=diyone7 (version 7.56+03) Com=Rf Fr Orig=DMB.ISHdWWIP Rfe DpCtrlIsbdR DC.CVAUn DSB.ISH IC.IVAUn DSB.ISH ISB FrePI { 0:X0=instr:"NOP"; 0:X1=P1:Lself00; 0:X3=x; 1:X0=x; 1:X2=P1:Lself00; } P0 | P1 ; STR W0,[X1] | LDR W1,[X0] ; DMB ISH | CBNZ W1,LC00 ; MOV W2,herd#1 | LC00: ; STR W2,[X3] | ISB ; | DC CVAU,X2 ; | DSB ISH ; | IC IVAU,X2 ; | DSB ISH ; | ISB ; | Lself00: ; | B .+12 ; | MOV W3,herd#2 ; | B .+8 ; | MOV W3,herd#1 ; exists (1:X1=1 /\ 1:X3=1)

relokin · 2024-02-01T16:53:54Z

Thanks @hugookeeffe. This PR LGTM and I will merge tomorrow at the end of the day unless anyone objects or needs more time to review this.

relokin · 2024-02-02T19:49:06Z

Merged into master, thanks @hugookeeffe!

hugookeeffe changed the title ~~Di insert~~ [gen]DC CVAU and IC IVAU relaxations Oct 26, 2023

maranget force-pushed the master branch 2 times, most recently from a23d589 to 5905deb Compare October 31, 2023 13:09

hugookeeffe force-pushed the DI_insert branch 2 times, most recently from de16555 to ea2295c Compare October 31, 2023 13:30

artkhyzha approved these changes Nov 13, 2023

View reviewed changes

hugookeeffe mentioned this pull request Nov 21, 2023

[gen] Ifetch config #719

Closed

relokin reviewed Jan 23, 2024

View reviewed changes

hugookeeffe force-pushed the DI_insert branch from 4f1afc2 to c647ff8 Compare January 31, 2024 15:17

relokin force-pushed the DI_insert branch from c647ff8 to fc45c7d Compare February 1, 2024 16:52

relokin approved these changes Feb 1, 2024

View reviewed changes

relokin merged commit b8ad302 into herd:master Feb 2, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[gen]DC CVAU and IC IVAU relaxations #707

[gen]DC CVAU and IC IVAU relaxations #707

hugookeeffe commented Oct 26, 2023

hugookeeffe commented Nov 1, 2023

murzinv commented Nov 3, 2023 •

edited

Loading

hugookeeffe commented Nov 6, 2023

artkhyzha left a comment

relokin Jan 23, 2024

hugookeeffe Jan 26, 2024

relokin Jan 23, 2024

hugookeeffe Jan 26, 2024

relokin Jan 29, 2024

relokin Jan 29, 2024

hugookeeffe Jan 31, 2024

hugookeeffe Jan 31, 2024

relokin commented Feb 1, 2024

relokin commented Feb 2, 2024

[gen]DC CVAU and IC IVAU relaxations #707

[gen]DC CVAU and IC IVAU relaxations #707

Conversation

hugookeeffe commented Oct 26, 2023

hugookeeffe commented Nov 1, 2023

murzinv commented Nov 3, 2023 • edited Loading

hugookeeffe commented Nov 6, 2023

artkhyzha left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

relokin commented Feb 1, 2024

relokin commented Feb 2, 2024

murzinv commented Nov 3, 2023 •

edited

Loading