|
Coqa: Concurrent Objects with Quantized Atomicity
Yu David Liu, Xiaoqi Lu, Scott Smith. Draft
Abstract: This paper introduces a new language
model, Coqa, for deeply embedding concurrent programming into objects. Every
program written in our language has built-in the desirable behaviors of
atomicity, mutual exclusion, and race freedom. Such a design inverts the
default mode of e.g. Java, where programmers may write programs highly
vulnerable to surprising runtime errors if they do not take advantage of
synchronized blocks and other advanced concurrency features. Coqa takes
advantage of basic object-oriented notions to express important concurrent
programming primitives, resulting in a powerful but concise model that
includes thread creation, shared object access and open nesting. A key
property of our model is the notion of quantized atomicity: all concurrent
program executions can be viewed as being divided into quantum regions of
atomic execution, greatly reducing the number of interleavings to consider.
The language design draws from different schools of concurrent language
design, especially Actors, and constructs a unified design close to
mainstream object-oriented programming practice. We justify our approach
both from a theoretical
basis by showing that a formal representation, CoqaKernel, has provable
quantized atomicity properties, and by implementing CoqaJava, a Java
extension incorporating all of the Coqa
features.
Long Version (PDF)
Short Submission Version (PDF)
|