Multithreaded programming is difficult and error prone. Multithreaded programs typically synchronize operations on shared mutable data to ensure that the operations execute

Chandrasekhar Boyapati CHANDRA@LCS.MIT.EDU Robert Lee RHLEE@LCS.MIT.EDU Martin Rinard RINARD@LCS.MIT.EDU MIT Laboratory for Computer Science,200Technology Square,Cambridge MA,02139USA

1.Introduction

Multithreaded programming is difficult and error prone. Multithreaded programs typically synchronize operations on shared mutable data to ensure that the operations exe-cute atomically.Failure to correctly synchronize such op-erations can lead to data races or deadlocks.A data race occurs when two threads concurrently access the same data without synchronization,and at least one of the accesses is a write.A deadlock occurs when there is a cycle of the form:,Thread holds Lock and Thread is waiting for Lock.

This paper presents a new static type system for multi-threaded programs;well-typed programs in our system are guaranteed to be free of data races and deadlocks.In recent previous work,we presented a static type system to prevent data races.In this paper,we extend the race-free type sys-tem to prevent both data races and deadlocks.The basic idea behind our system is as follows.When programmers write multithreaded programs,they already have a lock-ing discipline in mind.Our system allows programmers to specify this locking discipline in their programs.The resulting specifications take the form of type declarations. To prevent data races,programmers associate every object with a protection mechanism that ensures that accesses to the object never create data races.The protection mecha-nism of an object can specify either the mutual exclusion lock that protects the object from unsynchronized concur-rent accesses,or that threads can safely access the object without synchronization because either1)the object is im-mutable,2)the object is accessible to a single thread,or 3)the variable contains the unique pointer to the object. Unique pointers are useful to support object migration be-tween threads.The type checker statically verifies that a program uses objects only in accordance with their de-clared protection mechanisms.

To prevent deadlocks,programmers partition all the locks into afixed number of lock levels and specify a partial order among the lock levels.The type checker statically verifies that whenever a thread holds more than one lock,the thread acquires the locks in the descending order.Our system also allows programmers to use recursive tree-based data struc-tures to further order the locks that belong to the same lock level.For example,programmers can specify that nodes in a tree must be locked in the tree-order.Our system allows mutations to the data structure that change the partial order at runtime.The type checker uses an intra-procedural intra-loopflow-sensitive analysis to statically verify that the mu-tations do not introduce cycles in the partial order,and that the changing of the partial order does not lead to deadlocks. Although our type system is explicitly typed in principle,it would be onerous to fully annotate every method with the extra type information that our system requires.Instead, we use a combination of intra-procedural type inference and well-chosen defaults to significantly reduce the num-ber of annotations needed in practice.Our approach per-mits separate compilation.We have a prototype implemen-tation of our type system that handles all the features of the Java language.We also modified several multithreaded Java programs and implemented them in our system.These programs exhibit a variety of sharing patterns.Our expe-rience shows that our system is sufficiently expressive and requires little programming overhead.

2.The Type System

This section introduces our type system with two examples. Figure1presents an example program that has an Account class and a CombinedAccount class.To prevent data races,programmers associate every object with a protec-tion mechanism.In the example,the CombinedAccount class is declared to be immutable.A CombinedAccount may not be modified after initialization.The Account class is generic—different Account objects may have dif-ferent protection mechanisms.The CombinedAccount class contains two Accountfields—savingsAccount and checkingAccount.The key word self indicates that these two Account objects are protected by their own locks.The type checker statically ensures that a thread holds the locks on these Account objects before accessing the Account objects.