Computing Publications

Publications Home » Universe Types for Race Safety

Universe Types for Race Safety

David Cunningham, Sophia Drossopoulou, Susan Eisenbach

Conference or Workshop Paper
September, 2007

Race conditions occur when two incorrectly synchronised threads simultaneously access the same object. Static type systems have been suggested to prevent them. Typically, they use annotations to determine the relationship between an object and its ``guard'' (another object), and to guarantee that the guard has been locked before the object is accessed. The object-guard relationship thus forms a tree similar to an ownership type hierarchy.

Universe types are a simple form of ownership types. We explore the use of universe types for static identification of race conditions. We use a small, Java-like language with universe types and concurrency primitives. We give a type system that enforces synchronisation for all object accesses, and prove that race conditions cannot occur during execution of a type correct program.

We support references to objects whose ownership domain is unknown. Unlike previous work, we do so without compromising the synchronisation strategy used where the ownership domain of such objects is fully known. We develop a novel technique for dealing with non-final paths to objects of unknown ownership domain using effects.

Language Design
Distributed Software Engineering
PDF of full publication (340 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.