Specifying and dynamically verifying address translation-aware memory consistency

Conference Paper

Computer systems with virtual memory are susceptible to design bugs and runtime faults in their address translation (AT) systems. Detecting bugs and faults requires a clear specification of correct behavior. To address this need, we develop a framework for AT-aware memory consistency models. We expand and divide memory consistency into the physical address memory consistency (PAMC) model that defines the behavior of operations on physical addresses and the virtual address memory consistency (VAMC) model that defines the behavior of operations on virtual addresses. As part of this expansion, we show what AT features are required to bridge the gap between PAMC and VAMC. Based on our AT-aware memory consistency specifications, we design efficient dynamic verification hardware that can detect violations of VAMC and thus detect the effects of design bugs and runtime faults, including most AT related bugs in published errata. Copyright © 2010 ACM.

Full Text

Duke Authors

Cited Authors

  • Romanescu, BF; Lebeck, AR; Sorin, DJ

Published Date

  • May 19, 2010

Published In

  • International Conference on Architectural Support for Programming Languages and Operating Systems Asplos

Start / End Page

  • 323 - 334

International Standard Book Number 13 (ISBN-13)

  • 9781605588391

Digital Object Identifier (DOI)

  • 10.1145/1736020.1736057

Citation Source

  • Scopus