(Open this as a separate page)
Isla is a symbolic execution engine for Sail. It executes instruction set architecture (ISA) specifications written in Sail, such as our ARMv8 model translated from ARM’s machine readable specification, or Sail RISC-V.
Isla-axiomatic then combines these specifications with axiomatic memory models written in a subset of the cat language used by the diy tool suite (and in particular the memory model simulation tool herd7), with an SMT solver like z3 (used by this web interface) or CVC4.
The test/model dropdown provides a list of the currently open tests and their memory models. When a new litmus test or memory model definition is opened it will appear in this dropdown menu.
The litmus file dropdown provides options for opening litmus files and creating new litmus files. It also provides access to a pre-existing library of tests.
The memory model dropdown allows choosing the memory model to be used.
The architecture dropdown allows switching between ARMv8 mode and RISC-V mode.
The run test button runs the current litmus test with the selected model, showing an execution graph in (12) if the test is allowed. If the test is forbidden (or allowed) this will be shown in (9).
Allows setting addition options. Currently instruction fetch reads can be ignored (although they should not be ignored when using the ESOP2020 ifetch model), and it allows filtering out irf edges from the initial state in the ESOP2020 ifetch tests, as they can clutter the graph.
Allows creating a link to a snapshot of the interface state.
The concurrency litmus test, which can be edited.
A log of test results and feedback.
This tab shows the assembled machine code for the litmus test.
The editable memory model specified in the cat language. See below for a description of this language.
A graph of the execution, generated by (5). Relations can be toggled on and off by via the relations dropdown. If there are multiple valid executions, they can be switched between using the arrows in the top right.
The default litmus file format is a TOML file with a specific format described below. The .litmus files as used by herd7 are also supported.
It starts with two key value pairs for the name of the test and the (symbolic) address variables used. The symbolic key must be present, although symbolic = [] can be used if there are no such addresses. Note that this web interface currently always allocates (at least) 4-byte aligned concrete addresses to these variables where the memory values pointed to by these addresses are always symbolic. Other key/value pairs at the top of the file header are optional. For example:
name = "MP"
symbolic = ["x", "y"]Next comes a sequence of threads, e.g.
[thread.0]
init = { X3 = "y", X1 = "x" }
code = """
MOV W0,#1
STR W0,[X1]
MOV W2,#1
STR W2,[X3]
"""These should be named [thread.0], [thread.1], [thread.2] etc, in increasing order. They each contain two key/value pairs, init and code. The init key describes the initial state of registers for that thread. The register can be any bitvector typed register specified in the underlying Sail model. In addtion some synonyms are allowed, so Xn and Wn can be used for the underlying Rn registers on ARM. Values can be symbolic addresses like "x" or "y", hexadecimal or decimal values e.g. X1 = "1" or X5 = "0x14000001", or labels in the assembly source e.g. X2 = "g:". Note that all values should be passed as quoted strings.
The code section contains assembly code for each thread as a string. TOML’s multiline string notation with triple-quotes is used to split this over multiple lines.
Lastly the [final] section contains information about the expected final state of each test.
[final]
assertion = "(and (= (register X0 1) 1) (= (register X2 1) 0))"The only mandatory key here is assertion. An expect key can also be used with a hint about whether the underlying SMT problem should be sat or unsat, but this is not currently used by the web interface.
The assertion is specified in a SMTLIB-like S-expression format, where the special (register <name> <thread>) form can be used to specify the final state of any register in the Sail model. The <thread> corresponds to the number n in the various [thread.n] sections.
The form (last_write_to <address>) can also be used to write assertions that talk about the last written value to an address, which is typically a symbolic address like "x" or "y".
The cat language is described in detail here as part of the herd7 documentation.
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:
expr ::= 0
| id
| expr? | expr^-1
| ~expr
| [expr]
| expr | expr
| expr ; expr | expr \ expr | expr & expr | expr * expr
| expr expr
| let id = expr in expr
| ( expr )
binding ::= id = expr
closure_binding ::= id = expr^+
| id = expr^*
id ::= [a-zA-Z_][0-9a-z_.-]*
def ::= let binding { and binding }
| let closure_binding
| include string
| show expr as id
| show id {, id }
| unshow id {, id }
| [ flag ] check expr [ as id ]
check ::= checkname | ~checkname
checkname ::= acyclic | irreflexive | empty