Isla: Integrating full-scale ISA semantics and axiomatic concurrency models (extended version)

Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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 instructionset 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 the Sail language, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V. The symbolic execution engine is valuable also for other verification tasks: it has been used in automated ISA test generation for the Arm Morello prototype architecture, extending Armv8-A with CHERI capabilities, and for Iris program-logic reasoning about binary code above the Armv8-A and RISC-V ISA specifications. By using full-scale and authoritative ISA semantics, Isla 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 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 instructionfetch and virtual-memory models and examples of Simner et al.
Original languageEnglish
Number of pages30
JournalFormal Methods in System Design
Early online date12 May 2023
Publication statusE-pub ahead of print - 12 May 2023

Keywords / Materials (for Non-textual outputs)

  • instruction set architecture
  • axiomatic concurrency
  • symbolic execution


Dive into the research topics of 'Isla: Integrating full-scale ISA semantics and axiomatic concurrency models (extended version)'. Together they form a unique fingerprint.
  • Isla: Integrating full-scale ISA semantics andaxiomatic concurrency models

    Armstrong, A., Campbell, B., Simner, B., Pulte, C. & Sewell, P., 15 Jul 2021, Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021). Springer, p. 303-316 14 p. (Lecture Notes in Computer Science; vol. 12759).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access

Cite this