Coqa: Concurrent Objects with Quantized Atomicity

Abstract

A primary problem in programming todays multi-core machines is reliable debugging: with large numbers of concurrent threads executing there are a huge number of interleavings to consider, and many potential interleavings will be missed in program testing. This talk describes a new language model, Coqa, for reliable multi-core programming. A key property of Coqa is the notion of quantized atomicity: every concurrent program execution is divided into quantum regions of atomic execution, greatly reducing the number of logical interleavings that must be considered in debugging. Rather than building atomicity locally, with small declared zones, we build it globally, down from the top. We justify our approach both from a theoretical basis by showing that a formal representation, KernelCoqa, has provable atomicity properties, and by implementing CoqaJava, a Java extension incorporating Coqa features.

This is joint work with Yu David Liu and Xiaoqi Lu