Coqa and Task Types

Coqa is a new concurrent programming language where atomicity is inherent in an organic fashion. It takes the view that atomicity holds for whole threads by default, and a division into smaller atomic regions occurs only at points where an explicit need for sharing is needed and declared. A corollary of this view is every line of code is part of some atomic region. Task Types are a polymorphic type system for Coqa, enforcing most of the desired atomicity properties statically.

Task Types

Here is the paper: Task Types for Pervasive Atomicity (OOPSLA'10). This technical report includes an informal discussion of the type system, the formal type system, the operational semantics, meta-theories and proofs for them, and a rigorous definition of pervasive atomicity. Here are the slides used for the conference presentation.

Background

Task Types are developed on top of the Coqa language, which was first described in a CC'08 Paper. One terminology difference to note is that in the CC paper, we used term subtask to refer to what is named shared task in the Task Types paper. The invocation symbol previously used for such objects was =>, and now it is .->.

Without a static type system, the CC'08 paper treats every object with dynamic monitoring (modulo an ad hoc static analysis to remove obviously unnecessary locks). So from the perspective of Task Types, all classes in the CC'08 paper can be viewed as declared as shared, i.e. their instances are shared ordinary objects that require dynamic lock protection.

The Compiler

The compiler source code can be downloaded here. Here are some instructions for installing and building the compiler: Follow the following instructions to use the compiler to compile programs. First of all, all Task Types programs should have a suffix of .con.

Errata

None Yet. Please let us know!

      Photo Source: CDC.gov

free web stats