[herd,litmus] Initial support for translating addresses of instructions

[artkhyzha]

This PR adds basic support for address translation for instruction fetch into herd7 and litmus7.

The syntax of litmus tests is extended with:

• a new annotation .pagealign that aligns the next instruction to the new page and inserts an immediate branch to that instruction;
• ability to specify a TTD of a label, so that we could write TTD(P0:Page0)=... where Page0 is a label on P0;
• ability to specify an MMU fault as either coming from the data side (D-MMU) or the instruction side (I-MMU).

Functionality-wise, semantics of instruction fetch is reworked to benefit from the pre-existing support for address translation. Prior to the instruction fetch, the address of the instruction is translated, and a possibility of the address having been remapped onto a different page is considered.

---

Ideas for future work.

UI-wise, recommended, but not urgent:

• Currently herd hides register effects from graphs by default. This at times may result in "iico_ctrl" edges seemingly disappearing. With -variant ifetch, iico_ctrl edges may need to be displayed without '-showevents all'.
• Printing of the instruction should be omitted from boxes until after the Branching effect for ifetch

Refactoring-wise, optional and just for consideration:

• loader.ml now makes use of a pseudoinstruction Skip <imm> denoting the offset of a padding until the next page. To make use of it, the Loader module does yet another transformation of the internal data structure for a litmus test. Wasted transformations aside, it would be an improvement to maintainability if the organisation of the transformations was clearer.
• semExtra.ml implements checks for the purposes of mixed-size mode, which are then used by mem.ml during the rf construction. One of such checks interacted with the way offsets are created for instruction addresses. That interaction received "duct-tape" treatment (a special case got added) and is marked as "FIXME". Ideally, offsets for instruction addresses would pass the usual mixed-size checks.
• support for labels as VAs resulted into the following: the name of a symbolic constant, when it corresponds to a VA, is of a type "Constant.Symbol", while the name of a symbolic constant, when it corresponds to a PA, is of a type "string". This mismatch results in odd-looking pattern matches. See this comment.

[murzinv]

JFYI, #1507 also relies on [all] Turn labels into regular symbols. Given amount of merge conflict it generates when rebased would it make sense to merge it independently?

[artkhyzha]

That's good idea, @murzinv . It seems that this commit passes make test.self and make ifetch-test. With that, indeed we could merge it independently and ASAP.

UPD. I suppose some extra care could be taken to check if litmus7 has any regressions with -variant self.

[murzinv]

Just few nitpicks I noticed while trying to add support in litmus7

[murzinv]

Nitpick: can we please use W registers (here and in other tests) so litmus7 won't complain about different types for register

Register x0 has different types: <int> and <int64_t>

[murzinv]

Isn't test name A007?

[murzinv]

Isn't test name A009?

[murzinv]

Isn't test name A010?

[murzinv]

Isn't test name A011?

[murzinv]

JFYI, litmus7 support master...murzinv:herdtools7:litmus-vmsa-for-ifetch
Example output

$ qemu-system-aarch64 ACCEL=tcg sh t/run.sh
Thu Nov 20 03:23:16 PM GMT 2025
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for herd/tests/instructions/AArch64.vmsa+ifetch/A008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 A008

{
 [PTE(0:Page0)]=(oa:PA(0:Page0), af:0);
}
 P0           ;
 Page0:       ;
 ADD X0,X0,#1 ;

forall (fault(P0:Page0,MMU:AccessFlag))
Generated assembler
#START _litmus_P0
	mov wzr,#0
	.align 12
1:
	add x0,x0,#1
	.align 12
	mov wzr,#0
qemu-system-aarch64 -nodefaults -machine virt -accel tcg -cpu max -device virtio-serial-device -device virtconsole,chardev=ctd -chardev testdev,id=ctd -device pci-testdev -display none -serial stdio -kernel t/./A008.flat -smp 1 -append -q # -initrd /tmp/tmp.WWhV6aFlOb
Test A008 Required
Histogram (1 states)
100   :> fault(P0:Page0,MMU:AccessFlag);
Ok

