[gen] Clarify "plain" atomic annotations

[fsestini]

atom option in gen/common/edge.ml is currently used to represent the "plain annotation" P. I personally find there's room for improvement, for a couple of reasons:

1. One would expect the value None : atom option to represent "absence of annotation", or a failure state, but it doesn't. This is particularly counter-intuitive (IMO) when looking at the signature of functions like parse_atom : string -> atom option and incorrectly expecting atom option to represent "failure to parse".
2. The semantics of P itself makes it more similar to a wildcard. P makes the annotated access plain by default, but does not enforce this property. Indeed, merging P with any non-P atom a equals a, so P really stands for "plain unless specified otherwise". I think it would be useful to also be able to express scenarios where a diy edge endpoint must be plain, and not just "plain unless specified otherwise".

To address both issues, I propose we:

• extend atom with a constructor to represent the P annotation, removing the need for atom option. P's behaviour as a "wildcard"/"default annotation" can be preserved by modifying the edge/atom merging functions accordingly. This will also make atom more in like with sd, ie, etc., all of which also define their own wildcard constructors.
• further extend atom with a completely new constructor to represent accesses that must be plain.

The can (and probably, should) address these two points in two separate PRs.

See original discussion here. CC @ShaleXIONG

[ShaleXIONG]

In short, I agree. I am gradually improving various part of code so I can reach the point I will update annotation of P with small affect to the codebase. One I am currently spending a small protion of Friday afternoon is a better parser, and a bug-fix/improvement on annotation merge.

• https://github.com/ShaleXIONG/herdtools7/tree/code-better-parser
• https://github.com/ShaleXIONG/herdtools7/tree/better-edge-merge
  Those two branches are actually ready to reviewed however I am pending it to not overwhelm the pull request pipeline.

To add more technical detail upon your proposal, we might add a new annotation M to represent plain memory access in contract to release/acquire L/A annotations. Therefore P can become wildcard to automatically unfold in diy7/diycross7. Or the opposite way as M is the wildcard for plain memory access and P is strengthened to become primitive. Separately I will probably modify the code to remove the atom option but always enforce a concrete atom.

I will look into if there is a simple fix so to make your side of work easier.

[fsestini]

In short, I agree. I am gradually improving various part of code so I can reach the point I will update annotation of P with small affect to the codebase. One I am currently spending a small protion of Friday afternoon is a better parser, and a bug-fix/improvement on annotation merge.

• https://github.com/ShaleXIONG/herdtools7/tree/code-better-parser
• https://github.com/ShaleXIONG/herdtools7/tree/better-edge-merge
  Those two branches are actually ready to reviewed however I am pending it to not overwhelm the pull request pipeline.

Thanks, will look at these soon (hopefully!)

To add more technical detail upon your proposal, we might add a new annotation M to represent plain memory access in contract to release/acquire L/A annotations. Therefore P can become wildcard to automatically unfold in diy7/diycross7.

This is essentially my idea. I.e., to keep P as it is, and add a new annotation to represent the "must be plain" case.

Or the opposite way as M is the wildcard for plain memory access and P is strengthened to become primitive.

I would definitely avoid that, as this would break many things, including user's established intuition about the semantics of P.