A Semantic Framework for Designer Transactions

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

Abstract

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 supports nested and multi-threaded transactions. We give a semantics to TFJ that is parameterized by the definition of the transactional mechanism that permits the study of different transaction models.

@inproceedings{Vitek+2004ESOP,
  author = {Vitek, Jan and Jagannathan, Suresh and Welc, Adam and Hosking, Antony L.},
  title = {A Semantic Framework for Designer Transactions},
  booktitle = {European Symposium on Programming},
  series = {ESOP},
  year = {2004},
  pages = {249--263},
  month = {March},
  address = {Barcelona, Spain},
  doi = {10.1007/b96702},
  gscholar = {40}
}