Browsing by Author "Jackson, LillAnne"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
- ItemOpen AccessCapturing Register and Control Dependence in Memory Consistency Models with Applications to the Itanium Architecture(2006-07-11) Higham, Lisa; Jackson, LillAnne; Kawash, JalalA complete framework for modelling memory consistency that includes register and control dependencies is presented. It allows us to determine whether or not a given computation could have arisen from a given program running on a given multiprocessor architecture. The framework is used to provide an exact description of the computations of (a subset of) the Itanium instruction set on an Itanium multiprocessor architecture. We show that capturing register and control dependencies is crucial: a producer/consumer problem is solvable without using strong synchronization primitives on Itanium multiprocessors, but is impossible without exploiting these dependencies. Keywords: Multiprocessor Memory consistency, register and control dependency, Itanium, process coordination.
- ItemOpen AccessProgrammer-Centric Conditions for Itanium Memory Consistency(2006-08-17) Higham, Lisa; Jackson, LillAnne; Kawash, JalalA 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.
- ItemOpen AccessSpecifying Memory Consistency of Write Buffer Multiprocessors(2004-08-17) Higham, Lisa; Jackson, LillAnne; Kawash, JalalWrite buffering is one of many successful mechanisms that improves the performance and scalability of multiprocessors. However, it leads to more complex memory system behavior, which cannot be described using intuitive consistency models, such as sequential consistency. It is crucial to provide programmers with a specification of the exact behavior of such complex memories. This paper presents a uniform framework for describing systems at different levels of abstraction and proving their equivalence. The framework is used to derive and prove correct specification in terms of program-level instruction of the SPARC total store order and partial store order memories.
The framework is also used to examine the SPARC relaxed memory order. We show that it is not a memory consistency model that corresponds to any implementation on a multiprocessor that uses write-buffers, even though we suspect that the SPARC Version 9 specification of relaxed memory order was intended to capture a general write-buffer architecture. The same techniques can be used to show that coherence does not correspond to a write-buffer architecture. A corollary is that any implementation of Alpha consistency using write-buffers cannot produce all possible Alpha computations. That is, there are some computations that satisfy the Alpha specification but cannot occur in the given write-buffer implementation.