Dashboard

Now you are in the subtree of Misc public knowledge tree. 

Formalising and Optimising Parallel Snapshot Isolation (TR4ICDCS'2015)

Paper Summary

This paper investigate Parallel Snapshot Isolation (PSI) which is a weaker consistency condition than the classical Snapshot Isolation (SI).

In the original paper, PSI is defined in a low-level, operational way. The specification of PSI is given as an idealized, centralized algorithm, which involves lots of implementation details, such as replicas and messages.

The specification of PSI presented in this paper has two key features:

  1. It is axiomatic in that it is implementation-independent and abstracts from replicas and messages;
  2. It does not explicitly rely on the concept of snapshot points.

The resulting axiomatic specification of PSI is quite neat and easy-to-understand.

Under their axiomatic specification of PSI, the authors also determine conditions under which transactions running on PSI can be chopped into smaller pieces without introducing new behaviours.

My Reflections

In the email to the authors, I mentioned two questions/ideas.

  1. PSI allows the long-fork anomaly. I guess the long-fork anomaly is related to both the global constraint of G-SIb* cycle in RSI [1] [Lemma 3.5, Page 14] and the MON condition in NMSI [2]. If so, I think it is not difficult to express it under your formalism. I will try this.
  2. Inspired by your axiomatic formalism, especially by the (Atomic) axiom in it, I came up a "layered" perspective of an axiomatic formalism: In the low-layer, we only have individual read/write operations. In this layer, we already have lots of literature in the community of the shared-memory models [3] [4]. In particular, we can borrow its GWO, GDO, and GAO axioms from [4; Figure 13]. In the high-layer, we treat a transaction consisting of multiple read/write operations as a whole object. The high-layer perspective is necessary for isolation conditions such as SI and SR (serializability). In this way, your (Atomic) axiom plays an important role: it lifts the low-layer to the high-layer. I am not sure whether this layered formalism is worth exploring.
  • [1] Snapshot Isolation and Integrity Constraints in Replicated Databases. (Yi Lin et al@TODS'2009)
  • [2] Non-Monotonic Snapshot Isolation. (Masoud Saeida et al@arXiv'2013)
  • [3] A formal hierarchy of weak memory models. (Jade Alglave@FMSD'2012)
  • [4] A unified theory of shared memory consistency. (ROBERT C. STEINKE AND GARY J. NUTT@JACM'2004)