[gen] Rework AArch64 access atoms

[ShaleXIONG]

This PR reworks AArch64 generator atoms into a structured representation that separates the kind of access from its ordering semantics.

Problems with the old representation

The old representation was:

type atom_acc =
  | Plain of capa_opt
  | Acq of capa_opt
  | AcqPc of capa_opt
  | Rel of capa_opt
  | Atomic of atom_rw
  | Tag
  | CapaTag
  | CapaSeal
  | Pte of atom_pte
  | Neon of neon_opt
  | Pair of [ld_pair_opt | st_pair_opt] * pair_idx
  | Instr

type atom = atom_acc * MachMixed.t option

Ordinary and Morello accesses shared the same constructors

Plain, Acq, AcqPc, and Rel represented both ordinary accesses and Morello capability accesses. The capa_opt payload distinguished them:

Plain None              (* ordinary plain access *)
Plain (Some Capability) (* Morello plain access *)
Acq None                (* ordinary acquire access *)
Acq (Some Capability)   (* Morello acquire access *)

Consequently, code not relavant to morello had to inspect an option nested inside the ordering constructor. The common ordinary path always carried None, while Morello-specific behavior was encoded indirectly as Some Capability.
This also made constructor names incomplete descriptions of their values. For example, Plain did not by itself mean an ordinary plain access, and Acq did not by itself identify the accessed data kind.

Mixed size was represented as an independent optional dimension

Every atom was paired with a MachMixed.t option, even though only ordinary and atomic accesses meaningfully support mixed sizes. For example:

(Acq None, Some (MachSize.Byte, 0))

represented an acquire mixed-size access such as A.b0.

For non-mixed accesses, the second component was always None. More importantly, the type could also express combinations that have no valid meaning, such as attaching a mixed size to Tag, Pte, Neon, Instr, or a Morello capability access. These combinations had to be rejected or ignored later by convention. Code handling an atom therefore had to combine two independent matches: one over atom_acc and another over MachMixed.t option. Ordinary and mixed-size versions of the same operation often appeared in separate branches even when their behavior was otherwise identical.

PTE ordering semantics were encoded in constructor names

The old PTE representation was:

type atom_pte =
  | Read
  | ReadAcq
  | ReadAcqPc
  | Set of WPTESet.t
  | SetRel of WPTESet.t
  | ReadHAAcq
  | ReadHAAcqPc

This mixed the PTE operation with its ordering semantics:

• Read, ReadAcq, and ReadAcqPc represented the same read operation with plain, acquire, and acquire-PC ordering.
• Set and SetRel represented the same PTE-field update with plain and release ordering.
• ReadHAAcq and ReadHAAcqPc repeated the acquire distinction for the special HA read case.

As a result, changing only the ordering required changing constructors. For example, PteV1 and L were parsed as:

(Pte (Set V1), None)
(Rel None, None)

Their merge produced PteV1L by constructing:

(Pte (SetRel V1), None)

The release property moved from a general Rel constructor into the PTE-specific SetRel constructor. The same semantic operation was therefore represented differently depending on the access kind.

PteHA was especially subtle. Its plain form shared the Set representation for parsing reasons, while its acquire forms used dedicated read constructors. Code processing PTE atoms consequently needed special cases to determine whether HA described a read, a field update, or an ordered read.

Validity depended heavily on conventions outside the type

The old product type had many combinations that compilation could not use such as:

• a mixed-size Tag, Pte, Neon, Pair, or Instr atom;
• capability payloads on constructors for which capability access was not meaningful;
• PTE constructors combined with an unrelated MachMixed.t;
• ordering constructors applied to the wrong event direction;
• combinations whose two components independently looked valid but were invalid together.

These states were handled through repeated pattern matching, assertions, or later validation. Adding a constructor or semantic case required auditing printing, comparison, merging, enumeration, direction checking, machine-feature detection, and compilation code for both tuple components.

Atom operations duplicated representation knowledge

Printing, comparison, annotation merging, mixed-size handling, RMW validation, and compilation all needed to understand the same encoding rules:

• None versus Some Capability;
• None versus Some MachMixed.t;
• ordinary ordering constructors versus PTE-specific ordered constructors;
• special cases such as HA;
• constructors for which the tuple's second component had to remain None.

This produced large matches with similar branches and made it easy for two operations to interpret the same atom differently. It also made otherwise local changes to an access kind affect code throughout the generator.

New representation

Ordering is now represented explicitly:

