Transactional Memory (TM) is on its way to becoming the programming API of choice for writing correct, concurrent, and scalable programs. Hardware TM (HTM) implementations are expected to be significantly faster than pure software TM (STM); however, full hardware support for true closed and open nested transactions is unlikely to be practical.

We present a novel framework for defining memory models in terms of two properties: thread-local Instruction Reordering axioms and Store Atomicity, which describes inter-thread communication via memory. Most memory models have the store atomicity property, and it is this property that is enforced by cache coherence protocols. A memory model with Store Atomicity is serializable; there is a unique global interleaving of all operations which respects the reordering rules. Our framework uses partially ordered execution graphs; one graph represents many instruction interleavings with identical behaviors. The major contribution of this framework is a procedure for enumerating program behaviors in any memory model with Store Atomicity. Using this framework, we show that address aliasing speculation introduces new program behaviors; we argue that these new behaviors should be permitted by the memory model specification. We also show how to extend our model to capture the behavior of non-atomic memory models such as SPARC R TSO.

Programs that manipulate physical quantities typically represent these quantities as raw numbers corresponding to the quantities' measurements in particular units (e.g., a length represented as a number of meters). This approach eliminates the possibility of catching errors resulting from adding or comparing quantities expressed in different units (as in the Mars Climate Orbiter error [11]), and does not support the safe comparison and addition of quantities of the same dimension. We show how to formulate dimensions and units as classes in a nominally typed object-oriented language through the use of statically typed metaclasses. Our formulation allows both parametric and inheritance poly-morphism with respect to both dimension and unit types. It also allows for integration of encapsulated measurement systems, dynamic conversion factors, declarations of scales (including nonlinear scales) with defined zeros, and nonconstant exponents on dimension types. We also show how to encapsulate most of the "magic machinery" that handles the algebraic nature of dimensions and units in a single meta-class that allows us to treat select static types as generators of a free abelian group.

The advantages of the Haskell programming language are rooted in its clean equational semantics. Those advantages evaporate as soon as programmers try to write simple iterative computations and discover that their code must be annotated with calls to seq in order to overcome space leaks introduced by lazy evaluation. The Eager Haskell compiler executes Haskell programs eagerly by default, i.e., bindings and function arguments are evaluated before bodies. When resource bounds are exceeded, computation falls back and is restarted lazily. By using a hybrid of eager and lazy evaluation, we preserve the semantics of Haskell and yet permit efficient iteration.

In this paper, we report on our experiences with guaranteeing GC-pointer safety when using unsafe low-level language extensions to implement a JVM in Java. We give an overview of the original unsafe language extensions that were defined for use by Jalapeño implementers, and introduce sanitized replacements that capture common idioms while also guaranteeing GC-pointer safety. We also outline some simple static and dynamic checks for correct usage of low-level operations, and examine how code containing low-level operations can be optimized correctly and effectively.

This paper describes alternative memory semantics for Java programs using an enriched version of the Commit/Reconcile/Fence (CRF) memory model [16]. It outlines a set of reasonable practices for safe multithreaded programming in Java. Our semantics allow a number of optimizations such as load reordering that are currently prohibited. Simple thread-local algebraic rules express the effects of optimizations at the source or bytecode level. The rules focus on reordering source-level operations; they yield a simple dependency analysis algorithm for Java. An instruction-by-instruction translation of Java memory operations into CRF operations captures thread interactions precisely. The fine-grained synchronization of CRF means the algebraic rules are easily derived from the translation. CRF can be mapped directly to a modern architecture, and is thus a suitable target for optimizing memory coherence during code generation.