[gen] implementation of Ifetch annotation #703

hugookeeffe · 2023-10-24T16:14:04Z

This PR implements a new syntax for generating Ifetch tests, using a new annotation. The I annotation is used to represent explicit memory events to instruction locations (i.e. LDR and STR of an instruction stored at a location identified by a label). This PR also introduces the possibility of generating explicit reads of an instruction. With this new implementation, Ifetch sequences are generated by using the plain annotation with a read to a Code location.

example tests:

diyone7 -arch AArch64 -variant self "RfeII Pod** Rfe Pod** FrePI"
AArch64 A
"RfeII PodRWIP Rfe PodRR FrePI"
Generator=diyone7 (version 7.56+03)
Com=Rf Rf Fr
Orig=RfeII PodRWIP Rfe PodRR FrePI
{
0:X0=instr:"NOP"; 0:X1=P2:Lself00;
1:X0=P2:Lself00; 1:X3=x;
2:X0=x;
}
 P0          | P1          | P2          ;
 STR W0,[X1] | LDR W1,[X0] | LDR W1,[X0] ;
             | MOV W2,#1   | Lself00:    ;
             | STR W2,[X3] | B L00       ;
             |             | MOV W2,#2   ;
             |             | B L01       ;
             |             | L00:        ;
             |             | MOV W2,#1   ;
             |             | L01:        ;
exists (1:X1=instr:"NOP" /\ 2:X1=1 /\ 2:X2=1)

diyone7 -arch AArch64 -variant self "RfeIP Pod** Rfe Pod** FreII"
AArch64 A
"RfeIP PodRW Rfe PodRRPI FreII"
Generator=diyone7 (version 7.56+03)
Com=Rf Rf Fr
Orig=RfeIP PodRW Rfe PodRRPI FreII
{
0:X0=instr:"NOP"; 0:X1=P1:Lself00;
1:X2=x;
2:X0=x; 2:X2=P1:Lself00;
}
 P0          | P1          | P2          ;
 STR W0,[X1] | Lself00:    | LDR W1,[X0] ;
             | B L00       | LDR W3,[X2] ;
             | MOV W0,#2   |             ;
             | B L01       |             ;
             | L00:        |             ;
             | MOV W0,#1   |             ;
             | L01:        |             ;
             | MOV W1,#1   |             ;
             | STR W1,[X2] |             ;
exists (1:X0=2 /\ 2:X1=1 /\ 2:X3=instr:"B .+12")

diyone7 -arch AArch64 -variant self "Pod** RfeIP Pod** FrePI"
AArch64 A
"PodWWII RfeIP PodRR FrePI"
Generator=diyone7 (version 7.56+03)
Com=Rf Fr
Orig=PodWWII RfeIP PodRR FrePI
{
0:X0=instr:"NOP"; 0:X1=P1:Lself00; 0:X2=P1:Lself01;
}
 P0          | P1        ;
 STR W0,[X1] | Lself01:  ;
 STR W0,[X2] | B L00     ;
             | MOV W0,#2 ;
             | B L01     ;
             | L00:      ;
             | MOV W0,#1 ;
             | L01:      ;
             | Lself00:  ;
             | B L02     ;
             | MOV W1,#2 ;
             | B L03     ;
             | L02:      ;
             | MOV W1,#1 ;
             | L03:      ;
exists (1:X0=2 /\ 1:X1=1)

relokin · 2023-10-27T16:02:43Z

Thanks @hugookeeffe.

I haven't looked at the code yet, but looking a bit at the examples in this PR, I think that the post-condition of the 2 test is a little confusing.

diyone7 -arch AArch64 -variant self "RfeIP Pod** Rfe Pod** FreII"
AArch64 A
"RfeIP PodRW Rfe PodRRPI FreII"
Generator=diyone7 (version 7.56+03)
Com=Rf Rf Fr
Orig=RfeIP PodRW Rfe PodRRPI FreII
{
0:X0=instr:"NOP"; 0:X1=P1:Lself00;
1:X2=x;
2:X0=x; 2:X2=P1:Lself00;
}
 P0          | P1          | P2          ;
 STR W0,[X1] | Lself00:    | LDR W1,[X0] ;
             | B L00       | LDR W3,[X2] ;
             | MOV W0,#2   |             ;
             | B L01       |             ;
             | L00:        |             ;
             | MOV W0,#1   |             ;
             | L01:        |             ;
             | MOV W1,#1   |             ;
             | STR W1,[X2] |             ;