Witnesses
Positive: 100, Negative: 0
Condition forall (fault(P0:Page0,MMU:AccessFlag)) is validated
Hash=f1e020a2294bce0d3da8aca86232ae83
Variant=vmsa,ifetch
Observation A008 Always 100 0
Faults A008 100 P0:100
Time A008 0.06

EXIT: STATUS=1
Revision 8110380663bad54dc1445500a3520c25b3a0ccd3, version 7.58+1
Command line: litmus7 -o /kvm-unit-tests/t -mach kvm-armv8.1 -variant vmsa,self herd/tests/instructions/AArch64.vmsa+ifetch/A008.litmus -mode kvm -a 1 -s 10 -r 10
Parameters
#define SIZE_OF_TEST 10
#define NUMBER_OF_RUN 10
#define AVAIL 1
/* gcc options: -Wall -std=gnu99 -std=gnu99 -ffreestanding -I $(SRCDIR)/lib -I $(SRCDIR)/libfdt -Wall -Werror  -fomit-frame-pointer -Wno-frame-address   -fno-pic  -no-pie -Wmissing-parameter-type -Wold-style-declaration -Woverride-init -O2 $(call optional-ccopt, -mno-outline-atomics) -march=armv8.1-a */
/* barrier: userfence */
/* alloc: static */
/* proc used: 1 */
LITMUSOPTS=
Thu Nov 20 03:23:16 PM GMT 2025

[diaolo01]

Checking understanding: needs_vmsa_for_ifetch might be needed when the PTE fields change, while needs_ifetch is needed for labels that would enable changing the instruction at an address?

[diaolo01]

If this is future work, can it be added in the PR description similar to the other items?

[artkhyzha]

Fair. With a bit of thinking, I wonder if the PAs could use Symbols instead of strings too. That would make the interface here a bit clearer. However, it's not necessary for the functionality of this PR, so I am tempted to leave it as a FIXME.

Specifically, right now we have:

In mem.ml:

let solve_mem_non_mixed test es rfm cns kont res =
  ...
  | Some (V.Val (Symbolic (Physical (s,_)))) when (s |> Symbol.of_string |> Symbol.is_label) -> true
  ...

In semExtra.ml:

let is_non_mixed_symbol test =
  ...
  | Physical (s,_) when (s |> Symbol.of_string |> Symbol.is_label) -> true
  ...

In constant.ml:

let is_non_mixed_symbol = function
  | Physical (s,_) when (s |> Symbol.of_string |> Symbol.is_label)
  ...

In all of these cases, I am slightly surprised by how I need to analyse the string to understand if it is a label. This is in constract to VAs, where I just look at the type of the name. The need to provide logic for PAs of labels will likely remain, but perhaps the interface for checking if a constant is a PA of a label could become simpler by letting the type of PA's symbol be Constant.Symbol rather than a string.

[diaolo01]

Thanks @artkhyzha, great work. I have reviewed this PR in detail with the exception of loader.ml where I am not familiar with the code. I have ran the tests and checked the PR by adding my own work on top, making sure that things are correct. No unexpected surprises, only some minor suggestions.

[diaolo01]

@relokin @fsestini One of the commits of this PR, [herd] Modify tests to match new fault syntax, is concerned with modifying the output of some of the existing tests that have generic faults in their postcondition. This does not impact the hash of the test. This is required as a result of the introduction of D-MMU and I-MMU to differentiate between faults on the data vs instruction side. Can you please comment on whether this is an acceptable solution?

