An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors

    1
  Kathryn E. Gray1 Gabriel Kerneis1∗ Dominic Mulligan Christopher Pulte1 Susmit Sarkar2 Peter Sewell1

    1University of Cambridge ∗(during this work)                                       2University of St Andrews

ABSTRACT                                                                          not exist as precise artifacts. This is especially prob-
Weakly consistent multiprocessors such as ARM and                                 lematic for the concurrency behaviour of weakly consis-
IBM POWER have been with us for decades, but their                                tent multiprocessors such as ARM and IBM POWER,
subtle programmer-visible concurrency behaviour re-                               where programmer-visible microarchitectural optimisa-
mains challenging, both to implement and to use; the                              tions expose many subtleties:      the traditional docu-
traditional architecture documentation, with its mix of                           mentation does not define precisely which programmer-
prose and pseudocode, leaves much unclear.                                        observable behaviour is (and is not) allowed for con-
                         In this paper we show how a precise architectural        current code; the definitions are not executable as test
envelope model for such architectures can be defined,                             oracles for pre-silicon or post-silicon hardware testing;
taking IBM POWER as our example. Our model spec-                                  they are not executable as an emulator for software test-
ifies, for an arbitrary test program, the set of all its                          ing; and they are not mathematically rigorous enough
allowable executions, not just those of some particular                           to serve as a foundation for software verification.  In-
implementation.                        The model integrates an operational        stead, one has an awkward combination of those PDF
concurrency model with an ISA model for the fixed-                                documents, vendor-internal “golden” simulation models
point non-vector user-mode instruction set (largely au-                           (sometimes in the form of large C/C++ codebases),
tomatically derived from the vendor pseudocode, and                               manually curated test-cases,    and software emulators
expressed in a new ISA description language). The key                             such as gem5 [1] and QEMU [2].
question is the interface between these two:                      allowing               We argue instead that what is needed, for any ar-
all the required concurrency behaviour, without over-                             chitecture, is a definitive architectural envelope spec-
committing to some particular microarchitectural im-                              ification, precisely defining the range of allowed be-
plementation, requires a novel abstract structure.                                haviour for arbitrary code. Such a specification should
                         Our model is expressed in a mathematically rigor-        have many desirable properties:      it should be mathe-
ous language that can be automatically translated to                              matically rigorous, readable, clearly structured, sound
an executable test-oracle tool; this lets one either inter-                       with respect to the vendor      intent, sound with   re-
actively explore or exhaustively compute the set of all                           spect to existing implementations (allowing all exper-
allowed behaviours of intricate test cases, to provide a                          imentally observable behaviour, modulo errata), avoid
reference for hardware and software development.                                  over-commitment to particular microarchitectural im-
                                                                                  plementation choices, have a clear computational intu-
1.  INTRODUCTION                                                                  ition, and be executable as a test oracle, to enumerate,
                                                                                  check or explore the allowed behaviour of test cases, and
1.1 Problem                                                                       hence to serve as a reference.
                      Architecture definitions provide an essential inter-            We show here how this can be achieved for a substan-
face, decoupling hardware and software development,                               tial fragment of the IBM POWER architecture.
but they are typically expressed only in prose and pseu-                          1.2  Context
docode documentation, inevitably ambiguous and with-                                    We build on previous work by Sarkar et al. [3, 4],
out a tight connection to testing or verification; they do                        who describe an architectural model for IBM POWER
Permission to make digital or hard copies of all or part of this work for         concurrency.      That model is expressed in an abstract
personal or classroom use is granted without fee provided that copies are         microarchitectural  style, to give a clear computational
not made or distributed for profit or commercial advantage and that copies        intuition without committing to particular microarchi-
bear this notice and the full citation on the first page. Abstracting with        tectural choices.     There is a storage subsystem model
credit is permitted. To copy otherwise, or republish, to post on servers or to
redistribute to lists, requires prior specific permission and/or a fee. Request   that maintains a state of all the memory writes and
permissions from Permissions@acm.org.                                             barriers seen, the coherence relations among them that
MICRO-48, December 05-09, 2015 Waikiki, HI, USA                                   have been established so far (as a strict partial order),
Copyright is held by the authors. Publication rights licensed to ACM.             and the list of writes and barriers propagated to each
ACM 978-1-4503-4034-2/15/12...$15.00
DOI: http://dx.doi.org/10.1145/2830772.2830775 .                                  thread; this abstracts from the microarchitectural de-

ISA model Litmus frontend Binary frontend ties mentioned above requires several new contributions, which we summarise here and detail below. Power 2.06B test.litmus a.out Concurrency/ISA Model Interface The most fun- Framemaker damental question we address is what the interface be- Framemaker export Litmus parser ELF model Power 2.06B OCaml Lem tween the concurrency model and ISA semantics should XML be (§2). For a single-threaded processor one can regard parse, analyse, patch Concurrency model Harness instructions simply as updating a global register and Power 2.06B memory state. The same holds for a sequentially con- Sail Storage Text UI sistent (SC) multiprocessor, and TSO multiprocessor Sail typecheck semantics Web UI behaviour (as in x86 and Sparc) requires only the addi- Power 2.06B Lem System OCaml, CSS, JS tion of per-thread store buffers. But for weakly consis- Lem (Sail AST) 1 Thread semantics tent multiprocessors such as IBM POWER and ARM, semantics and of the non-multi-copy atomic storage subsystem, Sail interpreter Lem Lem executions some aspects of out-of-order and speculative execution, Lem are exposed to the programmer; we cannot use a simple Figure 1: Overview state-update model for instructions. We explain this, and discuss what is required instead, with a series of concurrent POWER examples. There has been a great tails of any particular cache protocol and storage hier- deal of work on modelling weakly consistent processors, archy. Then there is a model for each hardware thread e.g. [11, 12, 13, 14, 15, 16, 17, 18, 19], but none that we that maintains a tree of in-flight and committed instruc- are aware of deals with these issues with the interface tion instances, expressing the programmer-visible as- to the instruction semantics. pects of out-of-order and speculative computation; this Sail ISA Description Language Architecture de- abstracts from pipeline and local store queue microar- scriptions of instruction behaviour are traditionally ex- chitecture. Together these form an abstract machine pressed in a combination of prose and of pseudocode with a state and transitions. that looks like it is written in a sequential imperative That model has been experimentally validated language (of abstract micro-operations such as assign- against several generations of POWER implementations ments to registers, arithmetic operations, etc.). They (G5, 5, 6, 7, and 8), comparing the model behaviour are also relatively large, with hundreds-to-thousands of with that of production or pre-silicon hardware, on pages of instruction description, and it is important that hand-written litmus tests and on tests produced by the they be accessible to practising engineers. To achieve diy tool of Alglave and Maranget [5], using the Litmus this, permitting instruction descriptions to be expressed test harness [6]. It has been validated intensionally by in that familiar imperative style while simultaneously extensive discussion with a senior IBM architect (clar- supporting the structure we need for integration with ifying the intended concurrency model in the process); the concurrency model, we introduce a new instruction it has been validated mathematically by using it in a description language (IDL), Sail (§3). Sail has a pre- proof that C/C++11 concurrency [7] can be correctly cisely defined and expressive type system, using type compiled to POWER [8, 4]; and the tool has been used inference to check pseudocode consistency while keeping by Linux-kernel software developers [9]. This work (to- instruction descriptions readable. It currently supports gether with related research on axiomatic models [10]) a concrete syntax similar to the POWER pseudocode has also discovered errata in a number of multiprocessor language (front-ends tuned to other conventions are also implementations of POWER and ARM architectures, possible in future). both pre- and post-silicon (ARM concurrency is broadly similar to POWER, though not identical). ISA Description Tied to Vendor Documentation However, that previous model makes many major The vendor specification for the POWER architecture simplifying assumptions. In particular, it includes only is provided as a PDF document [20] produced from a tiny fragment of the POWER instruction set, and Framemaker sources. To keep our ISA model closely even that is given only an ad hoc semantics and only tied to that description, we took an XML version ex- at an assembly level; and it does not handle mixed-size ported by Framemaker and wrote a tool that extracts memory and register accesses. Effectively, it only de- and analyses the instruction descriptions from it, pro- fines the architectural behaviour for simple litmus-test ducing Sail definitions of the decoding and instruction programs, not of more general code. behaviour, and auxiliary code to parse and pretty-print 1.3 Contribution instructions (§4). The vendor pseudocode is less consis- tent than one might hope (unsurprisingly, as it has not In this paper we show how a precise architectural en- previously been mechanically parsed or type-checked), velope model for a weakly consistent architecture can so producing a precise Sail definition required dealing be defined, integrating a concurrency model (extending with ad hoc variations and patching the results. that of [3]) with an architectural model for all of the Extended Concurrency Model Scaling up the pre- fixed-point non-vector user-mode instruction set. Do- vious concurrency model of Sarkar et al. to this larger ing this in a way that achieves all the desirable proper-

