Determinate Imperative Programming: A clocked interpretation of imperative syntax

Vijay Saraswat, IBM TJ Watson Research Center
Radha Jagadeesan, De Paul University
Armando Solar-lezama, UC Berkeley
Christoph von Praun, IBM TJ Watson Research Center
July 17, 2005

Submitted for publication.


There are a large class of applications, notably those in high-performance computation (HPC), for which parallelism is necessary for performance, not expressiveness. Such applications are typically determinate and have no natural notion of deadlock. Unfortunately, today's dominant HPC programming paradigms (MPI and OpenMP) are based on imperative concurrency and do not guarantee determinacy or deadlock-freedom. This substantially complicates writing and debugging such code.

We present a new concurrent model for mutable variables, the clocked final model, CF, that guarantees determinacy and deadlock-freedom. CF views a mutable location as a monotonic stream together with a global stability rule which permits reads to stutter (return a previous value) if it can be established that no other activity can write in the current phase. Each activity maintains a local index into the stream and advances it independently as it performs reads and writes. Computation is aborted if two different activities write different values in the same phase.

This design unifies and extends several well-known determinate programming paradigms: single-threaded imperative programs, the ``safe asynchrony'' of [Steele90], reader-writer communication via immutable variables, Kahn networks, and barrier-based synchronization. Since it is predicated quite narrowly on a re-analysis of mutable variables, it is applicable to existing sequential and concurrent languages, such as Jade, Cilk, Java and X10. We present a formal operational model for a specific CF language, MJ/CF, based on the MJ calculus of [Parkinson03]. We present an outline of a denotational semantics based on a connection with default concurrent constraint programming. We show that CF leads to a very natural programming style: often an ``obvious'' shared-variable formulation provides the correct solution under the CF interpretation. We present several examples and discuss implementation issues.


Slides from a talk at MIT 10/07/2005

Back to Main page