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.
Notes
We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at digitize@ucalgary.ca