Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA

Below are links to web interfaces for the ARM Flowing and POP models as described in the paper. The models are written in Lem and exported to OCaml by the Lem tool. The OCaml models together with some OCaml code, to derive the user interface, are compiled to OCaml bytecode and then, using the js_of_ocaml compiler, compiled to JavaScript. This allows the tool to run in the browser on the client side.

To use the web interface click on the Flowing or POP link. The interface has two main pages, the configuration page where litmus test and options are selected and the run page where the selected test is run interactively.

Configuration Page:

• Litmus test (edit box in the centre): the litmus test to run on. A library of tests is provided with the tool and can be accessed from the Select ARM Test button.
• Interactive button: after a litmus test was selected clicking this button will start the tool.
• Select ARM Test button: open a dialog that lets you select a litmus test from the library provided with the tool.
• Select Options button: open a dialog that lets you chose some run options.
• Select Topology button (Flowing only): open a dialog that lets you chose the topology of the storage subsystem.

• System State: this box displays the current state of each subsystem of the model (storage subsystem at the top, followed by thread subsystem for each thread in the test) and lets you chose the next transition of the model (green text). To allow better tracking of changes after each transition, the interface will colour in red things that were just added and in grey things that were removed. The state of each thread includes for each fetched instruction the state of the sail interpreter (blue).
• Undo button: undo the last transition
• Reset button: return to the configuration page

Guided Example 1 (Flowing with default options) we will guide you, step by step, through the execution of the MP+dmb.sy+addr litmus test with default configuration.

• Go to the Flowing web interface by clicking on the Flowing link above
• Open the MP+dmb.sy+addr litmus test by clicking the Select ARM Test button and then selecting MP+dmb.sy+addr. Notice that placing the mouse over the different categories to the left changes the list of tests. The MP+dmb.sy+addr test is under the POPL16 category as all the other tests mentioned in the paper.
• You should now be back to the configuration page and the MP+dmb.sy+addr litmus test should be displayed in the centre.
• We are now ready to start the execution of the example. Click the Interactive button.
• You should now be in the run page and the initial state of the Flowing model should be displayed. Notice there are not events in the storage subsystem topology and the values in memory are all 0. Also notice each of the three threads is ready to fetch the initial instruction.
• Click the green text, prefixed with 0 under "Thread 0 state". This will cause the model to execute the fetch transition for the first instruction in Thread 0.
• You should now see the state of the model after the transition. The red colour indicates the text was added in the last transition. The blue colour indicates the text is part of the Sail interpreter state.
• Click transition 0 twenty four times and see how the Sail interpreter executes the ISA definition of the MOV instruction.
• At this point, Sail determined that a register write should be preformed. Click transition 0 again.
• Finally Sail has finished executing the ISA definition and the first instruction can be committed. Click the 0 transition again.
• Continue executing transitions until there are no more enabled transitions.

• Go to the Flowing web interface by clicking on the Flowing link above
• Open the WRC+addrs litmus test by clicking the Select ARM Test button and then selecting WRC+addrs (under POPL16).
• The WRC+addrs behaviour can be observed only with one topology, to selected it click the Select Topology button and click the [[0,1],2] topology (it should already be selected) and then click the Done button.
• In this example we are not interested in seeing the internal steps the Sail interpreter does. We can instruct the tool to take these transitions automatically for us by clicking on the Select Options button and selecting the Internal (Sail) option. Click the Done button after making the selection.
• Click the Interactive button to start the execution.
• You should now be in the run page and the initial state of the Flowing model should be displayed. Notice the topology we selected is displayed and we now have three thread states.
• Click transition 0. Notice the Sail interpreter has preformed all the internal transitions.
• Click transition 0 to preform the register write and then transition 0 again to commit the instruction.
• Click transition 0 seven times (you might need to wait between clicks) to fetch and preform the next instruction
• Notice that after the STR instruction is committed an event appears in the topology. Click the number 2 that should appear next to it, that will preform a flow transition in the storage subsystem and the event should move down one segment.
• Continue executing transitions until there are no more enabled transitions.

• Go to the POP web interface by clicking on the POP link above
• Open the WRC+addrs litmus test by clicking the Select ARM Test button and then selecting WRC+addrs (under POPL16).
• In this example we want the tool to take eagerly as much transitions as possible, without limiting the possible observed memory behaviour. Click on the Select Options button, select the Simple option and then click the Done button.
• Click the Interactive button to start the execution.
• You should now be in the run page, but this time the tool has already made some transitions. In particular notice the first thread has already committed the MOV instruction. Also notice the storage subsystem state is a POP state and not Flowing.
• Continue executing transitions until there are no more enabled transitions.

• Linux x86_64, Chrome 45.0.2454.101 (64-bit)
• Linux x86_64, Firefox 41.0.1
• Windows 10 x86_64, Chrome 45.0.2454.101 m