[gen] Refactor communication edge representation

[ShaleXIONG]

Unify constructors Rf, Fr, and Ws in relax.ml and the similar constructors CRf, CFr and CWs in code.ml. The former has been wrapped behind Communication (com, ie) and rename the latter constructors to Rf, Fr, and Co. Update edge folding, parsing, naming, relaxation handling, and generation code to use the unified communication representation while preserving existing printed syntax.

[TiberiuBucur]

A few minor comments / requests for clarifications :)

[TiberiuBucur]

Is it guaranteed that the f parameter will return the same result when applied to the same operators no matter the order? Because the old version did Rf -> Fr -> Ws whereas fold_com does the opposite.

[ShaleXIONG]

I change the order back to Rf -> Fr -> Ws(Co).

There is no guarantee on the same behaviour on different order. However the order does not matter in the the way we use all the fold_ functions. They are used to build a look-up table.

[TiberiuBucur]

I see. I don't have an issue either way if you think it doesn't make a difference, but in that case I would personally keep the definition of fold_com in the original order (Rf as the outermost parameter, Co as the innermost) for the sake of consistency.

[TiberiuBucur]

I understand this behaviour existed before this patch, but why do this function and the one below only concern themselves with external communication edges?

[ShaleXIONG]

I do not have a definitive answer but I believe the function count_a is used to heuristically to generate file name.

[relokin]

Sorry I’m still not convinced we want Com to be a constructor in edge.ml. Can you please explain what is it that you would like to achieve with this PR? Let’s focus on that first and then I can help with the how.

[ShaleXIONG]

Sorry I’m still not convinced we want Com to be a constructor in edge.ml. Can you please explain what is it that you would like to achieve with this PR? Let’s focus on that first and then I can help with the how.

This is purely code improve for now but the main goal here is to implement ExpObs edges which will be represented as Com(UnspecCom,Ext).

Also there were two datatypes that were the same thing but used in two separate places in the code.

• type com of CRf, CFr and CWs in the code.ml. They are pretty-print to Rf, Fr and Co , However they were not used for the common communication edges Rfe, Fre and Coe. They were used for edges LeaveRf, BackRf etc. For example you will see in the type tedge in edge.ml, there are constructors Leave (com) and Back (com)
• The actual communication edges Rfe, Fre, and Coe were defined in edge.ml with three explicit constructors Rf(ie), Fr(ie), and Ws(ie). The pretty-print for these three constructors were also Rf and Fr and Co.

The two datatypes were the same, so the best way is to fold the second datatype for communication edge into Com(com_type, ie), which is now in similar style as Leave(com_type) and Back(com_type).

[relokin]

Sorry I’m still not convinced we want Com to be a constructor in edge.ml. Can you please explain what is it that you would like to achieve with this PR? Let’s focus on that first and then I can help with the how.

This is purely code improve for now but the main goal here is to implement ExpObs edges which will be represented as Com(UnspecCom,Ext).

Exp-obs is not the only derived relation we need for aarch64.cat. We have many more, for example dob, are you suggesting we do that for data dependencies as well?

I’m not convinced this PR is the right solution to the problem. I think we need to come up with a way to define new symbols which group together multiple relaxations. This would work for Exps-obs as well as other relations in the cat file. This would be more syntactic sugar for the use of diy7 and not a fundamental relaxation. What I mean is that the user would write

ExpObs and diy7

would expand it to

Rfe
Coe
Fre

but the gen code will know nothing else about ExpObs.

Also there were two datatypes that were the same thing but used in two separate places in the code.

• type com of CRf, CFr and CWs in the code.ml. They are pretty-print to Rf, Fr and Co , However they were not used for the common communication edges Rfe, Fre and Coe. They were used for edges LeaveRf, BackRf etc. For example you will see in the type tedge in edge.ml, there are constructors Leave (com) and Back (com)
• The actual communication edges Rfe, Fre, and Coe were defined in edge.ml with three explicit constructors Rf(ie), Fr(ie), and Ws(ie). The pretty-print for these three constructors were also Rf and Fr and Co.

This part of the change seems sensible.

[ShaleXIONG]

Sorry I’m still not convinced we want Com to be a constructor in edge.ml. Can you please explain what is it that you would like to achieve with this PR? Let’s focus on that first and then I can help with the how.

This is purely code improve for now but the main goal here is to implement ExpObs edges which will be represented as Com(UnspecCom,Ext).

Exp-obs is not the only derived relation we need for aarch64.cat. We have many more, for example dob, are you suggesting we do that for data dependencies as well?

I’m not convinced this PR is the right solution to the problem. I think we need to come up with a way to define new symbols which group together multiple relaxations. This would work for Exps-obs as well as other relations in the cat file. This would be more syntactic sugar for the use of diy7 and not a fundamental relaxation. What I mean is that the user would write

ExpObs and diy7

would expand it to

Rfe Coe Fre

but the gen code will know nothing else about ExpObs.

