A transactional object calculus Export

@article{citeulike:248226, 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, 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}, citeulike-article-id = {248226}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.scico.2005.03.001}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6V17-4G24X8H-1/2/76d1cd6dae0c61b7006a68e9c73380f9}, doi = {10.1016/j.scico.2005.03.001}, journal = {Science of Computer Programming}, keywords = {featherweight-java, object-calculus, transactional}, month = {August}, number = {2}, pages = {164--186}, posted-at = {2007-10-23 19:19:02}, priority = {2}, title = {A transactional object calculus}, url = {http://dx.doi.org/10.1016/j.scico.2005.03.001}, volume = {57}, year = {2005} }

TY - JOUR ID - citeulike:248226 L3 - citeulike-article-id:248226 N2 - 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. IS - 2 JF - Science of Computer Programming EP - 186 TI - A transactional object calculus VL - 57 SP - 164 KW - featherweight-java KW - object-calculus KW - transactional AU - Jagannathan, Suresh AU - Vitek, Jan AU - Welc, Adam AU - Hosking, Antony PY - 2005/08// UR - http://dx.doi.org/10.1016/j.scico.2005.03.001 ER -