recent.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c recent:"true" -ob recent.bib sewellbib2.bib}}
@misc{n3005,
optkey = {},
author = {Jens Gustedt and Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Martin Uecker},
title = {N3005: A Provenance-aware Memory Object Model for {C}. Working Draft {Technical Specification ISO/IEC TS 6010:2023 (E)}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N3005 \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf}},
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf},
month = jun,
year = {2022},
abstract = {In a committee discussion from 2004 concerning DR260, WG14 confirmed the concept of provenance of pointers,
introduced as means to track and distinguish pointer values that represent storage instances with same address but
non-overlapping lifetimes. Implementations started to use that concept, in optimisations relying on provenance-based alias analysis, without it ever being clearly or formally defined, and without it being integrated consistently
with the rest of the C standard.
This Technical Specification provides a solution for this: a provenance-aware memory object model for C to
put C programmers and implementers on a solid footing in this regard.},
elver = {true},
topic = {WG14},
recent = {true},
optnote = {},
optannote = {}
}
@misc{acs-2020,
optkey = {},
author = {Peter Sewell and Christopher Pulte and Shaked Flur and Mark Batty and Luc Maranget and Alasdair Armstrong},
title = {Multicore Semantics: Making Sense of Relaxed Memory (MPhil slides)},
opthowpublished = {},
month = oct,
year = 2022,
optnote = {\url{https://www.cl.cam.ac.uk/~pes20/slides-acs-2022.pdf}},
url = {https://www.cl.cam.ac.uk/~pes20/slides-acs-2022.pdf},
optannote = {},
recent = {true},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}
@inproceedings{2022-popl-vip,
author = {Rodolphe Lepigre and Michael Sammler and Kayvan Memarian and Robbert Krebbers and Derek Dreyer and Peter Sewell},
title = {{VIP}: Verifying Real-World {C} Idioms with Integer-Pointer Casts},
optcrossref = {},
optkey = {},
conf = {POPL 2022},
booktitle = {Proceedings of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2022},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 6, POPL, Article 20},
optnote = {},
optannote = {},
doi = {10.1145/3498681},
abstract = {Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (e.g.~bitwise) operations on pointer values.
Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of \emph{integer-pointer casts}.
Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t.\ compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee.
However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI.
In this paper, we introduce VIP, a new memory object model aimed at supporting C verification.
VIP sidesteps the complexities of PNVI with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly.
At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI's validation with respect to practice.
In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics.
As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq.
We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP's expressiveness via an implementation in the Cerberus C semantics.},
optapollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
pdf = {http://www.cl.cam.ac.uk/users/pes20/2022-popl-vip.pdf},
supplementarymaterial = {https://doi.org/10.5281/zenodo.5662349},
topic = {Cerberus},
project = {https://gitlab.mpi-sws.org/iris/refinedc},
elver = {true},
recent = {true}
}
@inproceedings{relaxedVM-esop2022,
author = {
Ben Simner and
Alasdair Armstrong and
Jean Pichon-Pharabod and
Christopher Pulte and
Richard Grisenthwaite and
Peter Sewell
},
title = {Relaxed virtual memory in {Armv8-A}},
optcrossref = {},
optkey = {},
conf = {ESOP 2022},
booktitle = {Proceedings of the 31st European Symposium on Programming},
year = {2022},
optbooktitle = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
optbooktitle = {Programming Languages and Systems - 31st European Symposium on Programming,
{ESOP} 2022, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7,
2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13240},
pages = {143--173},
publisher = {Springer},
optyear = {2022},
url = {https://doi.org/10.1007/978-3-030-99336-8\_6},
doi = {10.1007/978-3-030-99336-8\_6},
timestamp = {Fri, 01 Apr 2022 15:49:28 +0200},
biburl = {https://dblp.org/rec/conf/esop/SimnerAPPGS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
abstract = {
Virtual memory is an essential mechanism for enforcing security boundaries,
but its relaxed-memory concurrency semantics has not previously been investigated in detail. The concurrent systems code managing virtual memory has been left on an entirely informal basis, and
OS and hypervisor verification has had to make major simplifying assumptions.
We explore the design space for relaxed virtual memory semantics in the Armv8-A architecture, to support future system-software verification. We identify many design questions, in discussion with Arm; develop a test suite, including use cases from the pKVM production hypervisor under development by Google; delimit the design space with axiomatic-style concurrency models; prove that under simple stable configurations our architectural model collapses to previous ``user'' models; develop tooling to compute allowed behaviours in the model integrated with the full Armv8-A ISA semantics; and develop a hardware test harness.
This lays out some of the main issues in relaxed virtual memory bringing these security-critical systems phenomena into the domain of programming-language semantics and verification with foundational architecture semantics.
},
pdf = {http://www.cl.cam.ac.uk/users/pes20/RelaxedVM-Arm/RelaxedVM-Arm-esop2022.pdf},
topic = {Power_and_ARM},
elver = {true},
project = {http://www.cl.cam.ac.uk/~pes20/RelaxedVM-Arm},
recent = {true}
}
@inproceedings{morello-proofs-esop2022,
author = {Bauereiss, Thomas and Campbell, Brian and Sewell, Thomas
and Armstrong, Alasdair and Esswood, Lawrence and Stark,
Ian and Barnes, Graeme and Watson, Robert N. M. and Sewell,
Peter},
title = {Verified Security for the {Morello} Capability-enhanced
Prototype {Arm} Architecture},
optcrossref = {},
optkey = {},
conf = {ESOP 2022},
booktitle = {Proceedings of the 31st European Symposium on Programming},
year = {2022},
optbooktitle = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
opteditor = {Ilya Sergey},
opttitle = {Verified Security for the Morello Capability-enhanced Prototype Arm
Architecture},
optbooktitle = {Programming Languages and Systems - 31st European Symposium on Programming,
{ESOP} 2022, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7,
2022, Proceedings},
optseries = {Lecture Notes in Computer Science},
optvolume = {13240},
pages = {174--203},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-030-99336-8\_7},
doi = {10.1007/978-3-030-99336-8\_7},
timestamp = {Fri, 01 Apr 2022 15:49:28 +0200},
biburl = {https://dblp.org/rec/conf/esop/BauereissCSAESB22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
optnote = {},
optannote = {},
abstract = {Memory safety bugs continue to be a major source of security vulnerabilities in our critical infrastructure. The CHERI project has proposed extending conventional architectures with hardware-supported \emph{capabilities} to enable fine-grained memory protection and scalable compartmentalisation, allowing historically memory-unsafe C and C++ to be adapted to deterministically mitigate large classes of vulnerabilities, while requiring only minor changes to existing system software sources. Arm is currently designing and building Morello, a CHERI-enabled prototype architecture, processor, SoC, and board, extending the high-per\-for\-mance Neoverse N1, to enable industrial evaluation of CHERI and pave the way for potential mass-market adoption. However, for such a major new security-oriented architecture feature, it is important to establish high confidence that it does provide the intended protections, and that cannot be done with conventional engineering techniques.
In this paper we put the Morello architecture on a solid mathematical footing from the outset. We define the fundamental security property that Morello aims to provide, reachable capability monotonicity, and prove that the architecture definition satisfies it. This proof is mechanised in Isabelle/HOL, and applies to a translation of the official Arm specification of the Morello instruction-set architecture (ISA) into Isabelle. The main challenge is handling the complexity and scale of a production architecture: 62,000 lines of specification, translated to 210,000 lines of Isabelle. We do so by factoring the proof via a narrow abstraction capturing essential properties of arbitrary CHERI ISAs, expressed above a monadic intra-instruction semantics. We also develop a model-based test generator, which generates instruction-sequence tests that give good specification coverage, used in early testing of the Morello implementation and in Morello QEMU development, and we use Arm's internal test suite to validate our model.
This gives us machine-checked mathematical proofs of whole-ISA security properties of a full-scale industry architecture, at design-time. To the best of our knowledge, this is the first demonstration that that is feasible, and it significantly increases confidence in Morello.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/morello-proofs-esop2022.pdf},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
topictwo = {ISA_semantics},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{2022-pldi-islaris,
author = {Michael Sammler and Angus Hammond and Rodolphe Lepigre and Brian Campbell and Jean Pichon-Pharabod and Derek Dreyer and Deepak Garg and Peter Sewell},
title = {{Islaris}: Verification of Machine Code Against Authoritative {ISA} Semantics},
optcrossref = {},
optkey = {},
doi = {10.1145/3519939.3523434},
year = {2022},
isbn = {978-1-4503-9265-5/22/06},
conf = {PLDI 2022},
booktitle = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
optbooktitle = {San Diego, CA, USA},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jun,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
abstract = {
Recent years have seen great advances towards verifying large-scale systems code. However, these verifications are usually based on hand-written assembly or machine-code semantics for the underlying architecture that only cover a small part of the instruction set architecture (ISA). In contrast, other recent work has used Sail to establish formal models for large real-world architectures, including Armv8-A and RISC-V, that are comprehensive (complete enough to boot an operating system or hypervisor) and authoritative (automatically derived from the Arm internal model and validated against the Arm validation suite, and adopted as the official formal specification by RISC-V International, respectively). But the scale and complexity of these models makes them challenging to use as a basis for verification.
In this paper, we propose Islaris, the first system to support verification of machine code above these complete and authoritative real-world ISA specifications. Islaris uses a novel combination of \emph{SMT-solver-based symbolic execution} (the Isla symbolic executor) and \emph{automated reasoning in a foundational program logic} (a new separation logic we derive using Iris in Coq). We show that this approach can handle Armv8-A and RISC-V machine code exercising a wide range of systems features, including installing and calling exception vectors, code parametric on a relocation address offset (from the production pKVM hypervisor); unaligned access faults; memory-mapped IO; and compiled C code using inline assembly and function pointers.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/2022-pldi-islaris.pdf},
project = {https://github.com/rems-project/islaris},
topic = {ISA_semantics},
recent = {true},
elver = {true}
}
@misc{cheri-formal-blog,
optkey = {},
author = {Peter Sewell and Thomas Bauereiss and Brian Campbell and Robert N. M. Watson},
title = {Formal {CHERI}: rigorous engineering and design-time proof of full-scale architecture security properties},
howpublished = {Blog post, \url{https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/}},
month = jul,
year = {2022},
optnote = {},
optannote = {},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
url = {https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@misc{reviewing-blog,
optkey = {},
author = {Peter Sewell},
title = {Bad Reasons to Reject Good Papers, and vice versa},
howpublished = {SIGPLAN PL Perspectives Blog},
month = dec,
year = 2021,
url = {https://blog.sigplan.org/2021/12/07/bad-reasons-to-reject-good-papers-and-vice-versa/},
note = {Also published 2022-12-07 on the Communications of the ACM Blog \url{https://cacm.acm.org/blogs/blog-cacm/267440-bad-reasons-to-reject-good-papers-and-vice-versa/fulltext}},
optannote = {},
recent = {true},
misc = {true},
topic = {misc}
}
@inproceedings{2023-popl-cn,
author = {Christopher Pulte and Dhruv C. Makwana and Thomas Sewell and Kayvan Memarian and Peter Sewell and Neel Krishnaswami},
title = {{CN}: Verifying systems {C} code with separation-logic refinement types},
optcrossref = {},
optkey = {},
conf = {POPL 2023},
booktitle = {Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2023},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {Conditionally accepted},
optnote = {Proc. ACM Program. Lang. 7, POPL, Article 1},
optnote = {},
optannote = {},
doi = {10.1145/3571194},
abstract = {Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability.
We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google's pKVM hypervisor for Android.
},
optapollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cn-draft.pdf},
optsupplementarymaterial = {https://doi.org/10.5281/zenodo.5662349},
topic = {Cerberus},
project = {https://www.cl.cam.ac.uk/~cp526/popl23.html},
elver = {true},
recent = {true}
}
@article{nextwave2023,
author = {Robert N. M. Watson and Peter Sewell and William Martin},
title = {Improving Security with Hardware Support: {CHERI} and {Arm's Morello}},
journal = {The Next Wave (The National Security Agency's review of emerging technologies)},
year = 2023,
optkey = {},
volume = 4,
number = 1,
pages = {10--21},
optmonth = {},
pdf = {https://media.defense.gov/2023/Jan/23/2003148354/-1/-1/0/TNW_24-1_2023_20230112.PDF},
note = {ISSN 2640-1789 (print), ISSN 2640-1797 (online)},
optannote = {},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true},
abstract = {
The CHERI project, from the University of Cambridge and SRI International, extends
instruction-set architectures (ISAs) with unforgeable architectural capabilities, to be
used in place of conventional machine-word addresses to access memory. CHERI, which
stands for Capability Hardware Enhanced Reduced Instruction Set Computer (RISC) Instructions,
deterministically protects C/C++ pointers and other references, and also enables in-address-space software sandboxing. With changes to the compiler and operating system (OS), CHERI
enables new hardware-software security protection models for existing software (typically with
only very minor changes for memory safety):
- Deterministic fine-grained C/C++ memory protection at low overheads; and
- Scalable software compartmentalization, including sandboxed libraries, with interprocess communication performance improvements and function-call-like domain transition.
In a 2020 blog post evaluating CHERI, the Microsoft Security Response Centre (MSRC) wrote:
``We've assessed the theoretical impact of CHERI on all the memory safety vulnerabilities we
received in 2019, and concluded that in its current state, and combined with other mitigations,
it would have deterministically mitigated at least two thirds of all those issues''[1]. Scalable
single-address software sandboxing has the potential to mitigate many more, and to enable a
more disruptive shift to stronger compartmentalized software architectures.
Arm has recently developed the Morello architecture and processor, incorporating the CHERI
protection model into a contemporary high-performance Arm design. Morello is an experimental
prototype extending the existing Armv8-A architecture and Neoverse N1 64-bit processor
design to support CHERI research and evaluation on the path to eventual productization, and
to demonstrate the viability of the CHERI technology using real commercial processes and
manufacturing. Extensive software porting is establishing feasibility. Development boards are
available for research and prototyping as of early 2022, and are already running significant
open-source software stacks, such as an adapted version of the FreeBSD OS and KDE desktop
stack running with strong memory safety [2].
In this article we give an overview of CHERI and Morello, and pointers to full discussions
elsewhere. It is based largely on material from the "Introduction to CHERI" [3] and "Verified
security for the Morello capability-enhanced prototype Arm architecture" [4] technical reports;
it does not contain new research results.
}
}
@article{10123148,
author = {Grisenthwaite, Richard and Barnes, Graeme and Watson, Robert N. M. and Moore, Simon W. and Sewell, Peter and Woodruff, Jonathan},
journal = {IEEE Micro},
title = {The {Arm Morello} Evaluation Platform---Validating {CHERI}-Based Security in a High-Performance System},
year = {2023},
volume = {43},
number = {3},
pages = {50--57},
doi = {10.1109/MM.2023.3264676},
url = {https://ieeexplore.ieee.org/document/10123148},
opturl = {https://www.repository.cam.ac.uk/items/5ce6229c-d21b-4f61-adae-483026648e84},
abstract = {Memory safety issues are a persistent source of security vulnerabilities, with conventional architectures and the C/C++ codebase chronically prone to exploitable errors. The Capability Hardware Enhanced RISC Instructions (CHERI) research project has explored a novel architectural approach to ameliorate such issues using unforgeable hardware capabilities to implement pointers. Morello is an Arm experimental platform for evaluation of CHERI in the Arm architecture context to explore its potential for mass-market adoption. This article describes the Morello Evaluation Platform, covering the motivation and functionality of the Morello architectural hardware extensions; their potential for fine-grained memory safety and software compartmentalization; formally proven security properties; impact on the microarchitecture of the high-performance, out-of-order multiprocessor Arm Morello processor; and the software-enablement program by Arm, the University of Cambridge, and Linaro. Together, this allows a wide range of researchers in both industry and academia to explore and assess the Morello platform.
},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{cheri-c-asplos,
author = {Vadim Zaliva and Kayvan Memarian and Ricardo Almeida and Jessica Clarke and Brooks Davis and Alex Richardson and David Chisnall and Brian Campbell and Ian Stark and Robert N. M. Watson and Peter Sewell},
title = {Formal Mechanised Semantics of {CHERI C}: Capabilities, Provenance, and Undefined Behaviour},
conf = {ASPLOS 2024},
optcrossref = {},
optkey = {},
optbooktitle = {},
year = {2024},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {Accepted for publication, subject to shepherd approval},
optannote = {},
abstract = {Memory safety issues are a persistent source of security vulnerabilities, with conventional architectures and the C codebase chronically prone to exploitable errors. The CHERI research project has shown how one can provide radically improved security for that existing codebase with minimal modification, using unforgeable hardware capabilities in place of machine-word pointers in CHERI dialects of C, implemented as adaptions of Clang/LLVM and GCC. CHERI was first prototyped as extensions of MIPS and RISC-V; it is currently being evaluated by Arm and others with the Arm Morello experimental architecture, processor, and platform, to explore its potential for mass-market adoption, and by Microsoft in their CHERIoT design for embedded cores.
There is thus considerable practical experience with CHERI C implementation and use, but exactly what CHERI C's semantics is (or should be) remains an open question. In this paper, we present the first attempt to rigorously and comprehensively define CHERI C semantics, discuss key semantics design questions relating to capabilities, provenance, and undefined behaviour, and clarify them with semantics in multiple complementary forms: in prose, as an executable semantics adapting the Cerberus C semantics, and mechanised in Coq.
This establishes a solid foundation for CHERI C, for those porting code to it, for compiler implementers, and for future semantics and verification.
},
pdf = {http://www.cl.cam.ac.uk/users/pes20/asplos24spring-paper110.pdf},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{AxSL-popl2024,
author = {Angus Hammond{$^1$} and Zongyuan Liu{$^1$} and Thibaut P{\'{e}}rami and Peter Sewell and Lars Birkedal and Jean Pichon-Pharabod},
title = {An axiomatic basis for computer programming on the relaxed {Arm-A} architecture: the {AxSL} logic},
conf = {POPL 2024},
optcrossref = {},
optkey = {},
booktitle = {Proceedings of the 51st ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2024},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {${}^1$These authors contributed equally. Proc. ACM Program. Lang. 8, POPL, Article 21},
optannote = {},
abstract = {Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the `current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next.
We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.
},
doi = {10.1145/3632863},
pdf = {https://www.cl.cam.ac.uk/~pes20/axsl-popl-2024.pdf},
topic = {Power_and_ARM},
optproject = {},
elver = {true},
recent = {true}
}