Another issue I'd like your opinion on is excluding the new execute bit in the PTE from the computation of the hash. This required as, by default, we have agreed x=1 means executable, which would change the hash of already existing tests that have PTE. Currently, I have removed the bit from the hash computation, but I am not comfortable with that. I saw that attrs and el0 are also excluded from the computation, but it was not clear to me why. A solution that would get rid of this problem and allow us to introduce the executable bit in the computation is to embed the bit with reverse polarity. It would still mean executable by default, but there would be xn=0 in the default, which I understand would not affect the hash. This would also be more closely aligned with the architecture, so I have a personal preference for this solution. What do you think?

[relokin]

Thanks for this Artem. A couple of thoughts:

• I think you can squash my commits into one, they don't stand on their own.
• You would have to squash the last commit into the relevant commits as well.
• This commit "Modify tests to match new fault syntax" should be squash with the commit that introduces the new syntax.

Overall, we should ensure that we can pass the regressions with every commit.

I am a little on the fence about D-MMU and I-MMU have we discussed and agreed on this syntax? In existing tests that we use MMU that implies D-MMU?

For litmus7 can we please check that we can run all catalogues in vmsa+ifetch mode?

Finally, variant=vmsa,ifetch now enables translation for data and for instructions. Do we see the need to have a mode where we have ifetch and translation only for data? Does this even make sense to support?

[relokin]

I am not entirely sure about this change. We can go with this for now, but there are two alternatives:

• Just like we count NOPs we could have counted .pagealign as the adding the corresponding number of NOPs.
• A better alternative in my opinion would be to not rely on NOP for markers at all, what can't litmus7 emits internal labels instead of counting NOPs?

Perhaps we can leave a note with a TODO here. Or otherwise something for @diaolo01's backlog.

[relokin]

@relokin @fsestini One of the commits of this PR, [herd] Modify tests to match new fault syntax, is concerned with modifying the output of some of the existing tests that have generic faults in their postcondition. This does not impact the hash of the test. This is required as a result of the introduction of D-MMU and I-MMU to differentiate between faults on the data vs instruction side. Can you please comment on whether this is an acceptable solution?

I think it's perfectly fine to change .expected files.

Another issue I'd like your opinion on is excluding the new execute bit in the PTE from the computation of the hash. This required as, by default, we have agreed x=1 means executable, which would change the hash of already existing tests that have PTE. Currently, I have removed the bit from the hash computation, but I am not comfortable with that. I saw that attrs and el0 are also excluded from the computation, but it was not clear to me why. A solution that would get rid of this problem and allow us to introduce the executable bit in the computation is to embed the bit with reverse polarity. It would still mean executable by default, but there would be xn=0 in the default, which I understand would not affect the hash. This would also be more closely aligned with the architecture, so I have a personal preference for this solution. What do you think?

Very good question and I am glad we are not brushing over this! Could we ignore the x bit for the purposes of computing the hash only when it has it's default value? Meaning if x=1, it is not used in the hash calculation, otherwise if x=0 we include it?

It would be great if @maranget could have a look at this question as well.

[artkhyzha]

As a status update and an interim response to @relokin's feedback (thanks!):

I am a little on the fence about D-MMU and I-MMU have we discussed and agreed on this syntax? In existing tests that we use MMU that implies D-MMU?

The current idea is to let MMU = D-MMU | I-MMU. With this approach, already written tests with Data Aborts do not need updating even though their faults would now become D-MMU faults. Outputs of herd7 change, which is relevant for unit tests, but the tests in the catalogue and their verdicts remain the same. This seems like a good tradeoff, assuming we want to keep backwards compatibility and support the term MMU in dozens of already written tests and published materials, but also for it to mean D-MMU.

There is an open question whether D-MMU and I-MMU are our preferred terms. The names may get updated based on feedback.

For litmus7 can we please check that we can run all catalogues in vmsa+ifetch mode?

Thank you for this suggestion. This is revealing some issues that will be investigated.

Finally, variant=vmsa,ifetch now enables translation for data and for instructions. Do we see the need to have a mode where we have ifetch and translation only for data? Does this even make sense to support?

