[gen] Add wildcard Amo.Safe.

[ShaleXIONG]

Add a new wildcard Amo.Safe that unfolds to Amo.Cas Amo.Swp Amo.StAdd and Amo.LdAdd. It corresponds the Amo.* that has no value collision problem, that is, there is distinct value different before and after the Amo.* operation when diy7 generates tests.

[fsestini]

Discussed offline: my suggestion is to investigate the possibility of representing Amo.Safe (and similarly, Amo.*) as macros/syntactic sugar, rather than as proper additional constructors of the rmw type. We already do a similar macro expansion here for allRW etc.

[ShaleXIONG]

Discussed offline: my suggestion is to investigate the possibility of representing Amo.Safe (and similarly, Amo.*) as macros/syntactic sugar, rather than as proper additional constructors of the rmw type. We already do a similar macro expansion here for allRW etc.

If I add in the relax.ml, then Amo.Safe will not appear in diy7 -show edge. Let me have a look if I can add the missing allowed edges in diy7 -show edge too, for example, allRR should be a valid edge.

[ShaleXIONG]

Discussed offline: my suggestion is to investigate the possibility of representing Amo.Safe (and similarly, Amo.*) as macros/syntactic sugar, rather than as proper additional constructors of the rmw type. We already do a similar macro expansion here for allRW etc.

[update]
I have a quick hack. Half way, I realise it is not a straightforward task. The problem here is relax macro unfold does not depends on the architecture now while edge unfold does. The actual parse and unfold process is as the follow:

• Assume an input relaxation $R$, if $R$ is an individual relax, it triggers relax macro unfold, while if it is a composite relax, it will NOT; I can fix this with a patch.
• If there is no macro unfold above, it will parse individual input string to an internal data structure edge, that is {atom_1, edge, atom_2}. Note that individual annotations are not merged with edges nor type check here. This overall process results a relax type which is effectively ERS of edge list. (There is a legacy PPO contractor in relax which I want to remove, too)
• Afterwards, the edges will be unfolded, which unfolds all the wildcard edges into the primitive edges.
• Last, cycle, in other words edge lists, will be resolved, when (1) annotations will be merged into edges, based on the data structure above, (1) annotations between adjacent edges will type checked and merged, and (3) adjacent edges will be type checked, for example read cannot match write etc.

In general, introducing Amo.Safe as macro will be a major change. We need a new macro mapping table based on architecture. The long term idea is probably remove the edge unfold step while shift all the wildcard edge into macro unfold. This will be a major change.

[relokin]

I agree with Filippo's comment and eventually we need to add support for macros. I am happy to merge this for now (if you address my one comment) but there are several cases where macros could tidy up the conf file.

[ShaleXIONG]

I agree with Filippo's comment and eventually we need to add support for macros. I am happy to merge this for now (if you address my one comment) but there are several cases where macros could tidy up the conf file.

You mean the clarification on the Amo.Safe ? I have updated the comments in the code.

I totally agree here, it will be useful to

• move all the wildcard edge type definition into macro unfold. This means introducing a new interface for different architectures to provide a macro unfold table. Therefore wildcard edge/macro is resolved much easier. This can also remove a lot of code in edge.ml and make the edge.ml focus on functionality related to individual edge.
• Pass all the macro to -show edges or -list in diy7. Currently macros such as AllRW, are not in the list, yet they are valid input relaxation.

[fsestini]

In general, introducing Amo.Safe as macro will be a major change. We need a new macro mapping table based on architecture. The long term idea is probably remove the edge unfold step while shift all the wildcard edge into macro unfold. This will be a major change.

I see. So essentially we would need architecture-specific macro expansion, but as of now macros can only apply generally to all archs as part of an earlier pre-processing step.

I'm fine with merging this for now (once @relokin and I are happy with the improved comments/documentation), but it would be great if we can revisit the macro implementation at some point. There are quite a few points in the code where we pattern match on edge constructors but assert false on wildcards/macros constructors, which IMO strongly suggests these two concepts should not be mixed together.

[ShaleXIONG]

In general, introducing Amo.Safe as macro will be a major change. We need a new macro mapping table based on architecture. The long term idea is probably remove the edge unfold step while shift all the wildcard edge into macro unfold. This will be a major change.

I see. So essentially we would need architecture-specific macro expansion, but as of now macros can only apply generally to all archs as part of an earlier pre-processing step.

I'm fine with merging this for now (once @relokin and I are happy with the improved comments/documentation), but it would be great if we can revisit the macro implementation at some point. There are quite a few points in the code where we pattern match on edge constructors but assert false on wildcards/macros constructors, which IMO strongly suggests these two concepts should not be mixed together.

I will work on this unification behind the scene as it is much more disrupted yet does not provide new functionality that needs to be merged in this pull request. Once I have a result, I will open a separate code improvement pull request.

[fsestini]

A few minor suggestions.

[fsestini]

I think this is fine to merge once @relokin is happy with the updated comment, subject to a future patch that will try to implement SafeAmo and similar as "macros" instead of concrete constructors.

[ShaleXIONG]

I think this is fine to merge once @relokin is happy with the updated comment, subject to a future patch that will try to implement SafeAmo and similar as "macros" instead of concrete constructors.

I have opened an issue #1784 to document the discussion here on rework macro and wildcard.

[relokin]

I am really sorry but for some reason, I added my review without posting my one comment. Shale has changed the comment since I reviewed but I think my comment is still valid.

[relokin]

Feel free to rebase, rework the history and merge!