The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

Specifying and dynamically verifying address translation-aware memory consistency

The work

AuthorsBogdan F. Romanescu; Alvin R. Lebeck; Daniel J. Sorin
Editors
Typemisc
Year2010
Citekeyromanescu2010specifying

Where it appeared

Pages323--334

Identifiers

DOI10.1145/1736020.1736057
OpenAlexW4254298894

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

Abstract

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.

How it got here

How it got hereagent via openalex
Added2026-10-26 12:42 UTC
Not denied bya person 2026-10-29 17:12 UTC

Filed under

verified-memory

Cite it as

@misc{romanescu2010specifying,
  title        = {Specifying and dynamically verifying address translation-aware memory consistency},
  author       = {Bogdan F. Romanescu and Alvin R. Lebeck and Daniel J. Sorin},
  year         = {2010},
  pages        = {323--334},
  doi          = {10.1145/1736020.1736057},
}

This record lives at https://refs.drheap.org/romanescu2010specifying/ and will keep doing so.