Flowing and POP (ARMv8) Web-interface
A Tool for Exploring the ARMv8 ISA and Memory Models
|
This is a web-interface for the tool described in this POPL16 paper.
It allows one to interactively explore all the behaviours the Flowing
and POP models admit for a litmus test selected from a library or written
by hand.
Usage
To use the web interface click on the Flowing
or POP link. The interface has two
main pages, the configuration page where the desired litmus test and options
are selected, and the run page where the selected test is run interactively.
Configuration Page:
- Select ARM Test: a
library of tests is provided with the tool and can be accessed from
here, or a test can be pasted in or edited in the central box.
- Select Options: this opens a dialog that lets you chose some run
options, affecting whether the tool automatically (eagerly) takes some simple transitions.
- Select Topology (Flowing only): this opens a dialog that lets you
chose the topology of the storage subsystem.
- Run Interactive: after a litmus test and the desired options have
been selected, this
starts the tool, constructing the initial state of the model for that
test and calculating its allowed transitions..
Run Page:
- System State: this box displays the current state of
the model, with the storage subsystem state at the top and the thread subsystem
state (for each thread in the test) below. The possible transitions
are shown underlined in green and can be clicked to take them.
To allow better tracking of changes after each transition, the
interface will colour in red things that were just added or changed and in grey
things that were removed since the last state.
The state of each thread includes, for each fetched instruction, the
state of the sail interpreter as the remaining Sail abstract microcode
to execute for this instruction (blue).
- Undo button: undo the last transition
- Reset button: return to the configuration page
Thread subsystem legend:
- ioid: unique identifier of the instruction instance.
- loc: the memory address of the instruction, followed by the
instruction assembly.
- opcode: the instruction opcode (ELF mode only, not available in
the web interface).
- regs_in/regs_out: the set of registers the instruction reads
from/writes to
- ioids_feeding_address: the set of instructions that make register
writes that feed address calculation in the current instruction
- nias: the set of possible Next Instruction Addresses.
- mem writes_read_from: the memory writes the instruction read from.
- committed_mem_writes: the memory writes the instruction committed.
- committed_barriers: the barriers the instruction committed.
- reg_reads: the registers the instruction has read from
(notice that reg_reads is dynamic and gets populated only after the
read has happened, where regs_in is calculated statically when the
instruction is fetched).
- reg_writes: the registers the instruction has written to
(notice that reg_writes is dynamic and gets populated only after the
write has happened, where regs_out is calculated statically when the
instruction is fetched).
- committed: true when the instruction has been committed.
- finished: true when the Sail interpreter has finished.
Examples
Below we show three examples in detail. To keep them simple, the
instructions explore only a tiny part of the reachable state space; to
see more interesting concurrent behaviour, one should select one of
the eager-transition options and explore more complex interactions
between threads and between threads and the storage subsystem models.
For each of the `Allowed' tests in the paper, it should be possible,
with some understanding of the model from the paper, to
find an execution that reaches the specified final state.
Guided Example 1 (POP with automatic 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).
- Open the WRC+addrs litmus test by clicking the Select ARM
Test button and then selecting WRC+addrs. Notice that placing the
mouse over the different categories to the left changes the list of
tests. The WRC+addrs test is under the POPL16 category, as are all
the other tests mentioned in the paper.
- In this example we want the tool to take eagerly as many
transitions as possible, without limiting the possible observed memory
behaviour. Click on the Select Options button, select "the above and
additional believed-safe transitions" option and then click the Done
button.
- Click the Run Interactive button to start the execution.
- You should now be in the run page. The tool has already
made some transitions. In particular notice the first thread has already
committed the MOV instruction.
- Clicking transition 0 twice to make Thread 0 preform the store of x=1.
- Click transition 0 to make Thread 1 issue a read request for x.
- Click transition 1 to propagate x=1 to Thread 1.
- Click transition 2 to propagate the read request of x to Thread 0.
- Click transition 2 to satisfy the read request of x with the write x=1.
- Click transition 0 twice to make Thread 1 preform the store of y=1.
- Click transition 0 to make Thread 2 issue a read request for y.
- Click transition 2 to propagate y=1 to Thread 2.
- Click transition 2 to propagate the read request of y to Thread 1.
- Click transition 2 to satisfy the read request of y with the write y=1.
- Click transition 0 to make Thread 2 issue a read request for x.
- Click transition 2 to propagate the read request of x to Thread 0.
- Click transition 2 to propagate the read request of x to Thread 1.
- Click transition 2 to satisfy the read request of x with the initial value x=0.
- Click transition 0 to propagate x=1 to Thread 2.
- Click transition 0 to propagate y=1 to Thread 0.
Guided Example 2 (Flowing with ISA transitions)
- 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.
- You should now be back to the configuration page and the
MP+dmb.sy+addr litmus test should be displayed in the centre. You
might want to keep Section 4.1 open while running the test, so you
can relate the test source to the model states you reach.
- We are now ready to start the execution of the example. Click the
Run Interactive button.
- You should now be in the run page and the initial state of the
Flowing model should be displayed. Notice there are no events in the
storage subsystem topology and the values in memory are all 0.
Also notice that each of the two threads is ready to fetch the initial
instruction.
- Click the green "Fetch from address" 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 what has changed in this last transition.
The blue colour indicates the text is part of the Sail interpreter
state for this instruction: it's just about to execute the
Sail
MoveWide
function.
- 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.
Guided Example 3 (Flowing with automatic ISA transitions and selecting topology)
- 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
select it click the Select Topology button and click the [[0,1],2]
topology (if it is not already 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 instruction-internal transitions" option.
Click the Done button after making the selection.
- Click the Run 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 performed all
the internal transitions and now a register write transition is enabled.
- 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 perform 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 perform a flow transition in the storage subsystem and the event
should move down one segment.
- Click transition 0 thirteen times to issue the read request of x
by Thread 1 and the read request of y by Thread 2.
- Click transition 2 twice to make the read request of x flow down
and satisfy by x=1.
- Click transition 0 thirteen times to complete the read of x=1 and
commit of y=1 by Thread 1.
- Click transition 2 twice and then transition 0 twice to make the
write y=1 flow all the way to memory.
- Click transition 1 and then transition 0 to make the read request
of y flow all the way to memory and satisfy by y=1.
- Click transition 0 nine times to complete the read of y=1 and
issue read request of x by Thread 2.
- Click transition 1 and then transition 0 to make the read request
of x flow all the way to memory and satisfy by x=0.
- Click transition 0 twice to complete the read of x=0 by Thread 2.
- Click transition 0 twice to make the write x=1 flow all the way to memory.
Browser compatibility:
we have tested the interface on the following
configurations:
- 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