Memory Consistency and Process Coordination for SPARC Multiprocessors

Abstract. Simple and unified non-operational specifications of the three memory consistency models Total Store Ordering (TSO), Partial Store Ordering (PSO), and Relaxed Memory Order (RMO) of SPARC multiprocessors are presented and proved correct. The specifications are intuitive partial order constraints on possible computations and are derived from natural successive weakening of Lamport's Sequential Consistency. The formalisms are then used to determine the capabilities of each model to support solutions to critical section coordination and both set and queue variants of producer/consumer coordination without resorting to expensive synchronization primitives. Our results show that none of RMO, PSO nor TSO is capable of supporting a read/write solution to the critical section problem, but each can support such a solution to some variants of the producer/consumer problem. These results contrast with the two previous attempts to specify these machines, one of which would incorrectl...

• Type: Conference
• Year: 2000
• Where: HIPC
• Authors: Lisa Higham, Jalal Kawash
• Keywords: Critical Section, Critical Section Problem, Distributed And Parallel Computing, HIPC 2000, Memory Consistency Models