Open
Conversation
…ests. - Add comment for auditing the connect between cat file and the forbidden file. - Fix the problem on `Hat`. - Add a missing `[A|Q Amo.* Po*W*]`. - replace `[Pod** Amo.SwpAL]` by `[Po**R Amo.* L]`, where the latter is weaker then the former. - Remove all `Amo.St*` and `Amo.Ld*` that causes problems due to commutative where the cycle is not correctly formed or observable. - Add `DSB` edges too, whenever there is `DMB`.
relokin
pushed a commit
that referenced
this pull request
Nov 6, 2025
With FEAT_HAFDBS, in the case where one PE, P0, is configured with
hardware updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), but
another PE, P1, using the same translation tables is configured with
hardware updates of Dirty state disabled ((TCR_ELx.{HA, HD}={x, 0}),
the following scenario can occur:
* P1 has a copy of a writable-clean translation table entry cached in
a TLB.
* P0 performs a hardware update of Dirty state for that translation
table entry.
* A store is attempted on P1, and this hits the writable-clean
translation table entry cached in the TLB.
The architecture permits the store on P1 to generate a Permission
fault, because P1 has hardware updates of Dirty state disabled.
However, the formal memory model did not permit this outcome. The
changes below relax the memory model to permit this outcome, and
therefore match the rules described in section D8.5.2.1 "Hardware
management of the dirty state".
As a result the following test is architecturally forbidden:
AArch64 S.HU+dsb.sy+dsb.sy-isb
Variant=vmsa
TTHM=P0:HD
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
0:X1=x; 0:X3=y;
1:X1=x; 1:X3=y;
}
P0 | P1 ;
MOV W0,#1 | LDR W2,[X3] ;
STR W0,[X1] | DSB SY ;
DSB SY | ISB ;
MOV W2,#1 | MOV W0,#2 ;
STR W2,[X3] | STR W0,[X1] ;
exists (1:X2=1 /\ fault(P1,x))
In addition, in the case where a PE is configured with hardware
updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), the
architecture forbids the hardware update of Dirty state on the PE
until the associated store is known to be non-speculative and,
therefore, ahead of the address translation or the tag check of an
instruction earlier in program order. However, the formal memory
model allowed such an outcome to be observed. The changes below
strengthen the memory model to forbid this outcome, and therefore
match the rules described in section D8.5.2.1 "Hardware management of
the dirty state".
As a result, the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-ttd
TTHM=P1:HD
Variant=vmsa,fatal
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), valid:0);
pteval_t 0:X6=(oa:PA(y), valid:1); 0:X7=TTD(y);
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0); 0:X9=TTD(x);
1:X1=x; 1:X3=y;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STR X6,[X7] | L1: STR W0,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
and the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-tag
TTHM=P1:HD
Variant=vmsa,fatal,mte,sync
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), TaggedNormal);
0:X6=y:red; 0:X7=y:green;
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0);
0:X9=TTD(x);
1:X1=x; 1:X3=y:red;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STG X6,[X7] | L1: STR WZR,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
[asl reference] added missing EQ operator to list of Bool-Bool operations
[asl spec] updated function/relation typing/semantics qualifiers
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Implement the distinction. This separation permits the handling of AArch64 instructions as data in ASL code.
[herd,litmus] Instruction as code vs. instruction as data, ASL now handles AArch64 instructions as data
Implement the distinction. This separation permits the handling of AArch64 instructions as data in ASL code.
As a consequence, the following test can now be executed in `-variant asl` mode:
```
AArch64 L105
{
ins_t *p;
0:X1=p; 0:X6=P0:L0;
1:X1=p; 1:X6=P0:L1;
}
P0 | P1 ;
STR X6,[X1] | STR X6,[X1] ;
L0: | ;
ADD W4,W4,#1 | ;
L1: | ;
ADD W4,W4,#2 | ;
LDR X3,[X1] | ;
LDR W2,[X3] | ;
forall 0:X2=instr:"ADD W4,W4,#1" \/ 0:X2=instr:"ADD W4,W4,#2"
```
The PR seizes the opportunity of refactoring the instruction-as-data implementation. In particular minimal support litmus is added for PPC and confirmed for ARM.
[herd,asl] Generate more asl code from published xml This PR uses 2 other resources published by Arm Ltd to automatically generate some asl code. Main positive advantage is not to have to change the ASL code every release. It also decluters our hand-written ASL files. - **[herd,asl] Implement bunlder.py for systerm registers** - **[asl] Improve Pretty-printer** - **[asl,herd] Extract features from released json file** - **[git] Update gitignore with new file names** - **[asl] Cleanup unused executable**
The clean target depended on build target. As a consequence, `make clean-asl-pseudocode` triggered the download and extraction of the asl files before erasing them. Authored-by: Hadrien Renaud <hadrien.renaud2@arm.com>
[build] Remove dependency of clean in asl-pseudocode directory The clean target depended on build target. As a consequence `make clean-asl-pseudocode` triggers the download and extraction of the ASL files before erasing them.
[ASL Reference] fixes following a PDF review
relokin
pushed a commit
that referenced
this pull request
Dec 12, 2025
This change implements AARCH-24571 as published in the Arm
Architecture Reference Manual for A-profile architecture: Known issues
in Issue L.b.
With FEAT_HAFDBS, in the case where one PE, P0, is configured with
hardware updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), but
another PE, P1, using the same translation tables is configured with
hardware updates of Dirty state disabled ((TCR_ELx.{HA, HD}={x, 0}),
the following scenario can occur:
* P1 has a copy of a writable-clean translation table entry cached in
a TLB.
* P0 performs a hardware update of Dirty state for that translation
table entry.
* A store is attempted on P1, and this hits the writable-clean
translation table entry cached in the TLB.
The architecture permits the store on P1 to generate a Permission
fault, because P1 has hardware updates of Dirty state disabled.
However, the formal memory model did not permit this outcome. The
changes below relax the memory model to permit this outcome, and
therefore match the rules described in section D8.5.2.1 "Hardware
management of the dirty state".
As a result the following test is architecturally forbidden:
AArch64 S.HU+dsb.sy+dsb.sy-isb
Variant=vmsa
TTHM=P0:HD
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
0:X1=x; 0:X3=y;
1:X1=x; 1:X3=y;
}
P0 | P1 ;
MOV W0,#1 | LDR W2,[X3] ;
STR W0,[X1] | DSB SY ;
DSB SY | ISB ;
MOV W2,#1 | MOV W0,#2 ;
STR W2,[X3] | STR W0,[X1] ;
exists (1:X2=1 /\ fault(P1,x))
In addition, in the case where a PE is configured with hardware
updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), the
architecture forbids the hardware update of Dirty state on the PE
until the associated store is known to be non-speculative and,
therefore, ahead of the address translation or the tag check of an
instruction earlier in program order. However, the formal memory
model allowed such an outcome to be observed. The changes below
strengthen the memory model to forbid this outcome, and therefore
match the rules described in section D8.5.2.1 "Hardware management of
the dirty state".
As a result, the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-ttd
TTHM=P1:HD
Variant=vmsa,fatal
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), valid:0);
pteval_t 0:X6=(oa:PA(y), valid:1); 0:X7=TTD(y);
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0); 0:X9=TTD(x);
1:X1=x; 1:X3=y;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STR X6,[X7] | L1: STR W0,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
and the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-tag
TTHM=P1:HD
Variant=vmsa,fatal,mte,sync
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), TaggedNormal);
0:X6=y:red; 0:X7=y:green;
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0);
0:X9=TTD(x);
1:X1=x; 1:X3=y:red;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STG X6,[X7] | L1: STR WZR,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
[asl reference] a few more fixes
Co-authored-by: Hadrien Renaud <Hadrien.Renaud2@arm.com>
Also when it edits the run-litmus workflow
[ci] add forgotten apt update Automated actions for running litmus in CI have failed this weekend. This is a tentative fix. See an [example failed workflow](https://github.com/HadrienRenaud/herdtools7/actions/runs/20002549485/job/57414307179)
relokin
pushed a commit
that referenced
this pull request
Dec 12, 2025
This change implements AARCH-24571 as published in the Arm
Architecture Reference Manual for A-profile architecture: Known issues
in Issue L.b.
With FEAT_HAFDBS, in the case where one PE, P0, is configured with
hardware updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), but
another PE, P1, using the same translation tables is configured with
hardware updates of Dirty state disabled ((TCR_ELx.{HA, HD}={x, 0}),
the following scenario can occur:
* P1 has a copy of a writable-clean translation table entry cached in
a TLB.
* P0 performs a hardware update of Dirty state for that translation
table entry.
* A store is attempted on P1, and this hits the writable-clean
translation table entry cached in the TLB.
The architecture permits the store on P1 to generate a Permission
fault, because P1 has hardware updates of Dirty state disabled.
However, the formal memory model did not permit this outcome. The
changes below relax the memory model to permit this outcome, and
therefore match the rules described in section D8.5.2.1 "Hardware
management of the dirty state".
As a result the following test is architecturally forbidden:
AArch64 S.HU+dsb.sy+dsb.sy-isb
Variant=vmsa
TTHM=P0:HD
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
0:X1=x; 0:X3=y;
1:X1=x; 1:X3=y;
}
P0 | P1 ;
MOV W0,#1 | LDR W2,[X3] ;
STR W0,[X1] | DSB SY ;
DSB SY | ISB ;
MOV W2,#1 | MOV W0,#2 ;
STR W2,[X3] | STR W0,[X1] ;
exists (1:X2=1 /\ fault(P1,x))
In addition, in the case where a PE is configured with hardware
updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), the
architecture forbids the hardware update of Dirty state on the PE
until the associated store is known to be non-speculative and,
therefore, ahead of the address translation or the tag check of an
instruction earlier in program order. However, the formal memory
model allowed such an outcome to be observed. The changes below
strengthen the memory model to forbid this outcome, and therefore
match the rules described in section D8.5.2.1 "Hardware management of
the dirty state".
As a result, the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-ttd
TTHM=P1:HD
Variant=vmsa,fatal
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), valid:0);
pteval_t 0:X6=(oa:PA(y), valid:1); 0:X7=TTD(y);
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0); 0:X9=TTD(x);
1:X1=x; 1:X3=y;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STR X6,[X7] | L1: STR W0,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
and the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-tag
TTHM=P1:HD
Variant=vmsa,fatal,mte,sync
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), TaggedNormal);
0:X6=y:red; 0:X7=y:green;
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0);
0:X9=TTD(x);
1:X1=x; 1:X3=y:red;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STG X6,[X7] | L1: STR WZR,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
[asl][www] Update `aslref-www` following herd#1611
… L.b Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
This change implements AARCH-23842 as published in the Arm Architecture Reference Manual for A-profile architecture: Known issues in Issue L.b. The purpose of this change is to make transliteration easier and it is not meant to change the intent of the architecture. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
There are cat clauses that expect that there is no intervening Effect in a specific relation. Add support for transliterating it with miaou7. For example: let rel = intervening(M, po & loc) will print latex that corresponds to the following text: There is a rel between E1 and E2 if all of the following apply: - E~1~ appears in program order before E~3~. - E~1~ and E~3~ are to the same Physical Address. - E~3~ is a Memory Effect. - E~3~ appears in program order before E~1~. - E~3~ and E~1~ are to the same Physical Address. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
…ps.cat This change implements AARCH-24622 as published in the Arm Architecture Reference Manual for A-profile architecture: Known issues in Issue L.b. The purpose of this change is to remove an ambiguity and simplify the transliteration of dependencies and pick-dependencies and it is not meant to change the intent of the architecture. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
This change implements AARCH-23849 as published in the Arm Architecture Reference Manual for A-profile architecture: Known issues in Issue L.b. This change replaces the relation of reads-from-register (rf-reg) with a new relation local register read successor (lrrs). Local register read successor builds on top of loc that applies between Register Effects to the same Register and po that applies between Effects that appear in program order. Local register read successor can be derived statically from the litmus test and without needing herd7 to compute the the reads from relation. Reads-from-register is used in dependencies and replacing it with local register read successor is not meant to change the behaviour of any tests that rely on dependecies that involve general purpose registers only. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Generalise the handling of the range() function. As a result, miaou7 can handle the use of range in bob: [range([(Exp & R & A)]; amo; [(Exp & W & L) | (FAULT & L)])]; po; [Exp & M | Imp & Tag & R | MMU & FAULT] which is transliterated to: All of the following apply: - One of the following applies: - E1 is an Explicit Memory Write Effect with Release semantics. - E1 is a Fault Effect with Release semantics. - E3 and E1 are generated by an atomic instruction. - E3 is an Explicit Memory Read Effect with Acquire semantics. - E1 appears in program order before E2. - One of the following applies: - E2 is an Explicit Memory Effect. - E2 is an Implicit Tag Memory Read Effect. - E2 is an MMU Fault Effect. and other uses of range() such as the one in TLBuncacheable-pred. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
…aarch64.cat This change implements AARCH-23766 and AARCH-24727 as published in the Arm Architecture Reference Manual for A-profile architecture: Known issues in Issue L.b. The relation "Same Location" which is meant to apply between two Effects that are either: - To the same physical address when the address translation for these two Effects has a valid output address, or - Share the same low-order bits when the translation for at least one of these Effects does not have a valid output address. This change is to facilitate the transliteration of Same Location and it not meant to change the intent of the architecture. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
This change implements AARCH-24571 as published in the Arm
Architecture Reference Manual for A-profile architecture: Known issues
in Issue L.b.
With FEAT_HAFDBS, in the case where one PE, P0, is configured with
hardware updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), but
another PE, P1, using the same translation tables is configured with
hardware updates of Dirty state disabled ((TCR_ELx.{HA, HD}={x, 0}),
the following scenario can occur:
* P1 has a copy of a writable-clean translation table entry cached in
a TLB.
* P0 performs a hardware update of Dirty state for that translation
table entry.
* A store is attempted on P1, and this hits the writable-clean
translation table entry cached in the TLB.
The architecture permits the store on P1 to generate a Permission
fault, because P1 has hardware updates of Dirty state disabled.
However, the formal memory model did not permit this outcome. The
changes below relax the memory model to permit this outcome, and
therefore match the rules described in section D8.5.2.1 "Hardware
management of the dirty state".
As a result the following test is architecturally forbidden:
AArch64 S.HU+dsb.sy+dsb.sy-isb
Variant=vmsa
TTHM=P0:HD
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
0:X1=x; 0:X3=y;
1:X1=x; 1:X3=y;
}
P0 | P1 ;
MOV W0,#1 | LDR W2,[X3] ;
STR W0,[X1] | DSB SY ;
DSB SY | ISB ;
MOV W2,#1 | MOV W0,#2 ;
STR W2,[X3] | STR W0,[X1] ;
exists (1:X2=1 /\ fault(P1,x))
In addition, in the case where a PE is configured with hardware
updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), the
architecture forbids the hardware update of Dirty state on the PE
until the associated store is known to be non-speculative and,
therefore, ahead of the address translation or the tag check of an
instruction earlier in program order. However, the formal memory
model allowed such an outcome to be observed. The changes below
strengthen the memory model to forbid this outcome, and therefore
match the rules described in section D8.5.2.1 "Hardware management of
the dirty state".
As a result, the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-ttd
TTHM=P1:HD
Variant=vmsa,fatal
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), valid:0);
pteval_t 0:X6=(oa:PA(y), valid:1); 0:X7=TTD(y);
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0); 0:X9=TTD(x);
1:X1=x; 1:X3=y;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STR X6,[X7] | L1: STR W0,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
and the following test is architecturally forbidden:
AArch64 S.HU+dmb.st+po-tag
TTHM=P1:HD
Variant=vmsa,fatal,mte,sync
{
[TTD(x)]=(oa:PA(x), dbm:1, db:0);
[TTD(y)]=(oa:PA(y), TaggedNormal);
0:X6=y:red; 0:X7=y:green;
pteval_t 0:X8=(oa:PA(x), dbm:1, db:0);
0:X9=TTD(x);
1:X1=x; 1:X3=y:red;
}
P0 | P1 ;
STR X8,[X9] | L0: LDR WZR,[X3] ;
DMB ST | MOV W0,#1 ;
STG X6,[X7] | L1: STR WZR,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
…b in aarch64.cat
This change implements AARCH-24643 as published in the Arm
Architecture Reference Manual for A-profile architecture: Known issues
in Issue L.b.
Feedback from the the Linux kernel indicated that the implementation
of qspinlock would benefit from stronger ordering guarantees for
mixed-size memory accesses. This proposal is updating to the
Explicit-hazard-ordered-before rule in order to strengthen the
ordering requirements of the architecture.
As a result of this change, the following two tests become forbidden:
AArch64 CoRR+amo.swph0h0-posh0a.w0+w0
Variant=mixed
{
uint32_t 0:X3; uint32_t 0:X2;
0:X0=x;
uint32_t 1:X1=0xccddeeff; 1:X0=x;
}
P0 | P1 ;
MOV W2,herd#42 | STR W1,[X0] ;
SWPH W2,W1,[X0] | ;
LDAR W3,[X0] | ;
exists (0:X1=0xeeff /\ 0:X3=42)
AArch64 CoRR+rmwh0h0-posh0a.w0+w0
Variant=mixed
{
uint32_t 0:X3; uint32_t 0:X2;
0:X0=x;
uint32_t 1:X1=0xccddeeff; 1:X0=x;
}
P0 | P1 ;
MOV W2,herd#42 | STR W1,[X0] ;
LDXRH W1,[X0] | ;
STXRH W4,W1,[X0] | ;
LDAR W3,[X0] | ;
exists (0:X1=0xeeff /\ 0:X3=42 /\ 0:X4=0)
Co-authored-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
… M.a Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
10 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.