ISA also revealed previously unconsidered architectural 1.5 Background: rigorous Lem specification questions, of just what behaviour should be allowed in To express our model in a way which is both various concurrent cases, which we investigated in dis- mathematically precise and executable, we use the cussion with architects and with ad hoc testing (§2, §5). Lem tool [21]. Lem provides a lightweight lan- Test-Oracle Tool To produce a useful tool from our guage of definitions, of types and pure functions, model, building on the previous ppcmem tool [3], we use that can be seen both as mathematical definitions Lem to automatically generate executable OCaml code and as executable pure functional programs; the tool from the mathematical model. We combine this with a typechecks them and (subject to various constraints) front-end for litmus tests, using boilerplate code gener- can export to executable OCaml code, proof assis- ated from the XML, and with a front-end based on a tant definitions for Coq, HOL4, and Isabelle/HOL, formal model of the ELF executable format, to be de- and typeset LaTeX. The Lem type system and li- scribed elsewhere. That gives us a tool, with command- brary include unbounded and bounded integers, tuples line and web interfaces1, for interactively or exhaus- t1*..*tn, records <|l1:t1,..,l2:tn|>, function types tively exploring the architecturally allowed behaviour t1->t2, sets set t, maps map t1 t2, and user-defined of small (but possibly highly intricate) concurrent test types, with top-level ML-style polymorphism. The cases (§6). expression language combines normal pure functional- Validation We validate that our model is a sound de- programming features (functions, pattern-matching, scription of POWER hardware, i.e. that the envelope etc.) together with simple higher-order logic, includ- of behaviour it defines includes the experimentally ob- ing bounded quantification and set comprehensions. servable behaviour of implementations, by comparing 2. THE ISA/CONCURRENCY INTERFACE model and implementation for a range of sequential and concurrent tests (§7). Our discussion with the vendors Modern multiprocessor implementations embody also provides some assurance that the model captures many sophisticated microarchitectural optimisations, the architectural intent on various points. Experimental and weakly consistent multiprocessor architectures testing can never provide complete assurance, of course, make a choice to let some consequences of those be and we intend to maintain and refine the model. observable to programmers; they trade off what is ar- guably a more complex programming model for benefits An overview of our system is in Fig.1, showing the in speed, power, simplicity, or verifiability. To make a formally specified components (in Lem and Sail), the precise architectural envelope model we have to iden- vendor descriptions we start from for the ISA model tify and specify exactly what the intended range of al- (in Framemaker and the derived XML), and the sur- lowed behaviour is, and these observable weakly con- rounding parsing and harness code (in OCaml). The sistent phenomena impact the structure of the model key internal interface is that between the ISA and Con- in interesting ways. At one extreme, we cannot simply currency models. model instructions as atomically updating a global reg- 1.4 Limitations ister and memory state, in the way that a sequential or sequentially consistent concurrent emulator might do, This is, to the best of our knowledge, the first as that would not be sound with respect to actual im- mathematically rigorous architectural model of weakly- plementations (it would not admit all their observable consistent multiprocessor behaviour that is integrated behaviour). But our architectural model should also in- with a substantial instruction-set model. But many volve as little implementation detail as possible, both important limitations remain: it handles only non- for simplicity and to be independent of any particular write-through cacheable coherent memory, and we do implementation. The details of some particular pipeline not consider exceptions and interrupts, floating point, or storage hierarchy (as needed for correctness or per- instruction-cache effects, or supervisor features (includ- formance evaluation of an implementation) would not ing page table manipulation). Given those limitations, make a a good definition of an architecture. our tool provides an emulator for concurrent programs, In this section we show how various weakly consistent but our focus is on making it architecturally complete, phenomena impact the interface between the modelling not on performance (or on performance modelling). We of instructions and that of the concurrency behaviour, compile our mathematical definitions to executable code describing how we can permit the right envelope of be- in a deliberately straightforward fashion, without opti- haviour while remaining as abstract as possible. misation, to maintain confidence that we are execut- 2.1 Constraints from observable behaviour ing the definition, and finding all executions of concur- rent programs is combinatorially challenging. The tool 2.1.1 No single program point should therefore be seen as a reference for small-but- intricate test programs (for hardware testing, and as We recall aspects of experimentally observed be- found in implementations of OS synchronisation primi- haviour that inform our design choices, reusing notation tives and concurrent data structures), not as an emula- and test naming conventions from previous work [3, 4]. tor for production-scale code. First, we have observable out-of-order and speculative execution, as in the MP+sync+ctrl litmus test below. 1http://www.cl.cam.ac.uk/~pes20/ppcmem2 The execution of interest is on the right, with reads-

