[WIP] [gen] Update baseline configuration for rmw

[ShaleXIONG]

Add several missing rmw relaxations since such relaxation can match memory access such as M, R, and W.

this pull requisition contains #1569 too.

[chacon01]

Thanks @ShaleXIONG! A couple of comments.

[ShaleXIONG]

There might a few things I might do before merge this pull, which might take a while:

• introduce include syntax so we can separate the baseline and rmw-enhancement version.
• Probably introduce syntax like [A|Q PosRW] which unfold to [A PosRW] and [Q PosRW]
• Wait [gen] Introduce more wildcard syntax in diy #1516 for this to be merged so we can use more wildcard syntax which will help us simply all the syntax. It becomes increasingly difficult to review and auditing this file.

However, I am planning to leave this pull request open so you (@chacon01) can use it.

[chacon01]

Amo and LxSx become tedious to enumerate the more the configuration file is restricted to prevent additional ordering. I see two issues:

• Several cases where an existing effect could be an Amo or LxSx without changing the meaning
• We can't create a general Rmw or Amo relaxation because it will include e.g. Amo.LdClr which has the value collision problem.

Perhaps the generator could support "user-defined" relaxations to help here e.g.

-define LdRmw LxSx|Amo.Swp|Amo.Cas|Amo.LdAdd
-define Rmw LdRmw|Amo.StAdd
...
-safe [A LdRmw PodW* ExpObs]
-safe [ExpObs PodWR Rmw L]

which would reduce the duplication everywhere else.

Additionally, perhaps an operation to make a relaxation "optional" e.g.

-safe [A Rmw? Pod** Rmw? ExpObs]

which would be equivalent to

-safe [A Pod** ExpObs]
-safe [A Rmw Pod** ExpObs]
-safe [A Pod** Rmw ExpObs]
-safe [A Rmw Pod** Rmw ExpObs]

[chacon01]

Be aware that tying to ExpObs here will prevent it from combining with other relaxations that begin with ExpObs or Hat. We will need some way to allow ExpObs to combine with itself and with Hat e.g. [DpCtrldW ExpObs] + [ExpObs PodRW L] -> DpCtrldW Fre PodRWPL or [DpCtrlIsbdR ExpObs] + [Hat LxSx] -> DpCtrlIsbdR Hat LxSx. I think expressing the possible combinations in the configuration file would be tedious and error-prone, so it'll likely need to be some option for the generator.

[chacon01]

[range([A];amo;[L])]; po; [Exp & M | Imp & Tag & R | MMU & FAULT] does not apply for LxSx, so this relaxation can be removed. While this will not produce allowed tests because we would need it to compose with a free Pod*R (that doesn't exist), it is inconsistent with the justifying comment.

For the Amo variants (and LxSx too), the generator will only compose these with the other relaxations which are properly ordered into the acquire read effect, so all the forbidden combinations will also be forbidden without the L.

[ShaleXIONG]

Amo and LxSx become tedious to enumerate the more the configuration file is restricted to prevent additional ordering. I see two issues:

• Several cases where an existing effect could be an Amo or LxSx without changing the meaning
• We can't create a general Rmw or Amo relaxation because it will include e.g. Amo.LdClr which has the value collision problem.

Perhaps the generator could support "user-defined" relaxations to help here e.g.

-define LdRmw LxSx|Amo.Swp|Amo.Cas|Amo.LdAdd
-define Rmw LdRmw|Amo.StAdd
...
-safe [A LdRmw PodW* ExpObs]
-safe [ExpObs PodWR Rmw L]

which would reduce the duplication everywhere else.

Additionally, perhaps an operation to make a relaxation "optional" e.g.

-safe [A Rmw? Pod** Rmw? ExpObs]

which would be equivalent to

-safe [A Pod** ExpObs]
-safe [A Rmw Pod** ExpObs]
-safe [A Pod** Rmw ExpObs]
-safe [A Rmw Pod** Rmw ExpObs]

User define is a good idea. I will probably use the let R = ... syntax in the hope I can copy-paste or reused some code in herd7.
The | syntax is introduced #1685 so it should be merged at some point.
Your proposal on ? is also a good idea. I will look into it.