This paper introduces a new language model, Coqa, for deeply embedding concurrent programming into objects. Every program written in our language has the desirable behaviors of atomicity, mutual exclusion, and race freedom automatically built in. A key property of our model is the notion of quantized atomicity: every concurrent program execution can be viewed as being divided into quantum regions of atomic execution, greatly reducing the number of interleavings to consider. Rather than building atomicity locally, i.e. declaring some code blocks as atomic blocks and leaving other code segments with no guarantee of any atomicity property, we build it in globally, so that a form of atomicity, quantized atomicity, ubiquitously exists at all program points. We justify our approach both from a theoretical basis by showing that a formal representation, Kernel-Coqa, has provable quantized atomicity properties, and by implementing CoqaJava, a Java extension incorporating all of the Coqa features.
展开▼
