Programmer-Centric Conditions for Itanium Memory Consistency
Date
2006-08-17
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
A programmer-centric model of memory consistency provides a sequence
of instructions for each proces- sor, and requires that these sequences
satisfy a collection of rules. It also requires that the notion of validity
of a sequence is the natural one: the value read from a shared memory
location must be one that was written by the most recent preceding instruction
that stored to the same location. A programmer-centric model supports
reasoning about programs at a non-operational level. It is not obscured by
the implementation details of the underlying architecture. In this paper, we
formulate a programmer-centric description of the memory consistency model
provided by the Itanium architec- ture. However, our definition is not tight.
We provide two very similar definitions, each motivated by slightly different
implementations of load-acquire instructions, and prove that the specification
of the Itanium memory model lies strictly between the two. We also entertain
a handful of other natural notions of load-acquire rules and show that none
exactly captures the Itanium specification. This leads us to question whether
the specification of the Itanium memory order [5] is actually faithful to the
Itanium architects' intentions.
Description
Keywords
Computer Science