I agree that turning on/off translation for data accesses and/or instruction fetches could be helpful. This functionality is more about user interface, I think, and it strikes me as an "expert" feature that could be not enabled by default. We could support variants NoTrForData and NoTrForInstr (or something with less cryptic names) to disable address translation for certain accesses. By default, these variants would not be enabled.

That said, I wonder if this idea is okay to implement separately, in a follow-up PR.

[artkhyzha]

For litmus7 can we please check that we can run all catalogues in vmsa+ifetch mode?

@relokin, thank you again for this suggestion. It has revealed some issues that were investigated:

• Many litmus tests from the VMSA catalogue used to crash, which is now fixed. Thanks to @diaolo01!
• Some of the tests from the VMSA catalogue keep crashing -- due to temporary limitations. For instance, consider Luc00.litmus. Litmus tests that runs a certain PE from EL0 are not yet supported.
• Litmus tests with SVC need extra engineering effort; as this is orthogonal to the current PR, the work on this has been moved to [litmus] Introduce ExS, EIS and EOS variants #1716.
• Litmus tests from the ifetch catalogue have several tests that "cannot be compiled". This is not a regression: the behaviour is the same on master with -variant self and -variant self -mode kvm. My suggestion is to consider the problem orthogonal and investigate it separately.

Overall, the open question is whether we would like to allow running PEs from EL0 and EL1 simultaneously. We do not currently expect to run litmus tests that execute from the same address both in EL0 and EL1, but in principle we could want to run litmus tests where some PEs are EL0 and others are EL1.

One of the questions that comes up is the meaning of the "x" bit in TTD tuples: does it correspond to PXN or UXN? To which point the suggestion could be that both of them get set with identical values.

Are there any other potential conceptual issues with mixing EL0 and EL1 in vmsa+ifetch tests? Do we consider this a blocking issue, or could it be left as future work?

[diaolo01]

Very good question and I am glad we are not brushing over this! Could we ignore the x bit for the purposes of computing the hash only when it has it's default value? Meaning if x=1, it is not used in the hash calculation, otherwise if x=0 we include it?

I've checked the behaviour I'd introduced and it already omits x when it is default (x=1) and includes it when it's different (x=0). No further action required on this.

[fsestini]

Thanks @artkhyzha . I’m not too familiar with the VMSA/ifetch specifics, but the changes look good from my side.

I left a few inline comments. They’re mostly general OCaml/style notes rather than feature concerns.

One additional follow-up idea (not for this PR): pseudo.ml publicly exposes constructors like Macro and Skip that are treated as “illegal” in several places (via assert false, like, say gen/top_gen.ml:044). That "contract" isn’t explicit from the public Pseudo.S signature alone, even though lib and pseudo.ml are shared across the repo. It might be worth a follow‑up refactor to split pseudo into more specific types or to hide those constructors behind narrower interfaces, so the API and types better reflect what’s actually supported. I appreciate this PR is building on existing structures, but since the pseudo type is being touched here I thought I’d mention it as something to keep in mind.

[fsestini]

Not a big deal in this particular case since mmu_t is a small variant, but as a general rule I try to avoid polymorphic equality (=) on custom datatypes since it’s a bit fragile if the type ever grows to include non-comparable data. Perhaps using an explicit let mmu_t_equal = (=) could keep the intent clear.

[artkhyzha]

Interesting. Does the same concern apply to the FaultType.t itself? Would it be a good practice to have equal : t -> t -> bool in its interface?

[fsestini]

It would apply to FaultType.t as well, yes, especially considering FaultType already exposes a compare function.

In general I would consider good practice for any module M exposing any type t that is intended to be compared for equality to also expose an explicit equality predicate.

[artkhyzha]

Thank you, @fsestini, for the comments -- I have tried to address them, so the PR should be up to date.

[relokin]

Thanks everyone for your efforts on this.

@artkhyzha feel free to merge when you are ready.