A transactional object calculus

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.