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.