isla-axiomatic

The --view flag will cause the output to be displayed as a graphviz generated graph using xdg-open to open an image viewer. The flag --dot <path> will instead generate the dot files used by graphviz in the directory specified by <path>. The --temp-dot flag will generate the dot files in either the default system temporary files directory (typically /tmp on Linux) or in TMPDIR if the environment variable is set. --view implies --temp-dot unless --dot is used.

If we append --dot . to our command in the previous section it will generate a file MP_1.dot in the current directory (if the test had multiple allowed executions, they would be MP_2.dot and so on). We can then use the dot command from graphviz to generate an image, like so:

This will generate the following picture:

The --refs flag will take a set of reference results produced by Litmus, Herd, or RMEM, and compare the output with the contents of that file.

The --ifetch flag generates additional events for our ARMv8 instruction fetch model. This option primarily changes the base set of relations and sets available to the Cat memory model. Roughly speaking, it causes instruction fetch (ifetch) events to be ordered by fetch-program-order (fpo) and non-ifetch events to be ordered by regular program order (po). ifetch events are related to regular events by the (fetch-to-execute) fe relation. The ifetch events will be in the set IF. Additionally there is a weak-coherence-order (wco) in addition to the normal coherence order, and an instruction-reads-from (irf) in addition to reads-from.

The --armv8-page-tables flag causes page tables to be created. See isla-axiomatic for full details of support for virtual memory and address translation for AArch64.

Next the test contains the data for each thread. There is a thread.N section for each thread numbered starting from thread.0. The code key contains the code for each thread - isla-axiomatic does not parse this code however, and it is directly passed to an assembler. For each thread N its code will be compiled into an ELF section called litmus_N. Where that section is located is determined by the [threads] section of the architecture configuration file:

It contains the base address for loading the code for each thread in a litmus test, and a stride which is the distance between each thread in bytes. The overall range for thread memory is the half-open range [base,top). Each thread is therefore located at threads.base + (threads.stride * N).

The initial state of registers can be set using the init key for each thread via a table of register = value pairs. The register names must correspond to the register names used in the Sail model (which may differ to those used by the assembler!). For example, in ARM assembly the general purpose registers are called X0 to X30 for their full 64-bit values, and W0 to W30 for their lower 32-bits. In the Sail model, these registers are represented using registers called R0 to R30. To facilitate using the assembler names, there is a [registers.renames] section in the configuration which allows for synonyms to underlying Sail model registers.

An important thing about the init section is it sets the register values at the beginning of time before any Sail code has been (symbolically-)executed by the tool. However, this can be problematic, as often the top-level of a Sail ISA specification looks something like:

Here each register in the init key will be set before main() is run. What happens if setup() initialises some registers to architecturally-defined values? isla allows initialising registers at an arbitrary user-defined point in time, using the reset_registers builtin. This would be set up in our example model as such:

We can now use the reset key in our thread sections, much like the init key, and the registers will be set when isla_reset_registers() is called.

The register keys in the reset table are actually slightly more general than in init and support setting individual subfields of a larger Sail register, as is shown above for PSTATE.

The last section of the file, [final] contains the assertion that the test must satisfy. We can either expect this assertion to be satisfiable (sat) or unsatisfiable (unsat). The assertion is written using a small assertion language, specified by the grammar:

The operators &, |, and ~ must be parenthesised to remove ambiguity. There are no implicit precedence rules to ensure clarity. The address terminal can be one of the addresses specified by the symbolic key at the start of the file, and register must be a Sail register name.

The file format also supports custom ELF sections in the generated litmus test binary, these are specified using a section like so:

The section is called [section.NAME] where name will the the name of the section in the ELF. There is a check to ensure this does not clash with any of the the generated thread sections. It will be assembled at the specified address in the generated ELF.

To constraint the non-determinism for self-modifying code, we must declare which addresses in the thread’s code can be modified and how, using the self_modify toml array:

Note that the address is a label from the code, which is shown below:

As can be seen, such labels can also be used as the initial value for registers, like X1 above.

Constrained addresses work like the self_modify sections, but allow restricting the values that are allowed at an address declared in a litmus file. For example:

