Safe Concurrent Programming in Java

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 dif?cult 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 speci?cations 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 veri?es that a program uses objects only in accordance with their de-clared protection mechanisms.

To prevent deadlocks,programmers partition all the locks into a?xed number of lock levels and specify a partial order among the lock levels.The type checker statically veri?es 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-loop?ow-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 signi?cantly 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 modi?ed 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 suf?ciently 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 modi?ed after initialization.The Account class is generic—different Account objects may have dif-ferent protection mechanisms.The CombinedAccount class contains two Account?elds—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.

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

1class Account {2int balance =0;

34int balance()accesses (this){return balance;}5void deposit(int x)accesses (this){balance +=x;}6void withdraw(int x)accesses (this){balance -=x;}7}89class CombinedAccount<readonly>{10LockLevel savingsLevel =new;11LockLevel checkingLevel <savingsLevel;12final Account<self:savingsLevel>savingsAccount 13=new Account;14final Account<self:checkingLevel>checkingAccount 15=new Account;1617void transfer(int x)locks(savingsLevel){18synchronized (savingsAccount){19synchronized (checkingAccount){20savingsAccount.withdraw(x);21checkingAccount.deposit(x);22}}}23int creditCheck()locks(savingsLevel){24synchronized (savingsAccount){25synchronized (checkingAccount){26return savingsAccount.balance()+27checkingAccount.balance();28}}}29 (30)

}Figure bined Account Example To prevent deadlocks,programmers associate every lock in our system with a lock level.In the example,the CombinedAccount class declares two lock levels—savingsLevel and checkingLevel .Lock levels are purely compile-time entities—they are not preserved at runtime.In the example,checkingLevel is declared to rank lower than savingsLevel in the partial order of lock levels.The checkingAccount belongs to checkingLevel ,while the savingsAccount belongs to savingsLevel .The type checker statically ensures that threads acquire these locks in the descending order of lock levels.

Methods in our system may contain accesses clauses to specify assumptions that hold at method boundaries.The methods of the Account class each have an accesses clause that speci?es that the methods access the this Ac-count object without synchronization.To prevent data races,our type checker requires that the callers of an Ac-count method must hold the lock that protects the corre-sponding Account object before the callers can invoke the Account method.

Methods in our system may also contain locks clauses.The methods of the CombinedAccount class contain a locks clause to indicate to callers that they may acquire locks that belong to lock levels savingsLevel or lower.To prevent deadlocks,the type checker statically ensures that callers of CombinedAccount methods only hold locks that are of greater lock levels than savingsLevel .

Figure 2presents part of a BalancedTree implemented in our type system.A BalancedTree is a tree of Nodes .Ev-

1class BalancedTree {

2LockLevel l =new;

3

Node<self:l>root =new Node;4}

56class Node<self:v>{

7

tree Node<self:v>left;8

tree Node<self:v>right;910//this this

11///\/\12//...x (v)

13///\-->

/\14//v y u x

15

///\/\16

//u w

w y

1718synchronized void rotateRight()locks(this){

19final Node x =this.right;if (x ==null)return;20synchronized (x){

21

final Node v =x.left;if (v ==null)return;22synchronized (v){

23final Node w =v.right;24v.right =null;25x.left =w;

26

this.right =v;27

v.right =x;

28}}}29 (30)

}

Figure 2.Tree Example

ery Node object is declared to be protected by its own lock.To prevent data races,the type checker statically ensures that a thread holds the lock on a Node object before ac-cessing the Node object.The Node class is parameterized by the formal lock level v .The Node class has two Node ?elds—left and a right .The Nodes left and right also be-long to the same lock level v .

Our system also allows programmers to use recursive tree-based data structures to further order the locks that belong to the same lock level.In the example,the key word tree indicates that the Nodes left and right are ordered lower than the this Node object in the partial order.To prevent deadlocks,the type checker statically veri?es that the rota-teRight method acquires the locks on Nodes this ,x and v in the tree-order.The rotateRight method in the example performs a standard rotation operation on the tree to restore the tree balance.The type checker uses an intra-procedural intra-loop ?ow-sensitive analysis to statically verify that the changing of the partial order does not lead to deadlocks.Our type system statically veri?es the absence of both data races and deadlocks in the above examples.More de-tails about the type system will appear in (Boyapati et al.,November 2002).

References

Boyapati,C.,Lee,R.,&Rinard,M.(November 2002).Ownership types for safe programming:Preventing data races and deadlocks.Object-Oriented Programming,Systems,Languages,and Applications (OOPSLA).

本文来源：https://www.bwwdw.com/article/teem.html