A Transactional Object Calculus

Jagannathan, Suresh and Vitek, Jan and Welc, Adam and Hosking, Antony


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.

  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}