exists (1:X0=2 /\ 2:X1=1 /\ 2:X3=instr:"B .+12")

Can't we simply write:

exists (1:X0=2 /\ 2:X1=1 /\ 2:X3!=instr:"NOP")

Otherwise, I think it would be better to have a uniform view of the old value in P1:Lself00 which means having B.+12 in the code of the test (instead of B L00).

relokin

Some comments on the code.

gen/AArch64Arch_gen.ml

gen/AArch64Compile_gen.ml

relokin · 2023-10-27T17:11:07Z

gen/cycle.ml

-      end ;
+      (* ensure Instr read is followed or preceded by plain read to same location*)
+      if E.is_ifetch m.edge.E.a1 && m.evt.dir = Some R && not
+        (is_read_same_nonfetch m.next m ||


Isn't this check redundant? I think find_node_prev (in the next line) will get to m.next, won't it?

gen/cycle.ml

gen/final.ml

hugookeeffe · 2023-10-31T11:05:36Z

@relokin in reference to your comment:

Can't we simply write:

exists (1:X0=2 /\ 2:X1=1 /\ 2:X3!=instr:"NOP")
Otherwise, I think it would be better to have a uniform view of the old value in P1:Lself00 which means having B.+12 in the code of the test (instead of B L00).

the issue with using != currently is that when creating the final condition in gen, the code currently assumes that all individual checks are checking for the value we think is in a register. Because of this, the code currently has no support to have a negation of a single register (excepting faults, which are treated differently).

We could implement support for this, but I think that this would need quite a bit more code. As there are not many cases like this, my preference would be to check for the value that is currently there (so in this case B .+12) and change the code of the test to have this as well. What do you think?

artkhyzha

LGTM! Adding two supernitpick-y comments, I don't consider them blocking.

artkhyzha · 2023-11-03T10:20:14Z

gen/AArch64Arch_gen.ml

@@ -795,6 +802,7 @@ include
        | _ -> false

      let pp_reg = pp_reg
+      let pp_i n = pp_i n


Suggested change

let pp_i n = pp_i n

let pp_i = pp_i

As a matter of nitpicking, could it be defined like this?

artkhyzha · 2023-11-03T10:22:46Z

gen/BellArch_gen.ml

@@ -271,6 +271,7 @@ include
      let is_symbolic _ = false

      let pp_reg = pp_reg
+      let pp_i _ = "instr:\"NOP\""


Suggested change

let pp_i _ = "instr:\"NOP\""

let pp_i _ = assert false

Does this function need to have an implementation for non-AArch64? My hunch is that it should never be called unless this is an error.

I agree with Artem, pp_i should be implemented as `let pp_i _ = assert false" for all *Arch_gen.ml other than AArch64Arch_gen.ml.

relokin · 2023-11-20T11:55:17Z

gen/BellArch_gen.ml

@@ -271,6 +271,7 @@ include
      let is_symbolic _ = false

      let pp_reg = pp_reg
+      let pp_i _ = "instr:\"NOP\""


I agree with Artem, pp_i should be implemented as `let pp_i _ = assert false" for all *Arch_gen.ml other than AArch64Arch_gen.ml.

gen/archExtra_gen.ml

relokin · 2023-11-20T12:48:25Z

gen/cycle.ml

-        Warn.user_error "Ambiguous Data/Code location es [%s] => [%s]"
-          (str_node p) (str_node m)
-      end ;
+      (* ensure Instr read is followed or preceded by plain read to same location*)


Can I check with you that I understand the need for this? Here you're checking that if there is a LDR from a location P0:Lself0 then there will be a label P0:Lself0, or in other words an instruction (fetch) at P0:Lself?

yes, exactly. The plain read to a code location is what creates the label in the body of the code, so if we don't have this then a Instr read will read from a non-existent label

relokin · 2023-11-20T12:58:22Z

gen/cycle.ml

+      if E.is_ifetch m.edge.E.a1 && m.evt.dir = Some R && not
+        (try
+          ignore (find_node_prev (fun n -> is_read_same_nonfetch n m) m);
+          true
+        with Not_found -> false)
+      then
+        Warn.user_error "Instruction read followed by ifetch to different location [%s] => [%s]"
+          (str_node p) (str_node m);


A suggestion that I think will help simplify this:

Suggested change

if E.is_ifetch m.edge.E.a1 && m.evt.dir = Some R && not

(try

ignore (find_node_prev (fun n -> is_read_same_nonfetch n m) m);

true

with Not_found -> false)

then

Warn.user_error "Instruction read followed by ifetch to different location [%s] => [%s]"

(str_node p) (str_node m);

if E.is_ifetch m.edge.E.a1 && m.evt.dir = Some R then begin

try

ignore (find_node_prev (fun n -> is_read_same_nonfetch) m)

with Not_found ->

Warn.user_error "Reading from label that doesn't exist [%s]" (str_node m)

end

(Please check the indentation of the above)

yes, that makes it a lot better. As i needed to use this sequence multiple times in order to fix a bug, I have moved it into the is_read_same_nonfetch function.

Thank you!

gen/cycle.ml

relokin · 2023-11-20T13:53:56Z

gen/cycle.ml

+      match m.edge.E.edge, p.edge.E.edge, m.evt.loc with
+      | E.Irf _,_,_ | _, E.Ifr _,_-> ()
+      | _,_,Code.Code _ -> if m.evt.dir = Some W && not (E.is_ifetch m.edge.E.a1) then
+        Warn.user_error "Plain annotation on write to code location not possible";
+      | _ -> ();


Wouldn't something like this work?

Suggested change

match m.edge.E.edge, p.edge.E.edge, m.evt.loc with

| E.Irf _,_,_ | _, E.Ifr _,_-> ()

| _,_,Code.Code _ -> if m.evt.dir = Some W && not (E.is_ifetch m.edge.E.a1) then

Warn.user_error "Plain annotation on write to code location not possible";

| _ -> ();

match m.evt.loc, m.evt.dir with

| Code.Code _,Some W when not (E.is_ifetch m.edge.E.a1) ->

Warn.user_error "Plain annotation on write to code location not possible";

| _ ->

() ;

ah, thank you for the suggestion. I have implemented this.

I will make the changes to get Irf, Ifr changed in my next patch

@relokin I have made the changes to make Irf/Ifr to be translated to Rf/Fr in the patch I have just pushed

gen/edge.ml

relokin · 2023-11-20T14:09:27Z

gen/top_gen.ml

+                    match n.C.prev.C.edge.E.edge, n.C.edge.E.edge, E.is_ifetch n.C.prev.C.edge.E.a2, E.is_ifetch n.C.edge.E.a1 with
+                    |E.Rf _,_,true,_| _,E.Fr _,_,true -> F.add_final (A.get_friends st) p o n finals
+                    |_,E.Po _,_,true -> F.add_final (A.get_friends st) p o n finals
+                    | _,_,_,_-> begin


don't you need to enclose this in begin ... end?

Suggested change

match n.C.prev.C.edge.E.edge, n.C.edge.E.edge, E.is_ifetch n.C.prev.C.edge.E.a2, E.is_ifetch n.C.edge.E.a1 with

|E.Rf _,_,true,_| _,E.Fr _,_,true -> F.add_final (A.get_friends st) p o n finals

|_,E.Po _,_,true -> F.add_final (A.get_friends st) p o n finals

| _,_,_,_-> begin

match n.C.prev.C.edge.E.edge, n.C.edge.E.edge with

| E.Rf _, _ when E.is_ifetch n.C.prev.C.edge.E.a2 ->

F.add_final (A.get_friends st) p o n finals

| _, E.Po _ | _, E.Fr _ when E.is_ifetch n.C.prev.C.edge.E.a1 ->

F.add_final (A.get_friends st) p o n finals

| _, _-> begin

I don't think we need to enclose it in begin ... end, it seems to be working as it is. Do you think it would be more legible with it implemented?

Thank you for the suggested change! I have implemented it.

gen/edge.ml

gen/AArch64Compile_gen.ml

relokin · 2023-12-01T15:54:52Z

gen/edge.ml

I cannot add a comment to line 66, but ideally I think we should remove Irf and Ifr from the definition of type tedge after all with the new annotations can't we just use Rf and Fr?

We could do that, but I thought we wanted to keep the ability to parse it in case it was in use by others at the moment?

Yes we do, a user should be able to specify the relaxation Irf or using this PR RfIP. But these two are equivalent, aren't they? Shouldn't we have just one implementation? Internally we don't need to have a special case for Irf in type tedge because this is just a case of Rf. Does this make sense?

That makes sense, however, the issue with this is that annotations are architecture-specific in the code, whereas the edge type is not. To have Irf be read by the tool as RfIP, we would have to implement the I annotation for all other architectures. We could do this but I'm not sure it would simplify the code much by doing so.

I am afraid I don't understand what you mean. Irf/Ifr is only implemented for AArch64 isn't it? When I do:

$> diyone7 -arch X86_64 -variant self PodWW Rfe PodRR Ifre

I get:

diyone7: Fatal error: Test A [PodWW Rfe PodRR Ifre] failed: No code location for X86_64

Is there any other architecture, Ifre is implemented for?

Why would you have to implement the new annotations for all other architectures? When I do:

$> diyone7 -arch X86_64 -variant self PodWW Rfe PodRR FrePI

I get:

diyone7: Fatal error: Bad relax: FrePI

Which for the end user this means the same thing as the previous error message. The feature is not implemented for X86_64. And I am not suggesting that you change this. All I am saying is that the user can either do:

$> diyone7 -arch AArch64 -variant self PodWW Rfe PodRR Ifre

or

$> diyone7 -arch AArch64 -variant self PodWW Rfe PodRR FrePI

and get the same test. Why have should we have different implementations? I would expect that the only support we need for Ifre, is in the parser. We would parse FrePI and Ifre using the same internal representation. Then we use the same code to generate the test which you've implemented already and completely get rid of the code that implements Ifre.

Whilst Ifr/Irf is only implemented for AArch64, it is implemented generally at the level of the parser (with the code location fail only happening later). When we are parsing for the type tedge, we go through the function do_pp_edge, which is a general function.

Currently, the way that my patch treats “Irf” and “Ifr” strings is that they get parsed as Irf/Ifr of type tedge and are then converted to the desired Rf/Fr representation when building the cycle (this can be seen in the function convert_ins in cycle.ml). This means that the same internal logic is used when the tests are being built and the same tests should be generated regardless of which syntax is used.

If we wanted the string Irf and Ifr to be converted to Rf and Fr at the point of parsing, we would need to implement architecture specific functions to return the appropriate annotations in the function do_pp_edge. However, for this we would need to implement such a function into all architectures.

Keeping Irf/ifr in tedge seems like the simpler solution here, as it reduces the amount of extra functions needed to be written into other architectures. And as Irf/Ifr are converted to Rf/Fr early on, the logic to generate the test should be the same.

I agree, it's not straightforward but it's better than having two separate implementations for "Ifr" and "Irf". I took a stub at it and the patch is here: relokin@184e12c . If you're happy with it, please cherry pick it in your PR.

Otherwise, I am happy with the PR, please rebase and squash your commits into 1 and I will then merge.

If all worked well, I have now rebased and squashed my commits into 1, with your commit cherry-picked. Thank you very much for the help and let me know if I did anything wrong or you would like me to do something else

@hugookeeffe, I think something went wrong, the PR is not rebased on top of the latest master and it doesn't compile:

sh ./version-gen.sh ~/.local dune build -j 8 --profile release File "gen/cycle.ml", line 952, characters 33-43: 952 | let to_com_rmw n0 = not (is_com_rmw n0.prev) && is_com_rmw n0 in ^^^^^^^^^^ Error: Unbound value is_com_rmw make: *** [build] Error 1

Can you have a look please?

that's strange. I've tried rebasing again, and it works for me now. I think I must have not pushed the rebase properly. Does it work for you now?

relokin · 2024-01-24T10:07:30Z

litmus/lexAffinity.mll

@@ -38,8 +38,8 @@ let num = digit+

 rule coms = parse
 | space+ { coms lexbuf }
-| "Fr"|"Iff"|"Irf"  { Fr :: coms lexbuf }


I'm a little worried about this, can you check if it is a problem? That is generate a test with Irf and use litmus7 to run it. I think it's not problem because diyone7 will not print Irf but Rf instead but just to make sure.

I have just done that with the following test,

diyone7 -arch AArch64 -variant self "PodWW Irfe PodRR Ifre" -moreedges true AArch64 A "PodWWII RfeIP PodRR FrePI" Generator=diyone7 (version 7.56+03) Com=Rf Fr Orig=PodWWII RfeIP PodRR FrePI { 0:X0=instr:"NOP"; 0:X1=P1:Lself00; 0:X2=P1:Lself01; } P0 | P1 ; STR W0,[X1] | Lself01: ; STR W0,[X2] | B .+12 ; | MOV W0,#2 ; | B .+8 ; | MOV W0,#1 ; | Lself00: ; | B .+12 ; | MOV W1,#2 ; | B .+8 ; | MOV W1,#1 ; exists (1:X0=2 /\ 1:X1=1)

and it has run with no issue with litmus7. As you suggested, diyone7 doesn't print Irf anyway so it doesn't create a problem

relokin · 2024-01-25T13:24:12Z

I will be doing a final check and planning to merge this tomorrow. Please let me know if you need more time to review this or have any objections.

relokin · 2024-01-28T20:28:57Z

Looks good to me. Thanks @hugookeeffe I am going to merge this now.

relokin reviewed Oct 27, 2023

View reviewed changes

maranget force-pushed the master branch from 5feae45 to a23d589 Compare October 30, 2023 15:04

hugookeeffe force-pushed the ifetch_newsyntax branch from 5c68020 to 5ad16ed Compare October 31, 2023 10:21

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

hugookeeffe force-pushed the ifetch_newsyntax branch from 37da7f4 to 8646407 Compare October 31, 2023 13:33

artkhyzha approved these changes Nov 3, 2023

View reviewed changes

hugookeeffe mentioned this pull request Nov 6, 2023

[gen]DC CVAU and IC IVAU relaxations #707

Merged

relokin requested changes Nov 20, 2023

View reviewed changes

hugookeeffe mentioned this pull request Nov 21, 2023

[gen] Ifetch config #719

Closed

relokin reviewed Dec 1, 2023

View reviewed changes

hugookeeffe force-pushed the ifetch_newsyntax branch from 5bf551f to b0e6227 Compare January 24, 2024 10:02

relokin reviewed Jan 24, 2024

View reviewed changes

hugookeeffe force-pushed the ifetch_newsyntax branch from b0e6227 to 8f74c9e Compare January 24, 2024 14:06

[gen] implementation of ifetch annotation

7458fc7

relokin force-pushed the ifetch_newsyntax branch from 8f74c9e to 7458fc7 Compare January 28, 2024 20:27

relokin approved these changes Jan 28, 2024

View reviewed changes

relokin merged commit 0b1fb59 into herd:master Jan 28, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[gen] implementation of Ifetch annotation #703

[gen] implementation of Ifetch annotation #703

hugookeeffe commented Oct 24, 2023 •

edited by relokin

Loading

relokin commented Oct 27, 2023

relokin left a comment

relokin Oct 27, 2023

hugookeeffe commented Oct 31, 2023

artkhyzha left a comment

artkhyzha Nov 3, 2023

artkhyzha Nov 3, 2023

relokin Nov 20, 2023

relokin Nov 20, 2023

relokin Nov 20, 2023

hugookeeffe Nov 21, 2023

relokin Nov 20, 2023

hugookeeffe Nov 21, 2023

relokin Nov 20, 2023

hugookeeffe Nov 21, 2023

hugookeeffe Nov 22, 2023

relokin Nov 20, 2023

hugookeeffe Nov 21, 2023

relokin Dec 1, 2023

hugookeeffe Dec 4, 2023

relokin Dec 4, 2023

hugookeeffe Dec 7, 2023

relokin Dec 7, 2023

hugookeeffe Dec 8, 2023

relokin Jan 22, 2024

hugookeeffe Jan 24, 2024

relokin Jan 24, 2024

hugookeeffe Jan 24, 2024

relokin Jan 24, 2024

hugookeeffe Jan 24, 2024 •

edited

Loading

relokin commented Jan 25, 2024

relokin commented Jan 28, 2024

[gen] implementation of Ifetch annotation #703

[gen] implementation of Ifetch annotation #703

Conversation

hugookeeffe commented Oct 24, 2023 • edited by relokin Loading

relokin commented Oct 27, 2023

relokin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hugookeeffe commented Oct 31, 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

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

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

hugookeeffe Jan 24, 2024 • edited Loading

Choose a reason for hiding this comment

relokin commented Jan 25, 2024

relokin commented Jan 28, 2024

hugookeeffe commented Oct 24, 2023 •

edited by relokin

Loading

hugookeeffe Jan 24, 2024 •

edited

Loading