Safe Typing for Transactional vs. Lock-Based Concurrency in Multi-threaded Java

Many concurrency models have been developed for high-level programming languages such as Java. A trend here is towards more flexible concurrency control protocols, going beyond the original Java multi-threading treatment based on lexically-scoped concurrency control mechanism. Two proposals supporting flexible, non-lexical concurrency control are the lock-handling via the Lock-classes in Java5 and Transactional Featherweight Java (TFJ), an extension of Featherweight Java by transactions. Even if these two take quite different approaches towards dealing with concurrency - “pessimistic” or lock-based vs. “optimistic” or based on transactions - the added flexibility of non-lexical use of the corresponding concurrency operators comes at a similar price: improper usage leads to run-time exceptions and unwanted behavior. This is in contrast with the more disciplined use under a lexically scoped regime, where each entrance to a critical region is syntactically accompanied by a corresponding exit (as e.g. with traditional synchronized methods or as with so-called atomic blocks). To assure safe use of locking, resp. transactions in these settings, we present in this paper abstractions in the form of two static type and effect systems, which make sure that for instance, no lock is released by a thread which does not hold it, resp., that no commit is executed outside any transaction. We furthermore compare the two mentioned approaches to concurrency control on the basis of these type abstractions.