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 specifies 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 fields—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 verifies 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 flow-sensitive analysis to statically verify that the changing of the partial order does not lead to deadlocks.Our type system statically verifies 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).