The addresses field declares virtual addresses. In non-translation tests where page_table_setup is not used, this is used for all addresses. It assigns addresses in a deterministic way using the architecture configuration, where address i in the list of addresses is defined as symbolic_addrs.base + (symbolic_addrs.stride * i).

Additional addresses are defined in the page_table_setup key, using the virtual, physical, and intermediate keywords. For example:

would define three virtual addresses x, y, and z; as well as two intermediate physical addresses ipa1 and ipa2; and two physical addresses pa1 and pa2. By default the addresses generated by each of these three lines are guaranteed to be disjoint, and aligned by symbolic_addrs.stride bytes from the architecture config. If it is required that the two addresses should not be disjoint, then they can be declared separately, for example the following will declare x and y, where both can have the same address. Note that they are not required to have the same address unless additional constraints are used.

Custom alignment requirements can be specified in the following way:

will require that pa1 and pa2 are disjoint and 4K aligned.

Constraints upon addresses can be specified using the assert keyword, for example

will require that the the two addresses in the previous example are the same. The grammar for these constraints is as follows:

Note that there is no operator precedence in the grammar, so all nested operators must be explicitly bracketed. This is both in the interests of simplicity, as well as ensuring that the address constraints remain as unambiguous as possible. The function identifiers in AtomicExp can be any primitive Sail operation known to Isla. These are the external functions specified in Sail type declarations, so using a definition such as the following from the Sail library

we could write a constraint like sign_extend(0xF, 64) == x in our address constraint assertions. The x[7 .. 0] notation can be used to slice bitvectors. As in Sail, ranges are inclusive, so in this example the lower 8 bits of x would be sliced.

Custom functions can be declared using the let keyword within page_table_setup, for example:

There are three ways to declare mappings in the page tables. These are the two mapping commands |-> and ?->, and the identity command. These commands are used in a mostly declarative way, so

declares a virtual address x and a physical address pa, and then creates page table entries to map x to pa. Note that we only said mostly declarative above - what actually happens is that the addresses are determined first using the address declarations and any constraints, then the mappings are created sequentially in the order they appear. The mapping declarations do not influence the choice of addresses in any way. It is important therefore to take care that these mapping declarations do not clobber each other in unexpected ways for certain choices of addresses.

The exact behaviour of the |-> operator depends on the types of the addresses (virtual, physical, or intermediate) used for each operand, as well as whether a stage 2 table is in scope. The second operand can also be invalid, which causes an invalid mapping to be created.

The |-> operator defines how the page table is set up in the initial state of the test. The ?-> operator declares how the mappings can change over the course of the test. For example, if we update our previous example to:

Then x is initially mapped to pa, but can become either invalid or be mapped to pa2 over the course of running the test.

Finally, we have the identity keyword, which is a shorthand way of creating identity mappings. The following shows for each type of address a use of the identity keyword, and the equivalent |-> operator usage on the next line.

Note the use of functions like va_to_ipa. These convert an address from one type to another without changing the bit representation. There are six such functions:

• va_to_ipa converts virtual to intermediate

• va_to_pa converts virtual to physical

• ipa_to_va converts intermediate to virtual

• ipa_to_pa converts intermediate to physical

• pa_to_ipa converts physical to intermediate

• pa_to_va converts physical to virtual

A mapping statement such as x |-> pa will create many descriptors in multiple tables in order to set up the overall mapping from x to pa (these will be the addresses walked by the translation table walk code). For some test descriptions it is useful to be able to access these addresses. We can use the as keyword to give the sequence of addresses used by a mapping command a name. For example:

We can then use the functions pteN where N is a number between zero and three, and tableN where N is a number between one and three. In ARMv8 pteN is equal to tableN plus the offset at that level given by the virtual address. For cases with both stage 1 and stage 2 translations, there are functions s2pteN and s2tableN which can be used to access addresses used in the stage 2 translations. These functions return a physical address.

The initial values of memory locations can be set within the page table setup description. For example:

Here the address x will be translated to the correct physical address using the initial page table setup.

By default, we create both stage 1 and stage 2 page tables, with the address of each table being determined by the architecture configuration, in the [mmu] section. For example, for ARM we have:

This declares the base address and default page size for the stage 1 and stage 2 tables. It also defines some default setup code which is prepended to the page_table_setup for each test using this configuration.

The default page table setup above may not be suitable for all tests. In these cases we can disable the use of default tables by using the option keyword, and setting the default_tables option to false.

With the default tables turned off, we can declare our own tables using the s1table and s2table commands. These commands take the name of the page table to be created, and its base address in memory as arguments. They also introduce an optional scope which can contain mapping commands. Each of the mapping commands |->, ?->, and identity will use the closest enclosing tables in scope. The following shows an example of how this works:

The first x |-> invalid mapping will be created in hyp_pgtable_new as a level 3 mapping, while the second will be created in hyp_pgtable as a level 2 mapping. The use of at level <n> is also new in this example, which allows creating mappings at a specific level in the page tables (the default for ARM would be level 3).

We also use ?-> table(table3(walk)) to tell the ?-> mapping command that table3(walk) is the physical address of a table, so it needs to create a table descriptor rather than a regular descriptor.

The third new feature seen in this example is the with code following the identity 0x1000 command. The with keyword is used to control the attributes used for the descriptors created by the mapping command. In this test 0x1000 is used for the address of an exception handler, so we need to ensure this memory is mapped with permissions suitable for executable code.

