Concurrent Constraint-based Memory Machines: A framework for Java Memory Models

(Draft Preliminary Report, v 0.6)

Vijay Saraswat

IBM TJ Watson Research Center

March 9, 2004

Abstract

A central problem in extending the von Neumann architecture to petaflop computers with millions of hardware threads and with a shared memory is defining the memory model. Such a model must specify the behavior of concurrent (conditional) reads and writes to the same memory locations. We present a simple, general framework for the specification of memory models based on an abstract machine that uses sets of (interdependent) order and value constraints to communicate between threads and main memory. The separation of order constraints allows a parametric treatment of different order consistency models such as sequential consistency, location consistency, happens-before consistency (HB-consistency), etc. The use of value constraints allows a simple formulation of the semantics of concurrent dependent reads and writes in the presence of look-ahead and speculative computation. Memory is permitted to specify exactly those linkings (mappings from read events to write events) which result in a unique solution for the constraints, and hence forces a unique patterns of bits to flow from write events to read events.

We show that this single principle accounts for almost all the ``causality test cases'' proposed for the Java memory model. To fix ideas, we present a structural operational semantics for a language using the HB order model. This operational semantics may be extended to develop a memory model for the Java programming language.

Keywords: Java, Memory models, Memory Consistency Models, Sequential Consistency, Location Consistency, Happens Before Consistency, Abstract Machines, Semantics of Concurrency, constraint-based programming, specification, concurrent constraint programming. 

@techreport{ccm-machines
  title =        {Concurrent {C}onstraint-based {M}emory {M}achines: 
                  A framework for {Java} {M}emory {M}odels},
  author =       {Vijay Saraswat},
  institution= {IBM {TJ} {W}atson {R}esearch {C}enter},
  month =        mar,
  year =         "2004"
}
Pdf file (512K), 74 pp