translating between itanium and sparc memory consistency models
Our general goal is to port programs from one multiprocessor architecture to another, while ensuring that each program's semantics remains unchanged. This paper addresses a subset of the problem by determining the relationships between memory consistency models of three Sparc architectures, (TSO, PSO and RMO) and that of the Itanium architecture. First we consider Itanium programs that are constrained to have only one load-type of instruction in {load, load _acquire}, and one store-type of instruction in {store, store_release}. We prove that in three out of four cases, the set of computations of any such program is exactly the set of computations of the "same" program (using only load and store) on one Sparc architecture. In the remaining case the set is nested between two natural sets of Sparc computations.Real Itanium programs, however, use a mixture of load, load acquire, store, store release and memory fence instructions, and real Sparc programs use a variety of barrier instruction as well as load and store instructions. We next show that any mixture of the loadtypes or the store-types (in the case of Itanium) or any barrier instructions (in the case of Sparc) completely destroys the clean and simple similarities between the sets of computations of these systems. Thus (even without considering the additional complications due to register and control dependencies) transforming these more general programs in either direction requires constraining the transformed program substantially more than the original program in order to ensure that no erroneous computations can arise.
itanium sparc memory consistency models multiprocessors program transformations