Have just released the paper "Concurrent Constraint-based Memory
Machines: A framework for Java Memory Models" on my website
The basic idea behind the paper is to describe an abstract machine,
somewhat in the style of the original JLS spec, but substantially
simplified by the use of constraints and the focus on completing a
concurrent set of events in one transition. This allows all the
causality problems this list has been looking at to be posed as simple
constraint problems which can be solved by known techniques. Indeed Bart
Demoen and Tom Schrijvers are developing an implementation of CCMs using
Constraint Handling Rules on top of SWI Prolog so that all possible
behaviors of "small" programs can be automatically generated. I hope to
see an announcement shortly.
I am releasing the paper early, and a bit reluctantly, because of the
timeline pressure on the JMM JSR work. In particular, the theoretical
development of this approach is just starting. e.g. I think it should be
fairly easy to develop a denotational semantics for shared memory
concurrency in which parallel composition is viewed as set intersection,
in the style of the POPL91 CCP semantics paper. Similarly, proof
systems for the language (e.g. establishing inequivalences for program
substitutability) need to be developed. The approach described here
should also generalize to give a semantic account to other kinds of
concurrent systems -- this should be investigated.
Additionally, there is more work to do, e.g. in understanding the
relationship with the Manson/Pugh and Adve approaches, developing
programs that distinguish between HB and LC etc etc.
Any case, would much appreciate comments and feedback on this paper.
Please feel free to send me comments directly, or to this list if you
think they are of more general interest.
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:59 EDT