A transaction defines a locus of computation that satisfies important concurrency and failure properties. These so-called ACID properties provide strong serialization guarantees that allow us to reason about concurrent and distributed programs in terms of higher-level units of computation (e.g., transactions) rather than lower-level data structures (e.g., mutual-exclusion locks). This paper presents a framework for specifying the semantics of a transactional facility integrated within a host programming language. The TFJ calculus, an object calculus derived from Featherweight Java, supports nested and multi-threaded transactions. We give a semantics to TFJ that is parametrized by the definition of the transactional mechanism that permits the study of different transaction models. We give two instantiations: one that defines transactions in terms of a versioning-based optimistic concurrency model, and the other which specifies transactions in terms of a pessimistic two-phase locking protocol, and present soundness and serializability properties for our semantics.
@article{Jagannathan+2005SCP,
author = {Jagannathan, Suresh and Vitek, Jan and Welc, Adam and Hosking, Antony},
title = {A Transactional Object Calculus},
journal = {Science of Computer Programming},
year = {2005},
volume = {57},
number = {2},
pages = {164--186},
month = {August},
doi = {10.1016/j.scico.2005.03.001},
gscholar = {56}
}