Here we have three addresses x, y, and z. The initial value at x is the address of z. The constrained section says the 8-bytes at this address can only contain the values of y or z. This constrains the symbolic execution for all the threads, so we don’t get a blow-up in the number of traces when we use a value read from memory as an address in one thread.

Herd has its own custom format for litmus files. To facilitate working with these files, we include a tool in the github repository isla-litmus which can convert from Herd’s .litmus format into the TOML format described above. This tool is written in OCaml, as it uses the parser from Herd itself.

The memory model language used by isla-axiomatic is based on the cat language used by Herd

The basic relational operators are mostly the same as in cat: We have | for union, ; for relational composition, & for intersection, \\ for difference, and * for the cartesian product.

Documentation on the full cat language can be found at: http://diy.inria.fr/doc/herd.html#herd%3Alanguage

The postfix operators are ^+, ^*, and ^-1 for transitive closure, reflexive-transitive closure, and the inverse of a relation. As in cat, R? is the union of the relation R and the identity relation.

Much like in cat the [S] operator will lift a set S to the identity relation over S.

We support arbitrary N-ary relations, and the various operators are defined to work on N-ary relations (and sets) where appropriate.

As an example, see the dependency-ordered-before (dob) relation in the Arm model:

Cat has some features which are not easy (or even possible at all) to translate into SMT. Roughly-speaking, we support the fragment of cat that defines sets and relations over events. More formally the fragment of cat we support is defined by the grammar:

Values can be extracted from the Sail model by using accessors. The possible outcomes/events of the model are declared in the Sail library (in lib/concurrency_interface) of the Sail model. As an example, the outcome declaration for a barrier looks like:

The idea here is that the outcome declarations are part of the Sail library, and therefore shared between the various ISA models, but the type variables such as 'barrier above can be instantiated with architecture-specific types in each ISA model.

By default, each event in the execution graph corresponds to a single event generated by the Sail model (as described by the outcomes in the interface). So a single memory access becomes a unique node in the graph, as does each fence, system register access (when selected for inclusion in the graph), and so on. This has two main issues:

A example of this is in models for address translation. Generating a separate event for every read in a translation table walk quickly explodes, as (in Arm) there can be up to 24 page table memory accesses for every regular memory access.

Isla allows avoiding this by creating graph events that correspond to a sequence of many trace events, while still allowing us to access the data from those events if required. We do this by creating an index type that allows us to map into the sequence of trace events, for example:

This declares a natural number T, such that the type bits(T) can be used to index the underlying trace events making up a single axiomatic event. Isla will automatically pick the smallest value possible for this index.

This number can be used when declaring indexed accessors. For the rest of this section we will assume that we are working with translation events that contain a sequence of memory read events. Let’s assume these memory read events contain a translation field, which in turn contains a struct with various information about the state of the page table walk where they were issued. Here we assume that there is a stage field telling us if an access is in the stage 1 or stage 2 tables:

Assume we have a graph that looks something like:

Here we have a translation event (in set Tr), a memory write (W), and a stage 1 TLB invalidate (TLBI-S1). We define a i-indexed relation tlbi-affects that relates TLBI events to Tr events if the trace sub-event i shares the same stage with the TLB invalidate. We assume also that the built-in relation trf (translation reads-from) is defined similarly.

Now we want to define the write-before-tlbi relation in red. How can we do this? We can use a where exists clause to combine a standard cat-style relational definition using let, with an additional constraint that the trf index must be less than the tlbi-affects index. Since the indices are bitvectors, we can use the SMT function bvult (bitvector unsigned less than) for this.

The axiomatic concurrency models depend on syntactic dependencies between instructions. In a perfect world this information would be provided to us explicitly as part of the architecture specification, but as large imperative ISA specifications have not typically been integrated with concurrency tools such as Isla, this is not the case in the real world at present.

The dependency relations we need are:

We have a way to derive sensible syntactic dependencies from the semantics of instructions. This may seem odd - how can one derive syntactic dependencies from semantics? The assumption here is that the syntax itself should determine all the possible behaviours, so if we use symbolic execution to explore all the possible behaviours of an instruction in any starting state, we should end up with the correct syntactic dependencies.

