Safe Commits for Transactional Featherweight Java

Abstract. Transactions are a high-level alternative for low-level concurrencycontrol mechanisms such as locks, semaphores, monitors. A recent proposal for integrating transactional features into programming languages is Transactional Featherweight Java (TFJ), extending Featherweight Java by adding transactions. With support for nested and multi-threaded transactions, its transactional model is rather expressive. In particular, the constructs governing transactions —to start and to commit a transaction— can be used freely with a non-lexical scope. On the downside, this flexibility also allows for an incorrect use of these constructs, e.g., trying to perform a commit outside any transaction. To catch those kinds of errors, we introduce a static type and effect system for the safe use of transactions for TFJ. We prove the soundness of our type system by subject reduction.

• Type: Journal
• Year: 2010
• Where: IFM
• Authors: Thi Mai Thuong Tran, Martin Steffen
• Keywords: Featherweight Java, Formal Methods, IFM 2010, Transactional Featherweight Java, Transactions —to Start