# topic.ISA_semantics.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -c 'topic:"ISA_semantics" or topictwo:"ISA_semantics"' -ob topic.ISA_semantics.bib sewellbib2.bib}}

@inproceedings{DBLP:conf/micro/GrayKMPSS15,
author = {Kathryn E. Gray and
Gabriel Kerneis and
Dominic P. Mulligan and
Christopher Pulte and
Susmit Sarkar and
Peter Sewell},
title = {An integrated concurrency and core-{ISA} architectural envelope definition,
and test oracle, for {IBM} {POWER} multiprocessors},
abstract = {Weakly consistent multiprocessors such as ARM and IBM POWER have been with us for decades, but their subtle programmer-visible concurrency behaviour remains challenging, both to implement and to use; the traditional architecture documentation, with its mix of prose and pseudocode, leaves much unclear.

In this paper we show how a precise architectural envelope model for such architectures can be defined, taking IBM POWER as our example.  Our model specifies, for an arbitrary test program, the set of all its allowable executions, not just those of some particular implementation.  The model integrates an operational concurrency model with an ISA model for the fixed-point non-vector user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in a new ISA description language).  The key question is the interface between these two: allowing all the required concurrency behaviour, without overcommitting to some particular microarchitectural implementation, requires a novel abstract structure.

Our model is expressed in a mathematically rigorous language that can be automatically translated to an executable test-oracle tool; this lets one either interactively explore or exhaustively compute the set of all allowed behaviours of intricate test cases, to provide a reference for hardware and software development.
},
conf = {MICRO 2015},
booktitle = {Proceedings of the 48th International Symposium on Microarchitecture,
, Waikiki, HI, USA},
pages = {635--646},
year = {2015},
month = dec,
optcrossref = {DBLP:conf/micro/2015},
opturl = {http://doi.acm.org/10.1145/2830772.2830775},
pdf = {http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf},
doi = {10.1145/2830772.2830775},
timestamp = {Sun, 10 Jan 2016 12:42:56 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/micro/GrayKMPSS15},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}