Finally we see that s1table hyp_pgtable_new appears nested within the s1table hyp_pgtable scope. Nesting table commands causes the tables to be mapped into each other. In this example, hyp_pgtable_new will be mapped into hyp_pgtable. If we wanted, we could insert more mappings into hyp_pgtable_new here, for example:

By default each table is mapped into itself. To disable this, use:

each table can then be mapped into itself explicitly as follows:

Above we saw the use of with code to create a mapping with code permissions. We can also set custom mappings, for example:

If a mapping command can create both stage 1 and stage 2 descriptors, we can write with <stage 1 attributes> and <stage 2 attributes> to set the attributes for each type of descriptor separately. This is often required as stage 1 and stage 2 tables have different sets of descriptor attributes, so the attributes used by one will be invalid for the other. For example:

Like how code is intended as a sensible default for mapping memory used for code, default represents sensible defaults for memory used for regular data.

The attributes supported by Isla for AArch64 are described in the ARM architecture reference manual. For stage 1 they are:

• UXN

• PXN

• Contiguous

• nG

• AF

• SH

• AP

• NS

• AttrIndx

And for stage 2 they are:

• XN

• Contiguous

• AF

• SH

• S2AP

• MemAttr

In the case where setting the attributes isn’t quite enough, and we need absoutely full control over the format of the descriptor, we can use the raw function to tell the mapping commands to treat it’s second argument as a raw descriptor value and not an address. For example:

Creating raw descriptors with virtual addresses will place them in the stage 1 table, whereas using intermediate physical addresses will cause them to be created in the stage 2 table. Parent descriptors at lower levels will still be created as usual.

There are two main options that affect how Isla generates candidate executions of translation tests, both of which are in some sense optimizations as they can make tests run considerably faster (by potentially several orders of magnitude). However neither are fully automatic, and require models to be written in specific ways to take full advantage.

• --merge-translations Causes all the translation table reads for each walk to be merged into a single event. This has the following consequences:

  • Each translate event can have multiple trf edges

  • No translate events are marked as either Stage1 or Stage2 (because all of them are merged together)

  • To work around the lack of explicit Stage1 and Stage2 sets, this information is encoded into the edges, as via trf1 and trf2 relations, such that trf; [Stage1 & T] = trf1 in the unmerged case.

  • After merging translations we can’t distinguish between the order of translate writes by via trfN; iio; [T]; trfM^-1 where N, M in {1, 2}, so we introduce ternary relations between pairs of writes and translate events that capture this.

• --merge-split-stages Modifes --merge-translations to generate two events for each walk, one for all the Stage1 and another for the Stage2 reads. This option shares the same consequences as the previous, except that we preserve the Stage1 and Stage2 event sets, so it tends to work for models written for unmerged translate events better, however models can still be made unsound depending on how they use trf; iio; [T]; trf^-1.

• --remove-uninteresting removes 'uninteresting' events. There are two variants safe and all. An uninteresting translate event is defined as one that can only read from the initial state (i.e. there are no possible writes to that descriptor). The all option removes every such translate event, whereas the safe option removes all such events, provided they do not occur within the same walk as any interesting translate read.

  • The all variant is quite dangerous as it can affect things like rules for TLBI invalidation in the model.

  • Experimentally the safe option seems to work well, although it is possible to create counter-examples with our current models. Currently, they derive on edges from ERET events to translates, then from translates to other non-translate events. If the model was changed to derive the edges from ERET to non-translate events directly without going through uninteresting translate events then this would likely dissappear. This is just an example, any similar situation where edges are derived via any translate will cause this type of issue.

The web interface can be used to run virtual memory tests. Enabling the page table setup, and toggling the various optimisations above is done via the options menu:

The Use ARMv8 page tables checkbox is equivalent to the --armv8-page-tables flag on the command line. For running virtual memory tests, the AArch64 VMSA model should be selected in Sail architecture menu:

A suitable model is included in the memory model menu. The above options will be set automatically when choosing a sample virtual memory test using the litmus file menu, using the AArch64 VMSA examples.

Isla supports an option --extra-smt that can be used to check additional properties that are hard to express in the cat format used for the memory model. In the context of virtual memory tests, this can be used to detect things like break before make (BBM) violations in tests. In this subsection, we will show how this can be done to detect at least some such potential violations. Note that this section is mainly intended to demonstrate how this can be done, rather than perfectly describe possible break-before-make violations.

When changing an existing translation mapping, from one valid entry to another valid entry, Arm require in many cases the use of a break-before-make (BBM) sequence: breaking the old mapping with a write of an invalid entry, a DSB to ensure that is visible across the system, and a broadcast TLBI with additional synchronisation to invalidate any cached entries for all threads, then making the new mapping with a write of the new entry, and additional synchronisation to ensure that it is visible to translations (specifically, to translation-walk non-TLB reads). If this sequence is not used then any number of undesirable consequences may occur.

We start by identifying the events that write a level 3 descriptor and it’s parents (some details omitted for brevity).

We then create constants for the two conflicting writes to a page table entry BBM_W1 and BBM_W2:

We can then define the sequence of events between BBM_W1 and BBM_W2 that would constitute a correct break-before-make sequence, namely writing an invalid entry to `BBM_W1’s descriptor or any parent descriptor, followed by a suitable TLBI. We then assert that there is no such sequence — meaning a satisfiable model is an example of a potential break before make failure.