@inproceedings{wait-free-weakrefs-ismm23,
author = {
Matthew J. Parkinson and
Sylvan Clebsch and
Ben Simner
},
title = {Wait-Free Weak Reference Counting},
conf = {ISMM 2023},
booktitle = {Proceedings of the 2023 ACM SIGPLAN International Symposium on Memory Management},
year = {2023},
month = jun,
abstract = {
Reference counting is a common approach to memory man- agement. One challenge with reference counting is cycles that prevent objects from being deallocated. Systems such as the C++ and Rust standard libraries introduce two types of reference: strong and weak. A strong reference allows access to the object and prevents the object from being deallocated, while a weak reference only prevents deallocation. A weak reference can be upgraded to provide a strong reference pro- vided there are other strong references to the object. Hence, the upgrade operation is partial, and may fail dynamically. The classic implementation of this upgrade operation is not wait-free, that is, it can take arbitrarily long to complete if there is contention on the reference count.
In this paper, we propose a wait-free algorithm for weak reference counting. The algorithm requires primitive wait- free atomic operations of ``compare and swap'', and ``fetch and add''. We provide a correctness proof of the algorithm using the Starling verfication tool. We provide a full imple- mentation in C++ and demonstrate the best and worst case performance using micro-benchmarks. For our best case sce- nario with high contention, our new algorithm provides ~3x more throughput, while for the worst case the new algorithm is ~85\% slower. Based on a worst case analysis, we provide a second algorithm that combines the strengths of the two algorithms, and has a significantly improved worst case with ~30\% overhead, while maintaining the ~3x speedup for the best case.
},
}
@inproceedings{relaxedvm-esop22,
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}},
conf = {ESOP 2022},
booktitle = {Proceedings of the 31st European Symposium on Programming, ESOP 2022},
year = {2022},
month = apr,
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},
}
@miscs{relaxedvm-arxiv22,
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} (extended version)},
month = mar,
year = {2022},
copyright = {http://creativecommons.org/licenses/by/4.0/},
archivePrefix = {arXiv},
primaryClass = {cs.AR},
eprint = {2203.00642},
note = {\url{http://arxiv.org/abs/2203.00642}},
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 \mbox{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.
This document is an extended version of a paper in ESOP 2022, with additional explanation and examples in the main body, and appendices detailing our litmus tests, models, proofs, and test results.
},
pdf = {https://arxiv.org/pdf/2203.00642},
}
@inproceedings{isla-cav21,
author = {Alasdair Armstrong and Brian Campbell and Ben Simner and Christopher Pulte and Peter Sewell},
title = {Isla: Integrating full-scale {ISA} semantics and axiomatic concurrency models},
conf = {CAV 2021},
booktitle = {Proceedings of the 33rd International Conference on Computer Aided Verification, CAV 2021},
month = jul,
year = {2021},
optpdf = {https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021.pdf},
optnote = {Extended version available at \url{https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021-extended.pdf}},
pdf = {https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021-extended.pdf},
abstract = {
Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g.~100k+ lines for Armv8-A.
In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in Sail, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications, which should be valuable also for other verification tasks. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V.
By using full-scale and authoritative ISA semantics, this lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of \emph{systems} functionality, as used by hypervisors and operating systems, e.g.~instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch model and self-modifying code examples of Simner et al.
},
}
@inproceedings{ifetch-esop20,
author = {Ben Simner and Shaked Flur and Christopher Pulte and Alasdair Armstrong and Jean Pichon-Pharabod and Luc Maranget and Peter Sewell},
title = {{ARMv8-A} system semantics: instruction fetch in relaxed architectures},
conf = {ESOP 2020},
booktitle = {Proceedings of the 29th European Symposium on Programming, ESOP 2020},
year = {2020},
optnote = {This is an extended version of the ESOP 2020 paper, with appendices giving additional details},
abstract = {
Computing relies on \emph{architecture specifications} to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and ``user-mode'' concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the \emph{system semantics}, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software.
In this paper we establish a robust model for one aspect of system semantics: instruction fetch and cache maintenance for ARMv8-A. Systems code relies on executing instructions that were written by data writes, e.g.~in program loading, dynamic linking, JIT compilation, debugging, and OS configuration, but hardware implementations are often highly optimised, e.g.~with instruction caches, linefill buffers, out-of-order fetching, branch prediction, and instruction prefetching, which can affect programmer-observable behaviour. It is essential, both for programming and verification, to abstract from such microarchitectural details as much as possible, but no more. We explore the key architecture design questions with a series of examples, discussed in detail with senior Arm staff; capture the architectural intent in operational and axiomatic semantic models, extending previous work on ``user-mode'' concurrency; make these models executable as test oracles for small examples; and experimentally validate them against hardware behaviour (finding a bug in one hardware device). We thereby bring these subtle issues into the mathematical domain, clarifying the architecture and enabling future work on system software verification.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/iflat/top-extended.pdf}
}
@miscs{rufous-york18,
author = {Ben Simner},
title = {Rufous: Black-box profiling implementations of purely functional data structures},
year = {2018},
month = mar,
abstract = {
It is a common occurrence that a programmer is writing a program, and
wishes to use an abstract datatype. Whether it’s a set, queue or graph, the
programmer has many potential implementations available to them. Deciding
which is the most appropriate for their given use case is difficult. Should they
use a simple set implemented as lists? or is it better to use a more complex
binary tree?
We present Rufous. A modern, easy to use tool for automatic data structure
comparison. Centred around the idea of the datatype-usage-graph, or DUG,
Rufous generates many usages and uses them to build a comprehensive picture
of how implementations of an ADT perform.
Multiple data structures are
automatically profiled and compared, and a report is compiled for the user
to study, so that they can choose the appropriate data structure for their
program.
},
}
@inproceedings{starling-cav17,
title = {Starling: Lightweight Concurrency Verification with Views},
author = {Matt Windsor and Mike Dodds and Ben Simner and Matthew J. Parkinson},
year = {2017},
doi = {10.1007/978-3-319-63387-9_27},
url = {https://doi.org/10.1007/978-3-319-63387-9_27},
researchr = {https://researchr.org/publication/WindsorDSP17},
pages = {544-569},
booktitle = {Proceedings of the 29th International Conference on Computer Aided Verification, CAV 2017},
editor = {Rupak Majumdar and Viktor Kuncak},
volume = {10426},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
isbn = {978-3-319-63387-9},
}