The approach is roughly as follows: for each instruction in the litmus test we execute it in an unconstrained starting state. This produces a set of all the possible behaviours of the instruction. We then look at those behaviours and track which registers were tainted by data read from memory, as well as what registers flow into store, load, and branch addresses. Using this information we can then compute the addr, data, and ctrl relations in a straightforward way.

The isla-footprint command with the -d(--dependency) option can be used to view the information generated by this process:

generates:

Some registers in the Sail ARM model aren’t really architectural registers and should be ignored for dependency analysis, these can be added to registers.ignore in the architecture configuration. Usually in ASL and therefore the ARMv8 Sail, these are prefixed by two underscores.

Unfortunately it is sometimes possible that this process doesn’t give us exactly the dependencies we need. There are two special builtins

That allows annotating registers with information (in the form of a string) at specific points during symbolic execution, for example:

will cause read-write edges from R0 to R1 to be ignored, "ignore_write" can also be used with a single register to ignore all read-write edges into a register.

While the notions of address, data, and control dependencies seem simple enough for user-mode concurrency, things become more unclear when we start thinking about systems features. For example: What if an instruction behaviour changes between exception levels? Should we included dependency information generated at all exception levels? Does dependency information cross between exception level boundaries? How does the MMU and address translation affect this?

In truth it seems syntactic dependencies are bit of a fuzzy concept once we start thinking at this level. In practice when we have the MMU enabled we can make instruction execution so non-deterministic that it becomes computationally infeasible to evaluate all paths through an instruction without abstracting away features. To work around these issues in systems tests, we have a --footprint-config option for isla-axiomatic that allows a separate architecture configuration to be used during dependency analysis.

For each litmus test the configuration for the in-memory page tables are specified using the page_table_setup key of the toml litmus test format. For example, the following is the beginning of a particularly simple virtual memory litmus test that contains a single virtual address x, which is mapped to some physical address x.

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:

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.

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:

And for stage 2 they are:

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.

Unlike for regular litmus tests, where the initial state for each thread usually does not go far beyond setting some general purpose registers, in systems litmus tests like the virtual memory tests, each thread may need to configure more registers in the model. To explain how this works, it is helpful to understand the initialisation flow in the Sail ARM model (and most other Sail models) that occurs for each thread in the litmus test. This is shown in the diagram below:

Blocks highlighted in yellow correspond to Sail primitive operations implemented in Isla. The first step is to call a Sail function, TakeReset in ARM, that defines programmatically how the model should initialised, ensuring any global invariants are set up correctly. The program counter _PC is then set to the entry point for the thread (using the same Sail primitives we use for loading ELF test files). Next, a special primitive reset_registers is called which sets registers based on values found in the litmus test file. Finally we tell Isla that the main fetch-execute-decode loop is starting by calling cycle_count for the first time.

The TOML litmus test format we use allows setting registers at two separate points in time.

Setting registers via the reset_registers primitive is more useful in general, so most of our virtual memory tests do this exclusively. The situation where we would need to set registers prior to TakeReset is if those registers are themselves used during TakeReset. Some registers in the ARM model are exclusively used in this way to configure the model via changing the behavior of TakeReset.

To assign registers during the reset_registers builtin we use the thread.N.reset key for each thread N. Below is an example from one of our tests:

Other that when it occurs, the main distinction between setting registers in a thread.N.reset section versus a thread.N.init section is that the reset section has access to the (symbolic) model state (whereas the init section is used to create this state in the first place). Having access to the model state has two main upsides:

Various functions can be used in the reset section to help constructing values for virtual memory tests. These are as follows:

To enable running tests with virtual memory we need to pass the --armv8-page-tables option to Isla. This will cause Isla to use the page_table_setup to create page tables suitable for AArch64. The other aspects of initializing the model to run virtual memory tests are handled via the usual configuration file passed via the -C/--config option. For running AArch64 virtual memory tests we provide the configuration file aarch64_mmu_on.toml in the configs subdirectory of the Isla repository.

Computing instruction footprints with address translation turned on is impracticle to the point of being impossible in any reasonable length of time, so a separate config can be provided for instruction footprint analysis using the --footprint-config option. For this, the standard aarch64.toml configuration file suffices.

Figuring out how to get Isla to run some tests can be tricky, as the architectural state relevant for systems features such as address translation and virtual memory can be large and complex. This section aims to contain some useful tips that can help when writing these tests.