from (rf), sync, and control-dependency edges between through its program-order (po) predecessors in the tree memory events; the POWER assembly, with initial and to find the most recent one that has written to that reg- final state that identifies that execution, is on the left ister, and take the value from there. We also have to for reference. Here Thread 0 writes some data to x and check that there are no po-intervening instructions that then sets a flag y, with a strong sync barrier between might write to that register (and block until otherwise to keep those two in order as far as any other thread if so), which means that we have to be able to pre- is concerned. Thread 1 reads the flag and then, after calculate their register-write footprints. Two POWER a conditional branch, the data. It is architecturally al- instructions (lswx and stswx) have data-dependent reg- lowed and observable in practice for the load of x to be ister footprints; for these we pre-calculate an upper satisfied speculatively (reading 0 from the initial state), bound that we refine after the XER register read that before the conditional branch is resolved by a load of determines them. y=1 from Thread 0’s write. 2.1.3 Register self-reads MP+sync+ctrl POWER Thread 0 Thread 1 Thread 0 Thread 1 Many instructions have pseudocode that reads from stw r7,0(r1) # x=1 lwz r5,0(r2) # r5=y a: W[x]=1 c: R[y]=1 one of their own register writes. To simplify the defi- sync # sync cmpw r5,r7 # if r5=1 stw r8,0(r2) # y=1 beq L sync rf ctrl nition of when register reads should block, we rewrite ... L: b: W[y]=1 rf d: R[x]=0 them to use a local variable instead. This gives the use- Initial state: 0:r1=x, lwz r4,0(r1) # r4=x ful property that for most instructions the register-read 0:r2=y, 0:r7=1, Test MP+sync+ctrl: Allowed and register-write footprints can be calculated statically 0:r8=1, 1:r1=x, 1:r2=y, 1:r7=1, x=0 Allowed: 1:r5=1, 1:r4=0 from its opcode fields, and that it will dynamically read This means that an operational model that permits all and write exactly once to each element of those. architecturally allowed behaviour cannot simply exe- 2.1.4 Dependencies and register granularity cute the instructions of each hardware thread one-by- In POWER, dependencies between instructions aris- one in program order. Instead, as in Sarkar et al. [3], ing from register-to-register dataflow are architecturally we maintain a tree of in-flight instruction instances for significant (shadow registers notwithstanding), as they each hardware thread, branching at conditional branch guarantee local ordering properties that concurrent con- or calculated jump points, and discarding un-taken sub- texts can observe, and that are used in idiomatic code. trees when branches become committed. For example: Address and data dependencies create local ordering i6 i7 between memory reads and writes, while control de- i1 i2 i3 i4 i5 i10 i11 i12 pendencies do so only in some circumstances (allowing i8 i9 implementations to speculate branches but not to ob- servably speculate values). Processor architectures typ- (committed instructions boxed) i13 ically have a more-or-less elaborate structure of register 2.1.2 No per-thread register state names and aliases. For example, POWER includes 32 64-bit general-purpose registers, GPR[0]..GPR[31] (de- In a sequential, SC, or TSO model, one can treat reg- noted ri in assembly) and a 32-bit condition register isters simply as a per-thread map from architected regis- CR (with bits indexed 32..63) that is partitioned into ter names to values, examined and updated on register 4-bit subfields CR0..CR7; those bits are also referred to reads and writes. But in a pipelined implementation with individual flag names LT, EQ, etc. All this must many instructions can be in flight, and concurrency can be supported in the pseudocode, but the more impor- make microarchitectural shadow registers and register tant semantic question is the architectural granularity renaming indirectly programmer-observable, as in the of mixed-size register accesses: a precise model has to MP+sync+rs example below (a message-passing vari- define when writing to one part of a register and read- ant of Adir et al. [17, Test 6]). Here the three uses of ing from another constitutes a dependency. The choice r5 on Thread 1 do not prevent the second read being is observable in tests such as MP+sync+addr-cr below: satisfied out-of-order (e.g. the first two uses of r5 on Thread 0 is just the same two message-passing writes, Thread 1 might involve one shadow register while the while Thread 1 has a putative dependency chain in- third usage might involve another). This is observable volving a write to CR3 followed by a read form CR4. The on some ARM and POWER processors. final state of 1:r6=1, 1:r5=0 is observable in implemen- MP+sync+rs POWER tations, telling us that a sound architectural model can- Thread 0 Thread 1 not treat CR as a single unit. stw r7,0(r1) # x=1 lwz r5,0(r2) # r5=y sync # sync mr r6,r5 # r6=r5 MP+sync+addr-cr POWER stw r8,0(r2) # y=1 lwz r5,0(r1) # r5=x Thread 0 Thread 1 Initial state: 0:r1=x, 0:r2=y, 0:r7=1, stw r7,0(r1) # x=1 lwz r5,0(r2) # r5 = y 0:r8=1, 1:r1=x, 1:r2=y, x=0 sync # sync mtocrf cr3,r5 # cr3 = 4 bits of r5 Allowed: 1:r6=1, 1:r5=0 stw r8,0(r2) # y=1 mfocrf r6,cr4 # set 4 bits of r6 = cr4 xor r7,r6,r6 # r7 = r6 xor r6 This means that a sound model cannot simply have lwzx r8,r1,r7 # r8 = *(&x + r7) a per-thread register state. Instead, when an instruc- Initial state: 0:r1=x, 0:r2=y, 0:r7=1, tion needs to do a register read, we have to walk back 0:r8=1, 1:r1=x, 1:r2=y, x=0 Allowed: 1:r6=1, 1:r5=0

                             Related experiments show that dependencies through   2.1.6      Non-atomic intra-instruction                  semantics    for
                       individual bits of CR are respected, as are dependencies              register reads
                       through adjacent bits of the same CRn field, so we could                             The previous examples showed that we need to be
                 treat CR either as a collection of 4-bit fields or as 32 1-bit                         able to dynamically analyse the register and memory

