COATCheck: Verifying memory ordering at the hardware-OS interface

Daniel Lustig, Geet Sethi, Margaret Martonosi, Abhishek Bhattacharjee

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

32 Scopus citations

Abstract

Modern computer systems include numerous compute elements, from CPUs to GPUs to accelerators. Harnessing their full potential requires well-defined, properly-implemented memory consistency models (MCMs), and low-level system functionality such as virtual memory and address translation (AT). Unfortunately, it is difficult to specify and implement hardware-OS interactions correctly; in the past, many hardware and OS specification mismatches have resulted in implementation bugs in commercial processors. In an effort to resolve this verification gap, this paper makes the following contributions. First, we present COATCheck1, an address translation-aware framework for specifying and statically verifying memory ordering enforcement at the microarchitecture and operating system levels. We develop a domain-specific language for specifying ordering enforcement, for including ordering-related OS events and hardware micro-operations, and for programmatically enumerating happens-before graphs. Using a fast and automated static constraint solver, COATCheck can efficiently analyze interesting and important memory ordering scenarios for modern, high-performance, out-of-order processors. Second, we show that previous work on Virtual Address Memory Consistency (VAMC) does not capture every translation-related ordering scenario of interest, and that some such cases even fall outside the traditional scope of consistency. We therefore introduce the term transistency model to describe the superset of consistency which captures all translation-aware sets of ordering rules.

Original languageEnglish (US)
Title of host publicationASPLOS 2016 - 21st International Conference on Architectural Support for Programming Languages and Operating Systems
PublisherAssociation for Computing Machinery
Pages233-247
Number of pages15
ISBN (Electronic)9781450340915
DOIs
StatePublished - Mar 25 2016
Event21st International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016 - Atlanta, United States
Duration: Apr 2 2016Apr 6 2016

Publication series

NameInternational Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
Volume02-06-April-2016

Other

Other21st International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016
CountryUnited States
CityAtlanta
Period4/2/164/6/16

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'COATCheck: Verifying memory ordering at the hardware-OS interface'. Together they form a unique fingerprint.

Cite this