@inproceedings{DBLP:conf/popl/FlurGPSSMDS16,
author = {Shaked Flur and
Kathryn E. Gray and
Christopher Pulte and
Susmit Sarkar and
Ali Sezgin and
Luc Maranget and
Will Deacon and
Peter Sewell},
title = {Modelling the {ARMv8} architecture, operationally: concurrency and {ISA}},
abstract = {In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA).  Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware.

Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor's architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined.  We therefore first develop a concurrency model with a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardware-designer intuition.  This means it can be discussed in detail with ARM architects.  We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t.~the first.

The instruction semantics involves further difficulties, handling the mass of detail and the subtle intensional information required to interface to the concurrency model.  We have a novel ISA description language, with a lightweight dependent type system, letting us do both with a rather direct representation of the ARM reference manual instruction descriptions.

We build a tool from the combined semantics that lets one explore, either interactively or exhaustively, the full range of architecturally allowed behaviour, for litmus tests and (small) ELF executables.  We prove correctness of some optimisations needed for tool performance.

We validate the models by discussion with ARM staff, and by comparison against ARM hardware behaviour, for ISA single- instruction tests and concurrent litmus tests.},
conf = {POPL 2016},
booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, St. Petersburg,
FL, USA },
pages = {608--621},
year = {2016},
month = jan,
optcrossref = {DBLP:conf/popl/2016},
opturl = {http://doi.acm.org/10.1145/2837614.2837615},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf},
project = {http://www.cl.cam.ac.uk/~sf502/popl16/index.html},
optproject = {http://www.cl.cam.ac.uk/~pes20/popl16-armv8/},
doi = {10.1145/2837614.2837615},
timestamp = {Fri, 08 Jan 2016 18:18:25 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/FlurGPSSMDS16},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}

@inproceedings{mixed17,
author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell},
title = {Mixed-size Concurrency: {ARM}, {POWER}, {C/C++11}, and {SC}},
conf = {POPL 2017},
booktitle = {The 44st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages,  Paris, France},
year = {2017},
month = jan,
pages = {429--442},
numpages = {14},
opturl = {http://doi.acm.org/10.1145/3009837.3009839},
doi = {10.1145/3009837.3009839},
project = {http://www.cl.cam.ac.uk/users/pes20/popl17/},
abstract = {Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store.  In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level.  A semantic foundation for software, therefore, has to address them.

We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff.  This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting.  In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency.  We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses.

This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}

@inproceedings{armv8-mca,
author = {Christopher Pulte and Shaked Flur and Will Deacon and Jon French and Susmit Sarkar and Peter Sewell},
title = {{Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8}},
optcrossref = {},
optkey = {},
conf = {POPL 2018},
booktitle = {Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages},
optpages = {},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
doi = {10.1145/3158107},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {Draft},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/},
abstract = {ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8.  Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits.  In particular, the model was originally \emph{non-multicopy-atomic}: writes could become visible to some other threads before becoming visible to all --- but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features.  The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model.  It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.

In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}

@inproceedings{sail-popl2019,
author = {Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Alastair Reid and Kathryn E. Gray and Robert M. Norton and Prashanth Mundkur and Mark Wassell and Jon French and Christopher Pulte and Shaked Flur and Ian Stark and Neel Krishnaswami and Peter Sewell},
title = {{ISA} Semantics for {ARMv8-A, RISC-V, and CHERI-MIPS}},
optcrossref = {},
optkey = {},
conf = {POPL 2019},
booktitle = {Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 3, POPL, Article 71},
optnote = {},
optannote = {},
doi = {10.1145/3290384},
abstract = {Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification.  But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground.

In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4.  Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite.

We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq.  We use the former for validation, and to assess specification coverage.  To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation.  We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration.  We prove (on paper) the soundness of the core Sail type system.

We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.
},
pdf = {http://www.cl.cam.ac.uk/users/pes20/sail/sail-popl2019.pdf},
supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/sail/popl2019.html},
topic = {ISA_semantics},
topictwo = {cheri},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
recent = {true}
}

@inproceedings{sail-arw18,
author = {  Alasdair Armstrong and
Thomas Bauereiss and
Brian Campbell and
Shaked Flur and
Kathryn E. Gray and
Prashanth Mundkur and
Robert M.~Norton and
Christopher Pulte and
Alastair Reid and
Peter Sewell and
Ian Stark and
Mark Wassell},
title = {Detailed Models of Instruction Set Architectures: From
Pseudocode to Formal Semantics},
optcrossref = {},
optkey = {},
conf = {Automated Reasoning Workshop (ARW) 2018},
booktitle = {Proc. Automated Reasoning Workshop},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {23--24},
month = apr,
optorganization = {},
optpublisher = {},
note = {Two-page abstract. Proceedings available at \url{https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf}},
optannote = {},
topic = {ISA_semantics},
topic2 = {cheri},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
pdf = {http://www.cl.cam.ac.uk/~pes20/sail/2018-04-12-arw-paper.pdf},
abstract = {Processor instruction set architectures (ISAs) are typically specified using a mixture of prose and
pseudocode. We present ongoing work on expressing such specifications rigorously and automatically trans-
lating them to interactive theorem prover definitions, making them amenable to mechanised proof. Our ISA
descriptions are written in Sail—a custom ISA specification language designed to support idioms from var-
ious processor vendor’s pseudocode, with lightweight dependent typing for bitvectors, targeting a variety of
use cases including sequential and concurrent ISA semantics. From Sail we aim to portably generate usable
theorem prover definitions for multiple provers, including Isabelle, HOL4, and Coq. We are focusing on the
full ARMv8.3-A specification, CHERI-MIPS, and RISC-V, together with fragments of IBM POWER and x86.}
}

@inproceedings{sail-arw18-minisail,
author = {Alasdair Armstrong and Neel Krishnaswami and Peter Sewell and Mark Wassell},
title = {Formalisation of {MiniSail} in the {Isabelle} Theorem Prover},
optcrossref = {},
optkey = {},
conf = {Automated Reasoning Workshop (ARW) 2018},
booktitle = {Proc. Automated Reasoning Workshop},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {27--28},
month = apr,
optorganization = {},
optpublisher = {},
note = {Two-page abstract. Proceedings available at \url{https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf}},
optannote = {},
topic = {ISA_semantics},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
pdf = {http://www.cl.cam.ac.uk/~pes20/sail/arw18_mpew2.pdf},
abstract = {Sail is a language used to model instruction set architectures. It has an imperative syntax and a
dependent type system. We formalise a core calculus of the language in the Isabelle theorem prover describing
the language syntax, substitution, the type system and operational semantics. A number of classic theorems
such as preservation and progress are then proved. The purpose of this formalisation is to ensure that the full
language is built on sound foundations and to provide a platform for the generation of the implementation of
a type checker and evaluator for the language.}
}