fields. The vendor documents are silent on this ques- writes of an instruction that is partially executed but tion, but the latter seems preferable: it allows the most not yet committed, but so far one might imagine that hardware implementation variation; we do not believe one could model each instruction atomically moving that code in the wild relies on false-register-sharing de- between three states: not started, fully executed but pendencies (though of course it is hard to be sure of not committed, and committed. The following exam- this); and it is mathematically simplest. We follow this ple shows that this is not the case, even for instructions choice for all register accesses, with a general definition that do just one memory write: we have to be able that assembles the value for a register read by reassem- to see that the memory footprint of an instruction be- bling fragments of the most recent writes (in POWER, comes determined after only some of its register reads the GPR registers are always fully written). have been satisfied, in order to know that po-later in- It is also important that interactions via the current structions will definitely be to different addresses and instruction address (CIA) do not give rise to dependen- hence can be executed out-of-order (before all the reg- cies in the model, as that would prevent out-of-order ister reads of the first instruction are resolved) without execution. The POWER instruction descriptions read violating coherence. and write two pseudoregisters, CIA and NIA, which are Without the middle writes of the example (b and not architected registers; our thread model treats those e), one has a plain ‘LB’ test, which is intended to specially. be architecturally allowed for POWER and ARM. The LB+datas+WW variant has extra writes, to two dif- 2.1.5 Reading from uncommitted instructions ferent addresses, inserted in the middle of each thread. For out-of-order execution to work, we clearly have to These middle writes are merely data-dependent on the let instructions read from register writes of po-previous first reads, not address-dependent, so even before the instructions that are not yet finished, just as in im- reads have been satisfied, the middle writes can be plementations register values might be forwarded from known to be to different addresses to the last writes on instructions before they are retired. each thread. In some implementations this lets those But we also have to let po-later instructions read from writes go ahead out-of-order and be read from by the the memory writes of earlier instructions in specula- reads on the other thread. If instead those middle writes tive paths. The POWER architecture states that writes were address-dependent on the first reads (as in a test are not performed speculatively but, while speculative LB+addrs+WW, not shown), then before those reads writes are never visible to other threads, they can be are satisfied the middle writes would not be known to be forwarded locally to program-order-later reads on the to different addresses to the last writes on each thread, same thread. The PPOCA variant of MP below shows and the last writes could not go ahead. The former is that this forwarding is observable to the programmer. observable on some ARM processors; the latter is not. Here f is address-dependent on e, which reads from the For the current POWER server processors, no LB vari- write d, which is control-dependent on c. One might ex- ant is observable. pect that chain to prevent read f binding its value before LB+datas+WW POWER Thread 0 Thread 1 c does, but in fact the write d can be forwarded directly Thread 0 Thread 1 to e within the thread while d, e, and f are all still spec- lwz r5,0(r1) # r5=x lwz r6,0(r2) # r6=y a: R[x]=1 d: R[y]=1 stw r5,0(r3) # z=r5 stw r6,0(r4) # w=r6 rf rf ulative (before the branch of the control dependency on stw r9,0(r2) # y=1 stw r9,0(r1) # x=1 data data c is resolved). This is intended to be architecturally Initial state: x=0, y=0, 0:r1=x, 0:r2=y, 0:r3=z, 0:r9=1, b: W[z]=1 e: W[w]=1 allowed and it is observable in practice; it means that 1:r1=x, 1:r2=y, 1:r4=w, 1:r9=1 the model must expose uncommitted writes to po-later Allowed: 0:r5=1, 1:r6=1 po po instructions. c: W[y]=1 f: W[x]=1 Test LB+datas+WW: Allowed A write instruction typically has a register read that PPOCAThread 0 Thread 1 POWER supplies the data to be written and one or more register stw r7,0(r1) # x=1 lwz r5,0(r2) # r5=y Thread 0 Thread 1 reads that are used to compute the address to be writ- sync # sync cmpw r5,r7 # if r5=1 a: W[x]=1 c: R[y]=1 ten, e.g. as in pseudocode below for the stw RS,D(RA) stw r8,0(r2) # y=1 beq L ... sync ctrl instruction used for those middle writes. This calculates L: rf an effective address EA from register RA and instruction stw r7,0(r3) # z=1 b: W[y]=1 d: W[z]=1 field lwz r6,0(r3) # r6=z D before reading the data from register RS and do- xor r6,r6,r6 # r6=r6 xor r6 rf ing the memory write. lwz r4,r6,r1 # r4=*(&x+r6) Initial state: 0:r1=x, 0:r2=y, 0:r7=1, e: R[z]=1 (bit[64]) b := 0; 0:r8=1, 1:r1=x, 1:r2=y, 1:r3=z, 1:r7=1, x=0, z=0 rf addr (bit[64]) EA := 0; Allowed: 1:r5=1, 1:r4=0 f: R[x]=0 if RA == 0 then b := 0 else b := GPR[RA]; EA := b + EXTS (D); Test PPOCA: Allowed MEMw(EA,4) := (GPR[RS])[32 .. 63]

      To permit LB+datas+WW, after the address register   atomic transactions, though they sometimes do need
  reads can be resolved (i.e., after the program-order-   to be aborted or restarted). But their individual pseu-
  previous instructions that write those registers have   docode can be interpreted sequentially, taking care with
     produced values for them, whether or not they have   the sequencing of register reads leading to addresses vs
     been committed), we have to be able to compute the   those leading to data.         The interface to an executing