type access_read = [ `Plain | `Acquire | `AcquirePC ]
type access_write = [ `Plain | `Release ]
type access_order = [ access_read | access_write ]

PTE operations carry an ordering appropriate to their direction:

type atom_pte =
  | Read of access_read
  | ReadHA of access_read
  | Set of access_write * WPTESet.t

The top-level atom identifies the access kind directly:

module StructuredAtom : sig
  type atomic_access =
    | AtomicOrdinary
    | AtomicSize of MachMixed.t

  type t =
    | OrdinaryAccess of access_order
    | MixedSizeAccess of access_order * MachMixed.t
    | MorelloAccess of access_order
    | PteAccess of atom_pte
    | NeonAccess of neon_opt
    | Atomic of atom_rw * atomic_access
    | MorelloTagAccess
    | MorelloSealAccess
    | MemoryTagAccess
    | PairAccess of [ld_pair_opt | st_pair_opt]
    | InstrAccess
end

This gives each semantic dimension one consistent location:

• the constructor identifies the access kind;
• access_read, access_write and then access_order for release-acquire order, which are used consistent through ordinary, vmsa, mixed-size and Morello;
• MachMixed.t appears only in constructors that support a mixed size;
• atom_rw continues to represent the read/write ordering of atomic operations;
• special accesses such as memory tags, Morello metadata, vector accesses, pairs, and instruction accesses no longer carry irrelevant optional values.

For example:

OrdinaryAccess `Acquire
MixedSizeAccess (`Acquire, (MachSize.Byte, 0))
MorelloAccess `Acquire
PteAccess (Read `Acquire)
PteAccess (Set (`Release, V1))

The PteV1 plus L merge now changes the ordering value while retaining the PTE operation and field set:

PteAccess (Set (`Plain, V1))
PteAccess (Set (`Release, V1))

Similarly, PteHA, PteHAA, and PteHAQ are represented as one operation with different read orders:

PteAccess (ReadHA `Plain)
PteAccess (ReadHA `Acquire)
PteAccess (ReadHA `AcquirePC)

Migration strategy

The migration is split into small commits. The structured representation is introduced alongside compatibility conversion, and individual consumers are then migrated in compilation order. Printing, comparison, enumeration, annotation merging, mixed-size handling, dependency compilation, RMW compilation, PTE compilation, vector compilation, and architecture metadata are moved incrementally before structured atoms become canonical.

Each commit is buildable, and the regression tests were generated before the refactoring so that the migration can be checked against the existing behavior at every stage.

Test suite

To ensure we preserve the existing behaviour. We introduce a new test suite to replace the old diycross7 +herd7 + checking log method. The old method is unnecessary via herd7 also the diycross7 inputs mixes various of testing targets. The new test suite includes individual test for edge and annotation. Each test file is a valid litmus test. Its first line is a comment containing the diyone7 command that reproduces the remainder of the file.

The suite contains eight AArch64 directories:

• AArch64 — Baseline coverage for Po, Dp*, atomic operations, and representative DMB/DSB fences. Annotations are tested around compilation-distinct edges such as PosRW, LxSx, Dp*, Amo.Cas, and Amo.Swp.
• AArch64.ifetch — Coverage for CacheSync*, DC.*, and IC.* edges, together with instruction annotations on representative dependency and atomic paths.
• AArch64.mixed — Mixed-size annotation coverage using representative sizes and offsets. It includes same-size and different-size pairs and exercises the CU, MixedDisjoint, and MixedStrictOverlap variants.
• AArch64.morello — Morello annotation coverage around PosRW, LxSx, representative dependencies, Amo.Cas, and Amo.Swp.
• AArch64.MTE — Memory-tagging coverage for the T annotation, including async and storeonly. Multi-process cases exercise fault generation.
• AArch64.vmsa — VMSA PTE annotation coverage. Representative annotations exercise dependency and atomic paths, while two-PTE combinations check compatibility and generated PTE values.
• AArch64.vector — Neon, SVE, and SME annotation coverage around representative plain, dependency, load-exclusive/store-exclusive, and atomic paths.
• AArch64.store — Focused coverage for the Store edge in each applicable direction.

These tests were generated before the refactoring began and provide a regression baseline to ensure that subsequent commits preserve existing behaviour.

[fsestini]

This PR adds thousands of files (mostly litmus tests as far as I can see). Were they added by mistake or was it intentional?

[ShaleXIONG]

This PR adds thousands of files (mostly litmus tests as far as I can see). Were they added by mistake or was it intentional?

I add a thorough test suite on diyone so we test all existing compilation paths (at least I am aware of). This includes valid and invalid diyone7 input. For example,

(* diyone7 -arch AArch64 -metadata false -oneloc DpAddrCselsW Rfi *)
AArch64 CoRW1+addrcsels-rfi
{
 0:X0=x;
}
 P0                  ;
 LDR W1,[X0]         ;
 CMP W1,W1           ;
 CSEL W2,WZR,WZR,EQ  ;
 MOV W3,#1           ;
 STR W3,[X0,W2,SXTW] ;

exists (0:X1=1)

it will read the first line to run the diyone7 ... and matching the following. I have read many small tests for cram might be too expensive. If we assembly all test into several cram files, those files become very long and difficult to audit. The test are organised similarly to the catalogues where one file per test case for better readability and also we can easily add a new test case.

[fsestini]

This PR adds thousands of files (mostly litmus tests as far as I can see). Were they added by mistake or was it intentional?

I add a thorough test suite on diyone so we test all existing compilation paths (at least I am aware of). This includes valid and invalid diyone7 input. For example,

I’m not sure just reducing some of the invalid paths is enough.

Cram tests should ideally be a curated and meaningful set of examples, each acting as representative of an input-output behaviour of interest, or a past bug. “Meaningful” is key: I see very little utility in having multiple golden tests exercising the same or very similar code paths. It just adds noise to the review process. For example, the two ifetch tests CoRW1+dc.cvauns-rfi.litmus and CoRW1+dc.cvaups-rfi.litmus look pretty much identical to me, and I struggle to see why we should have both, and how they are even relevant to the change being introduced in this PR to begin with. Perhaps they are and I just don’t see it, but in that case, maybe some additional clarification is needed.

Moreover, cram tests are only useful if they can be reviewed, to verify that their “expected output” is actually correct and indeed expected. However, this PR adds 3000+ tests, and I don’t think anyone could reasonably be asked to review all of them or even a tenth. So while I agree these cram tests are testing something, I’m not convinced they are necessarily testing for correct behaviour.

I’d suggest first identifying the core code paths and user-visible behaviours affected by this PR that need to be tested. Then we should think about whether those tests are better expressed as focused OCaml tests (e.g. using unit testing or property testing), or if they are actually better suited for broad end-to-end cram testing. If the latter, then I think we should then aim for one or maybe two curated cram tests per path.

I have read many small tests for cram might be too expensive.

It would be helpful to run benchmarks to better quantify this.

In general, whether they are "too" expensive or not also depends on their utility. A large test suite of cram tests accumulated over the years to capture meaningful behaviours might be time-expensive to run, but worth keeping nonetheless.

If we assembly all test into several cram files, those files become very long and difficult to audit.

I agree, but I think adding thousands of tests in one go will be difficult to audit in any case, whether they are put in a single file or multiple files.

[ShaleXIONG]

This PR adds thousands of files (mostly litmus tests as far as I can see). Were they added by mistake or was it intentional?

I add a thorough test suite on diyone so we test all existing compilation paths (at least I am aware of). This includes valid and invalid diyone7 input. For example,

I’m not sure just reducing some of the invalid paths is enough.

Cram tests should ideally be a curated and meaningful set of examples, each acting as representative of an input-output behaviour of interest, or a past bug. “Meaningful” is key: I see very little utility in having multiple golden tests exercising the same or very similar code paths. It just adds noise to the review process. For example, the two ifetch tests CoRW1+dc.cvauns-rfi.litmus and CoRW1+dc.cvaups-rfi.litmus look pretty much identical to me, and I struggle to see why we should have both, and how they are even relevant to the change being introduced in this PR to begin with. Perhaps they are and I just don’t see it, but in that case, maybe some additional clarification is needed.

Moreover, cram tests are only useful if they can be reviewed, to verify that their “expected output” is actually correct and indeed expected. However, this PR adds 3000+ tests, and I don’t think anyone could reasonably be asked to review all of them or even a tenth. So while I agree these cram tests are testing something, I’m not convinced they are necessarily testing for correct behaviour.

I’d suggest first identifying the core code paths and user-visible behaviours affected by this PR that need to be tested. Then we should think about whether those tests are better expressed as focused OCaml tests (e.g. using unit testing or property testing), or if they are actually better suited for broad end-to-end cram testing. If the latter, then I think we should then aim for one or maybe two curated cram tests per path.

I have read many small tests for cram might be too expensive.

It would be helpful to run benchmarks to better quantify this.

In general, whether they are "too" expensive or not also depends on their utility. A large test suite of cram tests accumulated over the years to capture meaningful behaviours might be time-expensive to run, but worth keeping nonetheless.

If we assembly all test into several cram files, those files become very long and difficult to audit.

I agree, but I think adding thousands of tests in one go will be difficult to audit in any case, whether they are put in a single file or multiple files.

Let me go through all the test cases again. I think to ensure the semantics equivalent we need to have test to cover behaviour regarding (1) one annotation and (2) pair of annotations in combine with (a) read or (b) write. Those should cover all the path regarding annotation. Current it exhausted all the combination but I think I can present the test based on group of annotation and only add a few test cases for a group.

[fsestini]

Rework AArch64 generator atoms into a structured representation that separates the access type from its ordering semantics. This is from the old

type atom_acc =
  | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt
  | Atomic of atom_rw | Tag | CapaTag | CapaSeal | Pte of atom_pte | Neon of neon_opt
  | Pair of [ld_pair_opt | st_pair_opt] * pair_idx | Instr

to the new structure type

type t =
  { access_type : access_type; (* for release acquire etc *)
    access_order : access_order; } (* for mixed-size, morello, memory tag, pte, pair, simd, ifetch etc *)

The new type separate out the access type from the order. This means:

• capa_opt for morello moves out of the access_type.
• Previously annotation like PteA represented as Pte of "PteA", is needed for representing acquire read off Pte but now it be separate annotation in both the syntaxPte A and internal data type.

Can you elaborate on why do you think this is an improvement over the previous representation? This description shows how PteA can be represented by the two versions of the atom type, but not why the new version is better than the old.

At a glance, the new representation looks less precise than the old in some cases. For example, the old atom_acc type does not provide a way to express "acquire tag" accesses. This is good, because "acquire tag" is an invalid combination, so the type's structure is helpfully ruling out non-sensical values thus enforcing the principle of "making invalid states unrepresentable". However the new type t does have a constructor for "acquire tag". Granted, we can use is_valid to check if a t value represents a valid combination of access_type and access_order. But it's easy to forget calling is_valid, and the typechecker won't help you if you do forget.

[ShaleXIONG]

Rework AArch64 generator atoms into a structured representation that separates the access type from its ordering semantics. This is from the old

type atom_acc =
  | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt
  | Atomic of atom_rw | Tag | CapaTag | CapaSeal | Pte of atom_pte | Neon of neon_opt
  | Pair of [ld_pair_opt | st_pair_opt] * pair_idx | Instr

to the new structure type

type t =
  { access_type : access_type; (* for release acquire etc *)
    access_order : access_order; } (* for mixed-size, morello, memory tag, pte, pair, simd, ifetch etc *)

The new type separate out the access type from the order. This means:

• capa_opt for morello moves out of the access_type.
• Previously annotation like PteA represented as Pte of "PteA", is needed for representing acquire read off Pte but now it be separate annotation in both the syntaxPte A and internal data type.

Can you elaborate on why do you think this is an improvement over the previous representation? This description shows how PteA can be represented by the two versions of the atom type, but not why the new version is better than the old.

At a glance, the new representation looks less precise than the old in some cases. For example, the old atom_acc type does not provide a way to express "acquire tag" accesses. This is good, because "acquire tag" is an invalid combination, so the type's structure is helpfully ruling out non-sensical values thus enforcing the principle of "making invalid states unrepresentable". However the new type t does have a constructor for "acquire tag". Granted, we can use is_valid to check if a t value represents a valid combination of access_type and access_order. But it's easy to forget calling is_valid, and the typechecker won't help you if you do forget.

First to clarify the old type was technically defined as :

type atom_acc =
  | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt
  | Atomic of atom_rw | Tag | CapaTag | CapaSeal | Pte of atom_pte | Neon of neon_opt
  | Pair of [ld_pair_opt | st_pair_opt] * pair_idx | Instr
type atom = atom_acc * MachMixed.t option

where there was a second projection MachMixed.t option used for mixed size operation.
The problem on the old type was that many variant specific instructions (not all as you mention tag) has acq-rel semantics, including baseline, morello, mixed size, pte, pair operations. Those were not represented uniformly, in particular,

• for baseline and morello, it used | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt where the capa_opt a option type for if it is a morello access
• for mixed size, it used the second project and Plain | Acq | ..., for example (Acq (None), Some Byte 0) was acq access for the 0-byte of a location
• for Pte, pair, Neon (including sve,sme,neon), the acq-rel semantics were wrapped inside the atom_pte, [ld_pair_opt | st_pair_opt], and neon_pot type definitions respectively; those types by-pass the outer Plain | Acq | .... (with some is_valid check if in annotation merge).

We could make it more restrictive by designing type that rules out acq-rel semantics to tag, ifetch and neon. However, I decide to make it slightly simpler of two fields in a structure and rule out same invalid cases. There was a similar is_valid check in the past because many combinations were invalid in the old typing atom_acc * MachMixed.t option.

[fsestini]

• for baseline and morello, it used | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt where the capa_opt a option type for if it is a morello access
• for mixed size, it used the second project and Plain | Acq | ..., for example (Acq (None), Some Byte 0) was acq access for the 0-byte of a location
• for Pte and pair, the acq-rel semantics were wrapped inside the atom_pte or [ld_pair_opt | st_pair_opt] type definition, which by-passes the outer Plain | Acq | .... (with some is_valid check if in annotation merge)

One thing I find particularly confusing in this representation is that it suggest the incorrect equivalence "acquire access <--> Acq constructor" (and similar for AcqPc and Rel). However, as you point out, there are other ways to construct an aquire access, but you wouldn't immediately guess it by looking at this type.

Have you considered replacing this line:

  | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt

with a single constructor like so:

  type acq_rel = Plain | Acq | AcqPc | Rel

  type generic_access = {
    acq_rel : acq_rel;
    capa : capa_opt;
  }

  type atom_acc =
    | Generic of generic_access
    | ...

Perhaps this might help in making things a bit more symmetrical/uniform.

However, I decide to make it slightly simpler of two fields in a structure and rule out same invalid cases.

I'm all for simple types where possible, however the simplification proposed here impacts the type-safety and general robustness of the code, so I think its tradeoffs should be highlighted and weighed against alternative solutions.

I'm also not entirely sure the proposed approach makes the implementation simpler overall, at least by looking at the diff. I think it would be useful to see some spelled-out concrete examples of code that was positively impacted (in terms of simplicity, readability, etc.) by the change proposed in this PR. In other words, I'm trying to understand whether the goal of this PR is just to make the atom types simpler/more uniform (which could be a valid goal to have, on its own), or if it's also aiming to unlock some additional maintenance benefit in downstream code that uses those types.

There was a similar is_valid check in the past because many combinations were invalid in the old typing atom_acc * MachMixed.t option.

Right, but the version of is_valid post-PR seems to be doing a lot more work than before.

[ShaleXIONG]

• for baseline and morello, it used | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt where the capa_opt a option type for if it is a morello access
• for mixed size, it used the second project and Plain | Acq | ..., for example (Acq (None), Some Byte 0) was acq access for the 0-byte of a location
• for Pte and pair, the acq-rel semantics were wrapped inside the atom_pte or [ld_pair_opt | st_pair_opt] type definition, which by-passes the outer Plain | Acq | .... (with some is_valid check if in annotation merge)

One thing I find particularly confusing in this representation is that it suggest the incorrect equivalence "acquire access <--> Acq constructor" (and similar for AcqPc and Rel). However, as you point out, there are other ways to construct an aquire access, but you wouldn't immediately guess it by looking at this type.

Have you considered replacing this line:

  | Plain of capa_opt | Acq of capa_opt | AcqPc of capa_opt | Rel of capa_opt

with a single constructor like so:

  type acq_rel = Plain | Acq | AcqPc | Rel

  type generic_access = {
    acq_rel : acq_rel;
    capa : capa_opt;
  }

  type atom_acc =
    | Generic of generic_access
    | ...

Can you elaborate a bit further here ? Here I think there is still different between mixed-size acq, (Acq (None), Some Byte 0) vs Pte-acq, Pte (AcqRead). The acq is still not unified?

Perhaps this might help in making things a bit more symmetrical/uniform.

However, I decide to make it slightly simpler of two fields in a structure and rule out same invalid cases.

I'm all for simple types where possible, however the simplification proposed here impacts the type-safety and general robustness of the code, so I think its tradeoffs should be highlighted and weighed against alternative solutions.

I'm also not entirely sure the proposed approach makes the implementation simpler overall, at least by looking at the diff. I think it would be useful to see some spelled-out concrete examples of code that was positively impacted (in terms of simplicity, readability, etc.) by the change proposed in this PR. In other words, I'm trying to understand whether the goal of this PR is just to make the atom types simpler/more uniform (which could be a valid goal to have, on its own), or if it's also aiming to unlock some additional maintenance benefit in downstream code that uses those types.

There was a similar is_valid check in the past because many combinations were invalid in the old typing atom_acc * MachMixed.t option.

Right, but the version of is_valid post-PR seems to be doing a lot more work than before.

Yes and No. If we are talking about a single annotation, the actually complexity is in the pp function: the data type with a valid pp will be valid syntax. However regarding annotation merging, we now relies mostly on is_valid function, rather than old-version, where a de facto a is_valid function is encoded in a big match to ensure two annotation can be merged.

[fsestini]

Can you elaborate a bit further here ? Here I think there is still different between mixed-size acq, (Acq (None), Some Byte 0) vs Pte-acq, Pte (AcqRead). The acq is still not unified?

Sure. Indeed I wasn't proposing a way to completely unify every instance of access order. Rather, that was a (sketched and incomplete) idea to address the specific asymmetry I was concerned with, which sees the same atom_acc type including constructors for access order (Acq, Rel, ...) and at the same time constructors for access types (Pte, Tag, ...). In my opinion this is mixing up different concerns, and is potentially confusing. My proposal was to collect the various Acq, Rel, etc. under a single Generic constructor (equivalent to your OrdinaryAccess) to make things more balanced: one constructor per access type, each optionally specifying some access order as a parameter:

type atom_acc = 
  | AccessType1 of acc_type_1_order
  | AccessType2 of acc_type_2_order
  | ...

There may be more opportunities for clean-up in addition to just adding a Generic/Ordinary constructor. For example, one could also move the mixed size logic into an additional constructor MixedAccess. I think my overall point is that it's worth exploring to what extent we can clean up and improve this type without throwing away its nice "valid by construction" properties.

[ShaleXIONG]

This PR adds thousands of files (mostly litmus tests as far as I can see). Were they added by mistake or was it intentional?

I add a thorough test suite on diyone so we test all existing compilation paths (at least I am aware of). This includes valid and invalid diyone7 input. For example,

I’m not sure just reducing some of the invalid paths is enough.
Cram tests should ideally be a curated and meaningful set of examples, each acting as representative of an input-output behaviour of interest, or a past bug. “Meaningful” is key: I see very little utility in having multiple golden tests exercising the same or very similar code paths. It just adds noise to the review process. For example, the two ifetch tests CoRW1+dc.cvauns-rfi.litmus and CoRW1+dc.cvaups-rfi.litmus look pretty much identical to me, and I struggle to see why we should have both, and how they are even relevant to the change being introduced in this PR to begin with. Perhaps they are and I just don’t see it, but in that case, maybe some additional clarification is needed.
Moreover, cram tests are only useful if they can be reviewed, to verify that their “expected output” is actually correct and indeed expected. However, this PR adds 3000+ tests, and I don’t think anyone could reasonably be asked to review all of them or even a tenth. So while I agree these cram tests are testing something, I’m not convinced they are necessarily testing for correct behaviour.
I’d suggest first identifying the core code paths and user-visible behaviours affected by this PR that need to be tested. Then we should think about whether those tests are better expressed as focused OCaml tests (e.g. using unit testing or property testing), or if they are actually better suited for broad end-to-end cram testing. If the latter, then I think we should then aim for one or maybe two curated cram tests per path.

I have read many small tests for cram might be too expensive.

It would be helpful to run benchmarks to better quantify this.
In general, whether they are "too" expensive or not also depends on their utility. A large test suite of cram tests accumulated over the years to capture meaningful behaviours might be time-expensive to run, but worth keeping nonetheless.

If we assembly all test into several cram files, those files become very long and difficult to audit.

I agree, but I think adding thousands of tests in one go will be difficult to audit in any case, whether they are put in a single file or multiple files.

Let me go through all the test cases again. I think to ensure the semantics equivalent we need to have test to cover behaviour regarding (1) one annotation and (2) pair of annotations in combine with (a) read or (b) write. Those should cover all the path regarding annotation. Current it exhausted all the combination but I think I can present the test based on group of annotation and only add a few test cases for a group.

I reduce the test cases to a similar size as before now but more importantly, I hope it becomes clearer and more representative.

First the old way rely only diycross to generate a list of tests and pipe it through herd7 to check if they still give the same logs. The old cycle was often unnecessary long, for example in the mixed mode, the old cycle were around 6-8 long. Separately what they are testing were not very clear to me.

To ensure this refactor on type atom is semantics equivalent, I basically craft a new test suite with file likes:

(* diyone7 -arch AArch64 -metadata false -oneloc DpAddrCselsW Rfi *)
AArch64 CoRW1+addrcsels-rfi
{
 0:X0=x;
}
 P0                  ;
 LDR W1,[X0]         ;
 CMP W1,W1           ;
 CSEL W2,WZR,WZR,EQ  ;
 MOV W3,#1           ;
 STR W3,[X0,W2,SXTW] ;

exists (0:X1=1)

I particularly want this file is a valid litmus test with the first commented-out like is the diyone7 commands. The new test suite contains 8 directories, where I try to mimic the directory name in catalogue.

• AArch64. It test for baseline. It contains single-process tests case for edges include Po, Dp*, Amo.Cas, Amo.Swp, Amo.StAdd, Amo.LdAdd, DMB.LD/ST/SY, DSB.LD/ST/SY. The Amo.StAdd and Amo.LdAdd are chosen to present other Amo.St* and Amo.Ld*. Similarly DMB.* and DSB.* are chosen to present other fence. For those edge need to specify location/R/W. We enumerate possible combination. After the test case for single edges, we systematically apply one annotation before or after PosRW LxSx Dp, Amo.Cas and Amo.Swp. Those edges has unique compilation path in AArch64Compile_gen.ml
• ifetch. we add extra test for new fence-like, i.e., CacheSync***, DC.* and IC.*, those three fences are in different contractors in code. Similar we apply annotation before and after PosRW LxSx Dp, Amo.Cas and Amo.Swp.
• mixed. Here there are only new annotations like b1 h2 and w0. For each latter we pick two numbers, i.e., b1, b2, h0, h2, w0, w4 and q0, we pair them and apply pairs to PosRW, Amo.Cas, Amo.Swp and LxSx. Since those annotation only change the instruction so we omit applying them to Dp* here to reduce the number of tests.
• morello. There are only new annotations. Hence we apply the new annotation before or after PosRW Amo.Cas, Amo.Swp.
• MTE. There is only one new annotation T. However there are two-sub variants stroreonly and async. For the memtag itself, we apply T to PosRW, Dp, Amo.Cas and Amo.Swp. Separately to check the fault-generation, we also apply T to MP-litmus tests. For those tests that generate fault, we also apply storeonly and async to ensure the correct behaviour.
• vmsa. There are a lot of new annotation here which can be represented by four annotations PteV1, Pte, PteHA, PteHD. Similar to many other variant, we apply it before and after PosRW, Amo.Cas and Amo.Swp. We also add test with two annotations, for example PteV1 PteAF1 and PteHA PteV1, this is necessary to check compatibility and if the correct value of Pte is generated.
• vector. There are three sub-variants, neon, sve and sme. Since there are only new annotations, so we apply then before and after PosRW, Amo.Cas and Amo.Swp again.

In short, the test are generated BEFORE any refactoring so it ensure any of the future commits does not change the existing expected behaviours

[ShaleXIONG]

Can you elaborate a bit further here ? Here I think there is still different between mixed-size acq, (Acq (None), Some Byte 0) vs Pte-acq, Pte (AcqRead). The acq is still not unified?

Sure. Indeed I wasn't proposing a way to completely unify every instance of access order. Rather, that was a (sketched and incomplete) idea to address the specific asymmetry I was concerned with, which sees the same atom_acc type including constructors for access order (Acq, Rel, ...) and at the same time constructors for access types (Pte, Tag, ...). In my opinion this is mixing up different concerns, and is potentially confusing. My proposal was to collect the various Acq, Rel, etc. under a single Generic constructor (equivalent to your OrdinaryAccess) to make things more balanced: one constructor per access type, each optionally specifying some access order as a parameter:

type atom_acc = 
  | AccessType1 of acc_type_1_order
  | AccessType2 of acc_type_2_order
  | ...

There may be more opportunities for clean-up in addition to just adding a Generic/Ordinary constructor. For example, one could also move the mixed size logic into an additional constructor MixedAccess. I think my overall point is that it's worth exploring to what extent we can clean up and improve this type without throwing away its nice "valid by construction" properties.

it was not valid by construction in the past due to the mixed-size. Considering (Neon Ne1, Some (Byte, 0)) as (* type atom = atom_acc * MachMixed.t option *).

I think we can do type atom = Plain of X | Acq of X | AcqPc of X | Rel of X | Tag | Instr | CapaTag | CapaSeal and then X wrap the rest constructors that allowed rel-acq semantics? Do you think it makes sense?

The following up question is X is still need check validity against Acq Rel. Though it should be smaller than here. For example Pte on read can be only Rel not Acq. Also I do not think it is a good idea to define Pte related type in two different locations at least for this commit PR, because different sub-variant contains specific functionality and it will be better they are structure together.

[fsestini]

it was not valid by construction in the past due to the mixed-size. Considering (Neon Ne1, Some (Byte, 0)) as (* type atom = atom_acc * MachMixed.t option *).

Correct, so let me be more specific: it wasn't “valid by construction” in 100% of cases. But it was at least partly so, to a good extent.

I think we can do type atom = Plain of X | Acq of X | AcqPc of X | Rel of X | Tag | Instr | CapaTag | CapaSeal and then X wrap the rest constructors that allowed rel-acq semantics? Do you think it makes sense?

I feel like I would still find this confusing, as I would ask myself in what way is Acq an alternative to Tag. Moreover as you pointed out this representation allows incorrect values like Rel (Pte Read).

[ShaleXIONG]

it was not valid by construction in the past due to the mixed-size. Considering (Neon Ne1, Some (Byte, 0)) as (* type atom = atom_acc * MachMixed.t option *).

Correct, so let me be more specific: it wasn't “valid by construction” in 100% of cases. But it was at least partly so, to a good extent.

I think we can do type atom = Plain of X | Acq of X | AcqPc of X | Rel of X | Tag | Instr | CapaTag | CapaSeal and then X wrap the rest constructors that allowed rel-acq semantics? Do you think it makes sense?

I feel like I would still find this confusing, as I would ask myself in what way is Acq an alternative to Tag. Moreover as you pointed out this representation allows incorrect values like Rel (Pte Read).

I think I am trying to avoid splitting some existing typing here for example type pte_atom = Pte | PteV1 | .... hence I think it should remain relatively untouched as X here. What do you think the best way here. It will be also nice for type pte_atom do NOT need to define a rel-acq in its own definition but get from the outside wrap; that is why I was saying Plain of X | .... Do have better idea here ?

[TiberiuBucur]

I have not had a look at individual tests yet. Will get back to that tomorrow.

[psafont]

When it's not possible to ensure a type that's valid by construction, one solution I've found to work well is to make the type module-private. While this is a compromise, I've found it to work well in several occasions. Making the type module-private excludes code that is not from the module to construct values of the type. This means it's easy to create constructor functions that tests properties of the components before returning valid values for the type. This pattern also allows users to pattern-match the type as well.

This means we have gained a valuable property, construction is now localised into a few (if not one) functions. It's now easy to verify the properties using unit-testing and property-based testing (if needed), and it's also nicer to review and believe that the code is correct and nothing slipped through the cracks. And if it did, it's also easier to fix.

Here's an example where a record was needed and the implementing types (ints) allowed way more values that what's actually valid. The module has the private type, a single constructor function (decode_st_dev), and some test-only functions to test diverging behaviour in the platform:

xapi-project/xen-api@7eae57c#diff-4f6dd276360a0eb59305e20b9febd7d5f7baaebdb499d2483a8d3aefa5919cb2R317

In this commit the module is used, showing pattern-matching to extract values from the record: xapi-project/xen-api@6046cce

Another cases where bounded floats were needed: xapi-project/xen-api@76eed66#diff-f8c1c61e079650079206ad08e503aee1a90065d39872f330c7bc37b2e8bee7d4R23

[ShaleXIONG]

When it's not possible to ensure a type that's valid by construction, one solution I've found to work well in several occasions, even if it's a compromise is to make the type type module-private. This means only code within the module can construct values of this types. This means it's easy to create constructor functions that tests properties of the components before returning valid values for the type. This also allows users to pattern-match the record type as well.

This also means it's quite easy to tests these functions and because construction is restricted to a single site it's also easy to review, which makes verification easier.

Here's an example where a record was needed and the implementing types (ints) allow way more values that what's actually allowed. The module has the private type, a single constructor function (decode_st_dev), and some test-only functions to test diverging behaviour in the platform

xapi-project/xen-api@7eae57c#diff-4f6dd276360a0eb59305e20b9febd7d5f7baaebdb499d2483a8d3aefa5919cb2R317

In this commit, the module is used, showing pattern-matching to extract values from the record: xapi-project/xen-api@6046cce

Another cases where bounded floats are needed: xapi-project/xen-api@76eed66#diff-f8c1c61e079650079206ad08e503aee1a90065d39872f330c7bc37b2e8bee7d4R23

Thanks for the suggestion ! I will read it. I have chatted with @fsestini offline, as we will tighter the type definition so it is closer to "correct" by construction here.

[TiberiuBucur]

I noticed this test is allowed, whilst the "non-strong" cachesync version with an ISB is forbidden. That is presumably because in the memory model Instr-obs is written in terms of DC.CVAU instructions. @artkhyzha is this on purpose?