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 de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.290-304, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00525183
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : lundi 11 octobre 2010 - 13:13:07
Dernière modification le : lundi 11 octobre 2010 - 13:13:07

Identifiants

  • HAL Id : inria-00525183, version 1

Collections

Citation

Thi Mai Thuong Tran, Martin Steffen. Safe Commits for Transactional Featherweight Java. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.290-304, 2010, Lecture Notes in Computer Science. 〈inria-00525183〉

Partager

Métriques

Consultations de la notice

132