write address, even if the data register reads cannot yet instruction has to expose its register and memory read be resolved, so that later instructions that might have and write events, together with memory barrier events. been to the same address can go ahead. In contrast, Other instruction instances in a thread have to be able whether the data register reads can be resolved has no to make progress while one is blocked waiting for a reg- effect on later instructions. Hence: ister read or memory read to be satisfied. It has to be 1. It would be unsound to block the middle writes un- possible to forward from a po-previous memory write in til their entire register-read footprint is available, the same thread that has not yet been committed. as that would block the later writes. We also saw that it is necessary to be able to dynami- cally calculate the possible memory read and write foot- 2. It would be sound to interpret the pseudocode in a print of a partially executed instruction instance, ana- dataflow style, or to rewrite it with explicit intra- lyzing its future behaviour, and we have to know which instruction concurrency, but that would introduce pending register reads can affect those footprints. unnecessary nondeterminism. This can all be achieved most simply, and with a tight connection to a readable pseudocode description of in- 3. It would be sound to interpret the pseudocode as structions, by a deep embedding of a formally defined written sequentially, as the address reads are be- pseudocode language (or instruction description lan- fore the data reads (but it would not be if they guage, IDL) into the generic Lem mathematical meta- were reversed). language in which our model is written; such an em- We adopt the last alternative, but note that this means bedding represents the typed instruction description as we have to be able to dynamically recalculate the poten- a Lem term of a Lem type for the IDL AST. We describe tial memory read and write footprint of an instruction our Sail IDL in the next section. It is given semantics in progress, after some but not all of its register reads with a Sail interpreter, defined in Lem, and that inter- are resolved. preter has a simple interface to the rest of the model, with types as below (slightly condensed for presenta- 2.1.7 Undefined values tion). Instruction descriptions often leave some register bits type instruction_state explicitly undefined, e.g. for some flag bits, or 32 bits of the result register in POWER multiply-word instruc- type outcome = tions. There are several possible interpretations of this. | Read_mem of address * size * (memval -> instruction_state) One could: (a) make a nondeterministic choice at as- || Write_mem of address * size * memval * instruction_state signment time (if stable, or when read, if not); (b) | Barrier of barrier_kind * instruction_state Read_reg of reg_slice * (regval -> instruction_state) feed in the concrete values from an observed hardware | Write_reg of reg_slice * regval * instruction_state or simulator trace; (c) work over lifted bits, 0, 1, or | Internal of instruction_state undef; or (d) work with symbolic bit values and accu- | Done mulate constraints on them. Option (a) is mathemati- val interp : instruction_state -> outcome cally attractive and suitable for testing software above the model, but would make it combinatorially infeasible val decode : context to find all allowed behaviours even for small examples, -> opcode -> instruction_or_decode_error and likewise infeasible to compare our emulator results val initial_state : context against actual hardware. Option (b) could be attractive -> instruction -> instruction_state_or_error for conformance testing vs. an existing simulator. Op- tion (d) is also combinatorially challenging, especially if The interpreter works over a type instruction_state any such bits are used in addresses. We currently sup- which is abstract as far as the rest of the model is con- port (c), allowing undefined bits in register and memory cerned. The main interp function takes a single in- values (to support testing against actual hardware) but struction state and executes it for one step, to produce not in address or instruction-field values (as that would an outcome. This is a labelled union type in which the make semantic exploration infeasible). This is reflected memory and register read cases include an instruction- in the interface to the ISA semantics. state continuation, abstracted on the value that should 2.2 The ISA semantics interface be supplied by the rest of the model. This lets us decou- ple the behaviour of a single instruction from the rest From the above, we can see that there is (so far) no of the system (other instructions can execute while that need for intra-instruction parallelism in the model. We continuation is saved). have to be able to execute multiple instructions from There are also functions to decode an opcode to an a thread concurrently, and to represent partially exe- instruction (an element of an instruction-set abstract- cuted instructions (instructions cannot be regarded as syntax type, and to create an initial instruction state

Store Doubleword with Update DS-form union ast member (bit[5],bit[5],bit[14]) Stdu

stdu RS,DS(RA) function clause decode Sl hl (: 0b111110 (bit[5]) RS 3 ik 16 31 : (bit[5]) RA : (bit[14]) DS EA © (RA) + EXTS(DS || 0b00) : 0b01 MEM(EA, 8 € (RS) as instr ) = RA © EA Stdu (RS,RA,DS) Let the effective address (EA) be the sum (RA)+ (DSII0b00). (RS) is stored into the doubleword in function clause execute (Stdu (RS, RA, DS)) = storage addressed by EA. { EA := GPR[RA] + EXTS (DS : 0b00); MEMw(EA,8) := GPR[RS]; EA is placed into register RA. GPR[RA] := EA } If RA=0, the instruction form is invalid. Special Registers Altered: function clause invalid (Stdu (RS, RA, DS)) = None (RA == 0)

Figure 2: Example instruction description, in vendor documentation and in Sail, showing the close correspondence between the two for execute and decode

from that; these are parameterised by a context which prises a language, with a formally defined type system, is essentially the complete ISA definition. and a tool that parses and typechecks ISA definitions, To calculate the potential register and memory foot- exporting them to a type-annotated Lem AST, and an prints of an instruction (from either its initial state or interpreter (written in Lem) that executes them. a partially executed state) we can simply run the inter- We illustrate Sail with an example instruction de- preter exhaustively, feeding in a distinguished unknown scription in Fig. 2 (stdu, one of the simplest of the value to the continuations for any reads; the interpreter several hundred instructions we consider). On the left operations treat unknown similarly to undef. It can also is the vendor documentation, while on the right are calculate the register reads that feed into memory ad- Sail definitions of a clause of the abstract-syntax type dresses by doing this with dynamic taint tracking. ast of instructions (Stdu, with three bitvector fields), a clause of the decode function, pattern-matching 32- 3. SAIL: ISA DEFINITION LANGUAGE bit opcode values into that abstract-syntax type, and a To express the mass of individual instruction descrip- clause of the execute function, defining the instruction behaviour, and a clause of the invalid predicate, iden- tions, we need an instruction definition language that tifying invalid instructions. Sail supports conventional (1) supports the interface in the previous section, in- imperative code, with access to memory (the write to cluding the interp, decode, and initial_state func- MEMw) and registers (the reads and writes of GPR[·]), tions and the analysis of the potential footprints and instruction fields from the AST value (RS, RA, DS), lo- dependencies of partially executed instructions, (2) is cal variables (EA), sequencing, conditionals, and loops. mathematically precise, and (3) is readable by engineers The Sail interpreter produces outcomes for register and familiar with the existing vendor documentation. There memory accesses, and for memory barriers, as described has been a great deal of previous work using domain- in the previous section. specific IDLs and proof assistants to describe instruc- We equip the language with an expressive type sys- tion behaviour: for emulation, generation of compiler tem to check consistency and detect errors in Sail defini- components, test generation, formal verification of com- tions. Many POWER instructions (especially the vector pilers and of hardware, etc. [22]. Emulators such as instructions) involve elaborate manipulation of bitvec- gem5 [1] and QEMU [2] each have their own internal tors, with computed indices and lengths, and registers descriptions of instruction behaviour. On the more for- are indexed from various start-index values. To check mal side, notable recent examples include the work of these we use a type system in which types can be de- Fox [23] for ARM in his L3 IDL, and Goel et al. [24] pendent on simple arithmetic expressions. In particu- for x86 in ACL2. Some of these are both precise and lar, for any type t, start index s, length l, and direction readable (and some rather complete), but to the best d, Sail has a type vector<s,l,d,t> of vectors of t, and of our knowledge none addresses instruction behaviour the start index and length can be computed, e.g. from in the context of weakly consistent multiprocessors and instruction fields and loop indices. In general type- the issues of the previous section. Accordingly, we have checking in such a system quickly becomes undecidable, developed a new IDL, Sail, for the purpose. Sail com-

with numeric constraints involving addition, multiplica- worked instead from an alternative XML export pro- tion, and exponentiation, but the constraints that arise vided by IBM from the Framemaker source. We wrote in practice for our ISA specification are simple enough a tool that extracts instruction descriptions automati- (e.g. 0 ≤ 2n + m, given n ≥ 0 and m ≥ 0) that they cally from this, stores them in an intermediate format can be handled by an ad hoc solver. Sail type construc- suitable for analyses, and produces a Sail model for tors (including user-defined types) and functions can be decoding and executing instructions, as well as helper parametric in types, in natural-number values, and in OCaml code to parse, execute and pretty-print litmus directions. In the POWER description indices increase tests. Some instructions needed additional patching, along a bitvector, from MSB to LSB, while other ar- e.g. for the setting of arithmetic flags, which are de- chitectures use the opposite convention; this direction scribed in the manual in prose, not in pseudocode, and polymorphism lets us use either style directly, without for a few errors in the pseudocode. error-prone translation and sharing the same library of The tool has to deal with many irregularities in the basic operations. Sail function types can be annotated XML to pull out the main blocks shown on the left of by sets of effects, to identify whether they are pure or Fig. 2 (instruction name, form, mnemonic, binary rep- can have register or memory side-effects, and there is resentation, pseudocode, and list of special registers al- also simple effect polymorphism. To keep Sail defini- tered) and parse the pseudocode into a simple untyped tions readable, we use type inference and some limited grammar. The powerful type inference that Sail pro- automatic coercions (between bits, bitvectors of length vides makes it simple to generate Sail code from this. 1, and numbers; from bit vectors to unsigned numbers; and between constants and bit vectors), so very few type 4.1 Current Status annotations are needed — none in the right-hand side We focus mainly on the user-mode Branch Facility of Fig. 2 except for the sizes of the instruction opcode and Fixed-Point Facility instructions of the POWER fields in the decode function. ISA User Instruction Set Architecture [20]. In the ver- All this lets us have definitions of decoding and sion we worked from, these include 154 normal user in- behaviour that are simultaneously precise and close structions; we currently extract decoding information enough to the vendor pseudocode to be readable, as and instruction pseudocode for all of these, and we de- Fig. 2 shows. scribe our test generation and validation for them in §7 (these instruction counts refer to the underlying in- 4. FROM VENDOR DOCUMENT TO SAIL structions as identified in the documentation, e.g. the Given a metalanguage for instruction description, one four add, add., addo, and addo. variants of Add are could produce a description for an existing architecture counted together as one). There are 5 system-call and manually, reading the existing prose+pseudocode doc- trap instructions, which are not in our scope, in those umentation and rendering it into the IDL. This gives chapters. We also handle memory barriers: the sync, the flexibility to refactor the definition, e.g. with an eye lwsync, eieio, and isync instructions from Chapter 4 to particular proofs in the work of Fox [23] and to fast of Book II: POWER ISA Virtual Environment Architec- symbolic evaluation in that of Goel et al. [24]. Some- ture; for these the instruction semantics simply signals times one may have to follow this manual approach: the corresponding event to the concurrency model. the existing documentation varies widely in how rigor- The remaining user ISA for server implementations ously defined and how complete the instruction descrip- comprises the vector, floating-point, decimal floating- tions are, from something reasonably precise for ARM point, and vector-scalar floating-point instructions. We through to something much less so for x86, and in any extract decoding information for almost all of these, case for some purposes such refactoring is essential. But and pseudocode for many of the vector instructions, but ISA definitions are moderately large (100s to 1000s of specifying floating-point operations is a major topic in pages), making this an error-prone and tedious task, itself [26, 27, 28], not in our scope here. and the result is less tightly coupled to the original than All this produces approximately 8500 lines of Sail, one might like: it may not be readable by practicing en- defining the Sail AST, decoding, and execution for 270 gineers, and it may be hard to update to a new version instructions, and around 17 000 lines of OCaml code to of the vendor specification. parse, pretty-print, and manipulate assembly instruc- The obvious alternative is to try to automatically ex- tions. tract all the information one can, doing as little manual During development we were provided with an up- patching as possible. This has been done for a sequen- dated version of the XML export; it required less than tial ARM description by Shi et al. [25], from PDF to a two days of work to adapt the extraction process (de- model complete enough to boot a kernel and theorem- spite various changes to XML tags), suggesting that this prover definitions in Coq. could be maintained over time and that in principle it For POWER, the vendor pseudocode is in between could be gradually integrated into a vendor workflow. those mentioned above in rigour, looking reasonably precise at first sight, and so an automatic extraction 5. THE CONCURRENCY MODEL seems feasible and worthwhile. It is maintained inter- Looking back at the Fig. 1 overview, Sections 2, 3, nally as a Framemaker document, publicly released as and 4 have described the left-hand block: our ISA model PDF. Neither is intended to be easily parsed, and so we and its interface. We now describe the concurrency

model, with respect to that of our starting point [3]. committing a memory write or barrier to the storage The thread semantics is adapted throughout to han- subsystem, issuing a memory read request, satisfying a dle mixed-size register accesses and the model of in- memory read from the storage subsystem, or an inter- struction behaviour from §2.2, and also to maintain an nal step; the thread can also fetch a new instruction explicit tree of in-flight instructions. instance at any leaf of its tree. To relate to the inter- For mixed-size memory accesses the thread model preter interface we saw earlier, the abstract micro-op also decomposes misaligned and large (vector) writes state of an instruction is an element of: into their architecturally atomic units. POWER is a type micro_op_state = non-multicopy-atomic architecture: two writes by one thread to different locations can become visible to two || MOS_plain of instruction_state MOS_pending_mem_read of other threads in opposite orders. This is an observable read_request * (memval -> instruction_state) consequence of the storage hierarchy and cache protocol | MOS_potential_mem_write of microarchitecture of implementations, but our model (list write) * instruction_state abstracts from those details; it maintains an explicit storing the continuation provided by the interpreter in description of the memory writes (and barriers) that the memory-read case. An instruction instance com- have been propagated to each hardware thread, and of bines this with the statically analysed footprint data, the coherence commitments between writes that have obtained by running the interpreter exhaustively, and a been established so far. The decomposition allows the record of the register and memory reads and writes the atomic units of an ISA memory write to be separately instruction has performed (cleared if the instruction is propagated to other threads. restarted). Handling mixed-size memory access requires a further At present we treat instruction and data memory change to the storage subsystem model: there are now separately, not having investigated the interactions be- coherence relationships between overlapping writes with tween concurrency and instruction-cache effects. In- distinct footprints (their address/size pairs). struction fetches read values from a fixed instruction For concreteness, we show the Lem type of our new memory, decode them (if possible) using the Sail decode storage subsystem state below. It is a record type, with function, as in Fig. 2, and use the exhaustive interpreter fields containing various sets, relations, and functions. to analyse their register footprint and potential next For example, the coherence field is a binary relation fetch addresses. The exhaustive interpreter is also used over write, a type of memory write events. This too is as necessary to re-analyse the possible future memory a record type (not shown), containing a unique id, an footprint of partially executed instructions. address and size, and a memory value (a list of bytes of The complete state of the model simply collects these lifted bits). components together: type storage_subsystem_state = <| type system_state = <| threads: set thread_id; program_memory: address -> fetch_decode_outcome; writes_seen: set write; initial_writes: list write; coherence: rel write write; interp_context: Interp_interface.context; events_propagated_to: thread_id -> list event; thread_states: map thread_id thread_state; unacknowledged_sync_requests: set barrier;|> storage_subsystem: storage_subsystem_state; The storage subsystem model can take transitions be- idstate: id_state; model: model_params; |> tween such states, to accept a new write or barrier from with a function to enumerate all the possible transitions a thread, to send a response to a read request, to prop- of a system state: agate a write or barrier to a new thread, to acknowl- edge a sync barrier to its originating thread when the val enumerate_transitions_of_system : relevant events have propagated to all threads, and to system_state -> list trans establish new coherence commitments. The details of val system_state_after_transition : our model lie in the preconditions and resulting states system_state -> trans -> system_state_or_error of such transitions. We cannot include them here, for lack of space (the interpreter and concurrency model 6. THE TOOL, WITH ELF AND LITMUS are around 4300 and 2800 non-comment lines of speci- fication), but we intend to make them available online. FRONT-ENDS From the type and transitions described above, though, To make an executable tool from our mathematical one can see that the model is abstracting from particu- model, following Fig. 1, we use the §4 extraction tool to lar microarchitecture but can still be directly related to generate a Sail definition of our POWER ISA fragment implementation behaviour. For example, some model and Sail to typecheck that and translate into a Lem def- coherence-commitment transitions will correspond to inition which we link with the concurrency model. Lem one write winning a race for cache-line ownership. typechecks both and translates into executable OCaml. The corresponding type for the model of each thread We link that with an OCaml test harness for ex- is essentially a tree of instruction instances, each of ploring the system-state transitions and with two front- which can take transitions for register writes or reads, ends: one to parse litmus tests such as the §2 examples, for making a memory write locally visible, satisfying a and another to parse statically linked Power64 ELF ex- memory read by locally forwarding from such a write, ecutable binaries. The former is based on the herdtools

Storage subsystem state: writes seen = { W 0x0000000000001050(x)/4=0x00000001, W 0x0000000000001040(y)/4=0x00000000, W 0x0000000000001050(x)/4=0x00000000} coherence = { W 0x0000000000001050(x)/4=0x00000000 -> W 0x0000000000001050(x)/4=0x00000001 } events propagated to: Thread 0: [ W 0x0000000000001040(y)/4=0x00000000, W 0x0000000000001050(x)/4=0x00000000, W 0x0000000000001050(x)/4=0x00000001 ] Thread 1: [ W 0x0000000000001040(y)/4=0x00000000, W 0x0000000000001050(x)/4=0x00000000 ] 4 Propagate write to thread: W 0x0000000000001050(x)/4=0x00000001 to Thread 1 unacknowledged Sync requests = {}

Thread 0 state: instruction: 0 ioid: 6 address: 0x0000000000050000 stw RS=7 RA=1 D=0 regs_in: {GPR7[32..63], GPR1} regs_out: {} NIAs: {succ} committed memory writes: W 0x0000000000001050(x)/4=0x00000001 remaining micro-operations: | () local variables: EA=0b0...01000001010000, b=0b0...01000001010000 0 (0:6) Finish 1 (0:6) Fetch from address 0x0000000000050004 sync L=0

Thread 1 state: instruction: 0 ioid: 4 address: 0x0000000000051000 lwz RT=5 RA=2 D=0 regs_in: {GPR2} regs_out: {GPR5} NIAs: {succ} remaining micro-operations: | GPR[to_num (RT)] := (0b00000000000000000000000000000000 : MEMr (EA,4)) local variables: EA=0b0...01000001000000, b=0b0...01000001000000 2 (1:4) Memory read request from storage R 0x0000000000001040(y)/4

instruction: 1 ioid: 5 address: 0x0000000000051004 cmp BF=0 L=0 RA=5 RB=7 regs_in: {XER.SO, GPR5[32..63], GPR7[32..63]} regs_out: {CR[32..35]} NIAs: {succ} remaining micro-operations: | a := EXTS (64,(GPR[5])[32 .. 63]); | b := EXTS (64,(GPR[to_num (RB)])[32 .. 63]) | if a < b then c := 0b100 else if a > b then c := 0b010 else c := 0b001; | CR[4BF+32 .. 4BF+35] := c : [XER.SO] local variables: b=0b0...0, a=0b0...0 3 (1:5) Fetch from address 0x0000000000051008 bc BO=12 BI=2 BD=1 AA=0 LK=0

This shows a state for the first MP+sync+ctrl example of §2.1, from the user interface of our tool (lightly edited for presentation). This state is reachable after 44 non-internal transitions, and the possible next transitions are underlined and highlighted in green; in the web interface they are clickable. The delta from the previous state is highlighted in red. Finished instruction instances are shown in a more condensed form, but there are none in this state. For each instruction, the remaining Sail abstract microoperations are shown in blue. Memory events (the writes and reads of x and y shown in the §2.1 execution diagram) are shown in cyan. On Thread 0 the write x=1 (in full, W 0x0000000000001050(x)/4=0x00000001) of the first stw has just been committed to the storage subsystem, and in the storage subsystem state it is coherence-after an initial-state write, but it has not yet been propagated to Thread 1. The sync can be fetched, but it will not be propagatable to Thread 1 until that first write is. On Thread 1 the first lwz and cmp are both executing. The former can read y from memory, and if that is done now (before the Thread 0 write of y=1 has been committed and propagated to Thread 1) it will get the zero from the initial state write. The cmp is blocked on a register read from GPR[5] waiting for the lwz to write to it. Thread 1 continues with a bc conditional branch; that fetch transition is already enabled, and after that fetch the final load lwz could also be fetched, and indeed also speculatively satisfy its read of x immediately, though it could not be committed until the branch is. The regs_in, regs_out, and NIAs static-analysis data for the cmp show how its precise register footprint has been calculated, including particular subfields and bit-ranges of XER, CR, and GPR registers.

Figure 3: A tool screenshot with a system state and currently enabled transitions for MP+sync+ctrl

front-end of Maranget et al. [29], using assembly pars- struction does register and memory reads or writes), ing and pretty-printing code produced by our extrac- and the vendor ISA description [20, §1.6.28] of how in- tion tool from the XML POWER definition. The lat- struction fields are used and what registers or mem- ter uses a mathematical model of the ELF file format, ory locations an instruction using this instruction field also written in Lem. Parsed binaries are checked for might depend on. Most of this can be done uniformly: static linkage and conformance with the Power64 ABI only 13 special cases were needed for individual instruc- before their loadable segments are identified and loaded tions, and 7 for certain load/store instruction forms. into the tool’s code memory. Names of global variables, For single-bit mode fields, our test generation is exhaus- their addresses in the executable memory image, and tive. For the 154 user-mode branch and fixed-point in- their initialisation values are also extracted to initialise structions, we currently generate 6984 tests (we omit the tool’s data memory and the user-interface symbol only conditional branches to absolute addresses). Run- pretty-printer. Text and web interactive user interfaces ning these on POWER 7 hardware and in our model, show the current state and enabled transitions; the user all of these instructions pass all their tests. This testing can select any of those, automatically skip internal tran- has found around 33 bugs, variously in our ISA model sitions, run sequentially, or (resources permitting) do an (e.g. where we omitted flag setting that is not in the exhaustive search. Fig. 6 gives a tool screenshot, show- pseudocode or made multiple accesses to the same reg- ing a model state and its enabled transitions. ister), interpreter (e.g. arithmetic mismatches), concur- rency model, and test generation. There was also one 7. TEST GENERATION AND VALIDATION error in the manual’s pseudocode and four cases where We validate our model in several ways. For the se- the pseudocode and text disagree. quential behaviour of instructions, we generate random For concurrent testing, we checked 2175 litmus tests, single-instruction tests and compare the behaviour of including those of §2 and [3], each of which identifies a the model (run in sequential mode) against that of a non-SC execution which might or might not be allowed POWER 7 server (allowing the hardware to exhibit ar- in the model or observed in practice. For each we ran bitrary values where the model has undef bits). For con- the model exhaustively to calculate the set of possible current behaviour, we use a range of concurrent litmus results it allows, and compared against previous exper- tests, running the model in exhaustive concurrent mode imentally observed behaviour for POWER G5, 6, 7 and and checking the set of results for each test includes 8 hardware. This identified a small number of problems those previously found by testing hardware (POWER in the model, all of which were fixed. Systematic gen- G5, 6, 7, and 8) using the litmus tool [6]. Experimen- eration of good litmus tests that exercise all the new tal testing can never give complete assurance, of course, features of the model is a research problem for future and we expect to evolve the model over time, but these work in itself, as there are now many more possibilities. results establish a reasonable level of confidence that our model is sound with respect to the behaviour of 8. CONCLUSION POWER hardware implementations. Assessing com- We have shown how one can construct a rigorous ar- pleteness is harder, as it is essentially a question of the chitectural model for a substantial fragment of a so- architectural intent of the vendor or designer, which phisticated multiprocessor architecture, combining in- has not previously been expressed precisely — enabling struction description and concurrency model to make that is the point of our work. But our discussion with a precise artifact embodying the architectural abstrac- IBM staff also serves to validate that our model cap- tion, not merely a prose document. The fact that we tures the vendor architectural intent for a number of can compute the set of all model-allowed outcomes for specific points. To the best of our knowledge our tool extensive sequential and concurrent tests validates our is complete, allowing all the behaviour that they intend claim that it can serve as a test oracle. to be allowed, except for certain exotic cases of unde- This opens up many possibilities for future work: us- fined behaviour or computed branches, which would be ing the model as a reference for hardware validation, combinatorially infeasible to enumerate. for exploring whether future microarchitecture designs In more detail, for sequential testing we wrote a tool provide the same programmer-observable concurrency to automatically generate assembly tests for each in- behaviour, and for testing whether implementations of struction supported by the model, for interesting partly- software concurrency libraries are correct with respect random combinations of machine state and instruction to the architecture (previous sequential POWER hard- parameters, and taking care with branches and suchlike. ware testing deemed construction of an architecture Each test can be run either in the model or on actual model to be a “critical step [that] should not be un- hardware, logging the register values and relevant mem- derestimated” [30]). Related work on ARM is also in ory state before and after execution of the instruction in progress [31]. question, then we compare those logfiles (up to undef). We have focussed on precision, clarity, abstraction, These tests are standard ELF binaries produced with soundness, and completeness, not on performance, and GCC (so this also exercises our ELF front-end). that is the obvious limitation of our current tool: it is Tests are generated largely automatically, from the just fast enough for the testing we have considered (the Sail names and inferred types of instruction fields, the sequential and concurrent checking above take minutes inferred Sail effect annotation (stating whether the in- and hours respectively, on a single machine). There is

ample scope for improving both sequential and concur- [14] J. M. Stone and R. P. Fitzgerald, “Storage in the rent performance, though the latter will always be lim- PowerPC,” IEEE Micro, vol. 15, pp. 50–58, April 1995. ited by the combinatorial challenge. Ideally one would [15] C. May, E. Silha, R. Simpson, and H. Warren, eds., The be able to generate high performance, verified, and ar- PowerPC architecture: a specification for a new family of chitecturally complete emulators from such models, but RISC processors. San Francisco, CA, USA: Morgan that needs a great deal of further research. Kaufmann Publishers Inc., 1994. We have done all this for a pre-existing industrial [16] S. V. Adve and K. Gharachorloo, “Shared memory consistency models: A tutorial,” IEEE Computer, vol. 29, architecture, but our techniques, tools, and much of the no. 12, pp. 66–76, 1996. concurrency model should also be applicable to research [17] A. Adir, H. Attiya, and G. Shurek, “Information-flow architectures. There one can hope to escape some of the models for shared memory with an application to the legacy issues and move directly to precise architecture PowerPC architecture,” IEEE Trans. Parallel Distrib. descriptions that one can test against. Syst., vol. 14, no. 5, pp. 502–515, 2003. [18] J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, “Fences 8.1 Acknowledgements in weak memory models,” in Proc. CAV, 2010. [19] D. Lustig, M. Pellauer, and M. Martonosi, “Pipe check: We acknowledge funding from EPSRC grants Specifying and verifying microarchitectural enforcement of EP/H005633 (Leadership Fellowship, Sewell) and memory consistency models,” in Proceedings of the 47th EP/K008528 (REMS Programme Grant), an ARM Annual IEEE/ACM International Symposium on Microarchitecture, MICRO-47, (Washington, DC, USA), iCASE award (Pulte), and the Scottish Funding Coun- pp. 635–646, IEEE Computer Society, 2014. cil (SICSA Early Career Industry Fellowship, Sarkar). [20] Power ISA Version 2.06B. IBM, 2010. https://www.power.org/wp-content/uploads/2012/07/ 9. REFERENCES PowerISA_V2.06B_V2_PUBLIC.pdf (accessed 2015/07/22). [21] D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, “Lem: reusable engineering of real-world [1] N. Binkert, B. Beckmann, G. Black, S. K. Reinhardt, semantics,” in Proc. ICFP, 2014. A. Saidi, A. Basu, J. Hestness, D. R. Hower, T. Krishna, S. Sardashti, R. Sen, K. Sewell, M. Shoaib, N. Vaish, M. D. [22] P. Misra and N. Dutt, eds., Processor Description Hill, and D. A. Wood, “The gem5 simulator,” SIGARCH Languages. Morgan Kaufmann, 2008. Comput. Archit. News, vol. 39, pp. 1–7, Aug. 2011. [23] A. C. J. Fox, “Directions in ISA specification,” in [2] F. Bellard, “QEMU, a fast and portable dynamic Interactive Theorem Proving – Third International translator,” in Proceedings of the Annual Conference on Conference, ITP 2012, Princeton, NJ, USA, August 13-15, USENIX Annual Technical Conference, ATEC ’05, 2012. Proceedings (L. Beringer and A. P. Felty, eds.), (Berkeley, CA, USA), pp. 41–41, USENIX Association, vol. 7406 of Lecture Notes in Computer Science, 2005. pp. 338–344, Springer, 2012. [3] S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and [24] S. Goel, W. A. Hunt, M. Kaufmann, and S. Ghosh, D. Williams, “Understanding POWER multiprocessors,” in “Simulation and formal verification of x86 machine-code PLDI, 2011. programs that make system calls,” in Proceedings of the 14th Conference on Formal Methods in Computer-Aided [4] S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell, Design, FMCAD ’14, (Austin, TX), pp. 18:91–18:98, L. Maranget, J. Alglave, and D. Williams, “Synchronising FMCAD Inc, 2014. C/C++ and POWER,” in Proc. PLDI, 2012. [25] X. Shi, J.-F. Monin, F. Tuong, and F. Blanqui, “First steps [5] J. Alglave and L. Maranget, “The diy tool.” towards the certification of an ARM simulator using http://diy.inria.fr/. Compcert,” in Certified Programs and Proofs (J.-P. [6] J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, “Litmus: Jouannaud and Z. Shao, eds.), vol. 7086 of Lecture Notes in running tests against hardware,” in Proc. TACAS 2011, Computer Science, pp. 346–361, Springer Berlin 2011. Heidelberg, 2011. [7] M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber, [26] J. Harrison, “Floating-point verification,” Journal of “Mathematizing C++ concurrency,” in Proc. POPL, 2011. Universal Computer Science, vol. 13, pp. 629–638, may 2007. [8] M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell, [27] S. Boldo and G. Melquiond, “Flocq: A unified library for “Clarifying and compiling C/C++ concurrency: from proving floating-point algorithms in Coq,” in Proceedings of C++11 to POWER,” in Proc. POPL, 2012. the 2011 IEEE 20th Symposium on Computer Arithmetic, [9] P. McKenney, “Validating memory barriers and atomic ARITH ’11, (Washington, DC, USA), pp. 243–252, IEEE instructions,” Linux Weekly News, 2011. Computer Society, 2011. http://lwn.net/Articles/470681/. [28] D. M. Russinoff, “Computation and formal verification of [10] J. Alglave, L. Maranget, and M. Tautschnig, “Herding cats: SRT quotient and square root digit selection tables,” IEEE Modelling, simulation, testing, and data-mining for weak Trans. Comput., vol. 62, pp. 900–913, May 2013. memory,” in Proceedings of the 35th ACM SIGPLAN [29] L. Maranget et al., “herdtools.” Conference on Programming Language Design and https://github.com/herd/herdtools. Implementation, PLDI ’14, (New York, NY, USA), pp. 40–40, ACM, 2014. [30] L. Fournier, A. Koyfman, and M. Levinger, “Developing an [11] M. Dubois, C. Scheurich, and F. Briggs, “Memory access architecture validation suite: Applicaiton to the PowerPC buffering in multiprocessors,” in Proceedings of the 13th architecture,” in DAC, pp. 189–194, 1999. Annual International Symposium on Computer [31] S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin, Architecture, ISCA ’86, (Los Alamitos, CA, USA), L. Maranget, W. Deacon, and P. Sewell, “Modelling the pp. 434–442, IEEE Computer Society Press, 1986. ARMv8 architecture, operationally: Concurrency and ISA,” [12] W. Collier, Reasoning about parallel architectures. in Proceedings of POPL, 2016. Prentice-Hall, Inc., 1992. [13] K. Gharachorloo, “Memory consistency models for shared-memory multiprocessors,” WRL Research Report, vol. 95, no. 9, 1995.