Skip to content

[gen] Add wildcard Amo.Safe.#1745

Open
ShaleXIONG wants to merge 2 commits intoherd:masterfrom
ShaleXIONG:amo-wildcard
Open

[gen] Add wildcard Amo.Safe.#1745
ShaleXIONG wants to merge 2 commits intoherd:masterfrom
ShaleXIONG:amo-wildcard

Conversation

@ShaleXIONG
Copy link
Copy Markdown
Collaborator

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.

This wildcard unfold to `Amo.Cas` `Amo.Swp` `Amo.StAdd` and `Amo.LdAdd`.
@ShaleXIONG ShaleXIONG requested a review from relokin March 11, 2026 12:58
@fsestini
Copy link
Copy Markdown
Collaborator

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
Copy link
Copy Markdown
Collaborator Author

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
Copy link
Copy Markdown
Collaborator Author

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.

@ShaleXIONG ShaleXIONG requested a review from fsestini March 25, 2026 09:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants