Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Monday, October 11, 2010 - 1:13:07 PM
Last modification on : Tuesday, February 18, 2020 - 2:11:07 PM


  • HAL Id : inria-00525183, version 1



Thi Mai Thuong Tran, Martin Steffen. Safe Commits for Transactional Featherweight Java. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.290-304. ⟨inria-00525183⟩



Record views