TriCheck: Memory model verification at the trisection of software, hardware, and ISA

Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Rose Martonosi

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

14 Scopus citations

Abstract

Memory consistency models (MCMs) which govern intermodule interactions in a shared memory system, are a significant, yet often under-appreciated, aspect of system design. MCMs are defined at the various layers of the hardwaresoftware stack, requiring thoroughly verified specifications, compilers, and implementations at the interfaces between layers. Current verification techniques evaluate segments of the system stack in isolation, such as proving compiler mappings from a high-level language (HLL) to an ISA or proving validity of a microarchitectural implementation of an ISA. This paper makes a case for full-stack MCM verification and provides a toolflow, TriCheck, capable of verifying that the HLL, compiler, ISA, and implementation collectively uphold MCM requirements. The work showcases TriCheck's ability to evaluate a proposed ISA MCM in order to ensure that each layer and each mapping is correct and complete. Specifically, we apply TriCheck to the open source RISCV ISA [55], seeking to verify accurate, efficient, and legal compilations from C11. We uncover under-specifications and potential inefficiencies in the current RISC-V ISA documentation and identify possible solutions for each. As an example, we find that a RISC-V-compliant microarchitecture allows 144 outcomes forbidden by C11 to be observed out of 1,701 litmus tests examined. Overall, this paper demonstrates the necessity of full-stack verification for detecting MCM-related bugs in the hardware-software stack.

Original languageEnglish (US)
Title of host publicationASPLOS 2017 - 22nd International Conference on Architectural Support for Programming Languages and Operating Systems
PublisherAssociation for Computing Machinery
Pages119-133
Number of pages15
ISBN (Electronic)9781450344654
DOIs
StatePublished - Apr 4 2017
Event22nd International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017 - Xi'an, China
Duration: Apr 8 2017Apr 12 2017

Publication series

NameInternational Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
VolumePart F127193

Other

Other22nd International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017
CountryChina
CityXi'an
Period4/8/174/12/17

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Hardware and Architecture

Keywords

  • C11
  • Compilation
  • Computer architecture
  • Heterogeneous parallelism
  • Memory consistency
  • RISC-V
  • Shared memory
  • Verification

Fingerprint Dive into the research topics of 'TriCheck: Memory model verification at the trisection of software, hardware, and ISA'. Together they form a unique fingerprint.

  • Cite this

    Trippel, C., Manerkar, Y. A., Lustig, D., Pellauer, M., & Martonosi, M. R. (2017). TriCheck: Memory model verification at the trisection of software, hardware, and ISA. In ASPLOS 2017 - 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (pp. 119-133). (International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS; Vol. Part F127193). Association for Computing Machinery. https://doi.org/10.1145/3037697.3037719