Skip to content

[WIP][gen] memory tag diy7 configuration file#1836

Draft
ShaleXIONG wants to merge 18 commits into
herd:masterfrom
ShaleXIONG:memtag-conf
Draft

[WIP][gen] memory tag diy7 configuration file#1836
ShaleXIONG wants to merge 18 commits into
herd:masterfrom
ShaleXIONG:memtag-conf

Conversation

@ShaleXIONG

Copy link
Copy Markdown
Collaborator

No description provided.

ShaleXIONG and others added 18 commits June 30, 2026 12:28
Add equality helpers for code, edge components, dependencies, and RMWs.
This avoids polymorphic equality for `tedge` internals.
Use existing `compare_atom` for `atom` equality check.
Extend the relax AST with a predicate node and teach the lexer/parser to
recognise predicate applications such as `@before(...)` and `@after(...)`.

Add `map_predicate` support to the AST so predicate names can be
converted before expansion. Parse `before` and `after` into edge predicates,
then attach the parsed predicate to every edge produced by the decorated
relax expression.
Move predicate-specific relaxation filtering into Alt.Make, where diy7
predicate edges are represented.

Reject predicate-only relaxations and invalid before/after predicate
placement after expanding the plain relaxation through the existing
Relax.remove_invalid_relaxes path. Expose the predicate-aware filtering
helper for parser tests.
Teach the diy7 search to interpret leading `@before(...)` and trailing
`@after(...)` predicate edges when deciding whether two relaxation
fragments can be placed next to each other.
…tests.

For `...;po` and `...;po;[M]` in cat, we append the external
communication edges `Obs` in the translation. Similarly for `po;...` and
`[M];po;...`, we prefix `Obs`.
Add back `Amo.StAdd` and `Amo.LdAdd` as the representation for all other
atomic operation. We also remove `[Q Amo.* ***]` as `Q` cannot apply to
`Amo.*`
Split DumpAll's check/dump path into explicit and clear stages: atom variation,
edge resolution, normalisation, duplicate detection, test construction, and
final dumping.  This makes the ordering clearer and avoids rebuilding the same
test separately for each scope/name variant. It also massively simply error
handling.

minor:
- Change `mk_info` from a function over the normalised edge list into prepared
  metadata passed with the candidate.
- Make `Edge.varatom` return the list of atomic variations directly, leaving
  edge resolution to the DumpAll pipeline. This keeps varatom focused on atom
  enumeration and makes resolve_edges placement explicit.
Add earlier candidate checks in alt.ml before calling into DumpAll/test
construction
- It rejects candidates that already exceed the configured process or
  per-procedure instruction limit
- It checks both (1) the immediate adjacent boundary and (2) the effective
  non-pseudo memory-access boundary when concatenating relaxation.
- Rework on rejecting cycle or cycle segment.
  Replace the old reject substring/span helpers with direct cycle/list
  matching helpers used by both partial generation and last-minute checking.
  For the final check, we apply a simpler and more readable algorithm
  by checking if the `cycle @ cycle` contains any reject edge lists, which
  is much more efficient and readable compated to previous `cut` based.
Add an Adjacent helper for the diy7 cycle search that assigns local ids to
relaxation chunks and precomputes their adjacency compatibility.

This lets the recursive search use table lookups for repeated predecessor
checks instead of recomputing the filter and boundary predicate merge logic
on every call.
It now always decreases by `1`. Previously, it only decreases when the
input relax contain at least non-pseudo edge. This is unnecessary.
Add more consecutive none fault check. This rule out undesired situations
where a memory access does not fault but the consecutive one faults.
Generate AArch64 CSEL dependency variants using register self-compare
instead of hardcode comparison against zero. This makes the
selected CSEL path deterministic. It also removes the extra register
instruction.

Update the affected AArch64 generator baselines.
Add gen/libdir/memtag.conf for generating forbidden tests for memory
tags.
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.

1 participant