I totally agree here. This is similar to issue #1784. I think we should treat ExpObs and many other wildcard for example Po as a macro or in other word, a syntactic sugar. A macro in diy* is basically a string-based shorthand for example AllRW. diy* will directly map the input string to a list of unfolded concrete datatype. While currently syntax like Po and ExpObs (if we do minimum change to achieve ExpObs), are treated as a wildcard. A wildcard has an internal datatype to represent them, for example Po as Po(Unspec,Unspec,Unspec). Then a separate step to expand an wildcard to the list of concrete datatype.

There is nothing to stop us to remove the use of wildcard completely, in fact I already have a local PR for that. Yet it breaks some test cases on cat2config which I already chatted with @fsestini, and I will try to patch those test cases on cat2config. Separately, the PR itself is very large. Although I organised it in theme, for example, (1) move Po to macro, (2) move Dp to macro, etc., yet I think we probably need to merge them in phases.

Also there were two datatypes that were the same thing but used in two separate places in the code.

• type com of CRf, CFr and CWs in the code.ml. They are pretty-print to Rf, Fr and Co , However they were not used for the common communication edges Rfe, Fre and Coe. They were used for edges LeaveRf, BackRf etc. For example you will see in the type tedge in edge.ml, there are constructors Leave (com) and Back (com)
• The actual communication edges Rfe, Fre, and Coe were defined in edge.ml with three explicit constructors Rf(ie), Fr(ie), and Ws(ie). The pretty-print for these three constructors were also Rf and Fr and Co.

This part of the change seems sensible.

The change here is purely for the second part, hence I decide to put forwards first, which can be independent from how we want to implement ExpObs.

[TiberiuBucur]

I think we should treat ExpObs and many other wildcard for example Po as a macro or in other word, a syntactic sugar. A macro in diy* is basically a string-based shorthand for example AllRW. diy* will directly map the input string to a list of unfolded concrete datatype.

If the plan is to do this thing for all kinds of aarch64 dependencies, do you think diy can use the cat file as some sort of ground truth for what "primitive edges" (coe, rfe, fre) a dependency is made of? It would help with future changes to the cat file not requiring updates to diy.

[fsestini]

I think we should treat ExpObs and many other wildcard for example Po as a macro or in other word, a syntactic sugar. A macro in diy* is basically a string-based shorthand for example AllRW. diy* will directly map the input string to a list of unfolded concrete datatype.

If the plan is to do this thing for all kinds of aarch64 dependencies, do you think diy can use the cat file as some sort of ground truth for what "primitive edges" (coe, rfe, fre) a dependency is made of? It would help with future changes to the cat file not requiring updates to diy.

FWIW, this is precisely what cat2config does (for a subset of the cat file).

[ShaleXIONG]

I think we should treat ExpObs and many other wildcard for example Po as a macro or in other word, a syntactic sugar. A macro in diy* is basically a string-based shorthand for example AllRW. diy* will directly map the input string to a list of unfolded concrete datatype.

If the plan is to do this thing for all kinds of aarch64 dependencies, do you think diy can use the cat file as some sort of ground truth for what "primitive edges" (coe, rfe, fre) a dependency is made of? It would help with future changes to the cat file not requiring updates to diy.

FWIW, this is precisely what cat2config does (for a subset of the cat file).

@TiberiuBucur @fsestini That is a good comment. I think it is certainly possible to gradually bring in some cat language, for example treating them as macros first, as the ground true into diy7, esp. those cat axioms that can be easily translated to diy relax/edge and ultimately to the instruction sequences. However we have some cat axioms are non-trivial and challenging to map to instruction sequences; one example here is implicit event which may be triggered by many explicit memory events. Here I also want to emphasise instruction sequences because diy* are tools that helps us generate interaction sequences and eventual litmus tests. This means the diy* input should give some idea of the final litmus tests.

I think some of this comments are much more related to #1784 , if you @TiberiuBucur are interested, we can collaborate !

[fsestini]

I think we should treat ExpObs and many other wildcard for example Po as a macro or in other word, a syntactic sugar. A macro in diy* is basically a string-based shorthand for example AllRW. diy* will directly map the input string to a list of unfolded concrete datatype.

If the plan is to do this thing for all kinds of aarch64 dependencies, do you think diy can use the cat file as some sort of ground truth for what "primitive edges" (coe, rfe, fre) a dependency is made of? It would help with future changes to the cat file not requiring updates to diy.

FWIW, this is precisely what cat2config does (for a subset of the cat file).

@TiberiuBucur @fsestini That is a good comment. I think it is certainly possible to gradually bring in some cat language, for example treating them as macros first, as the ground true into diy7, esp. those cat axioms that can be easily translated to diy relax/edge and ultimately to the instruction sequences. However we have some cat axioms are non-trivial and challenging to map to instruction sequences; one example here is implicit event which may be triggered by many explicit memory events. Here I also want to emphasise instruction sequences because diy* are tools that helps us generate interaction sequences and eventual litmus tests. This means the diy* input should give some idea of the final litmus tests.

I think some of this comments are much more related to #1784 , if you @TiberiuBucur are interested, we can collaborate !

For the record, I'm not proposing a solution here. Just wanted to point out that if we do decide to involve the cat model for this sort of feature, cat2config constitutes a potentially useful precedent to draw inspiration (and maybe implementation) from :)