TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA

  • Authors:
    Caroline J. Trippel (Princeton)
    Publication ID:
    P090942
    Publication Type:
    e-Workshop
    Received Date:
    19-May-2017
    Last Edit Date:
    19-May-2017
    Research:
    2384.008 (University of Michigan)
    Replay:
    44 minutes
    Sign in to see the View Replay button »

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 hardware-software 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 talk will make a case for full-stack MCM verification and present a toolflow, TriCheck, capable of verifying that the HLL, compiler, ISA, and implementation collectively uphold MCM requirements. There will be a focus in this talk on TriCheck’s ability to evaluate a proposed ISA MCM in order to ensure that each layer and each mapping is correct and complete. Specifically, this will consist of an application of TriCheck to the open source RISC-V ISA, seeking to verify accurate, efficient, and legal compilations from C11. Under-specifications and potential inefficiencies in the current RISC-V ISA documentation are uncovered and possible solutions for each are identified. Additionally, this talk will demonstrate the applicability of TriCheck to verifying other components of the hardware-software stack by identifying two counter-examples to a previously "proven-correct" compiler mapping from C11/C++11 to both POWER and ARMv7. Overall, this talk demonstrates the necessity of full-stack verification for detecting MCM-related bugs in the hardware-software stack.

Past Events

  Event Summary
18 May 2017
STARnet
STARnet
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
Thursday, May 18, 2017, 4 p.m.–5 p.m. ET
Ann Arbor, MI, United States

E-Workshop

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450