Advertisement
Published in:
2010 | OriginalPaper | Chapter
Safe Commits for Transactional Featherweight Java
Authors : Thi Mai Thuong Tran, Martin Steffen
Published in: Integrated Formal Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Transactions are a high-level alternative for low-level concurrency-control 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.