Safe Commits for Transactional Featherweight Java - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Safe Commits for Transactional Featherweight Java

Thi Mai Thuong Tran
  • Fonction : Auteur
  • PersonId : 880463
Martin Steffen
  • Fonction : Auteur
  • PersonId : 880464

Résumé

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.
Fichier non déposé

Dates et versions

inria-00525183 , version 1 (11-10-2010)

Identifiants

  • HAL Id : inria-00525183 , version 1

Citer

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⟩
69 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More