Isla: Integrating full-scale ISA semantics andaxiomatic concurrency models

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

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

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 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.
Original languageEnglish
Title of host publicationProceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021)
PublisherSpringer
Number of pages21
Publication statusAccepted/In press - 27 May 2021
Event33rd International Conference on Computer-Aided Verification - Online, Los Angeles, United States
Duration: 18 Jul 202124 Jul 2021
http://i-cav.org/2021/

Conference

Conference33rd International Conference on Computer-Aided Verification
Abbreviated titleCAV 2021
CountryUnited States
CityLos Angeles
Period18/07/2124/07/21
Internet address

Fingerprint

Dive into the research topics of 'Isla: Integrating full-scale ISA semantics andaxiomatic concurrency models'. Together they form a unique fingerprint.

Cite this