In A Critique of Snapshot Isolation, published in EuroSys 2012, they present write-snapshot isolation, a simple but clever approach to making snapshot isolation serializable. This work was published a few years after Michael Cahill’s original work on Serializable Snapshot Isolation (TODS 2009), and around a similar time as the work of Dan Ports on implementing serializable snapshot isolation (VLDB 2012), which applied Cahill’s ideas in PostgreSQL.| William Schultz
Database transactions are traditionally modeled as a sequence of read/write operations on a set of keys, where each read operation returns some value and each write sets a key to some value. This is reflected in most of the formalisms that define various transactional isolation semantics (Adya, Crooks, etc.).| William Schultz
There have been many attempts to formalize the zoo of various transaction isolation and consistency concepts over the years. It is not always clear, though, to what extent these attempts have clarified things, especially when each approach has introduced new variations of complexity and formal notation. The rise of distributed storage and database systems and the need to reason about isolation in these contexts has likely worsened the situation.| William Schultz
Formal specifications havebecomea core part of rigorous distributed systems design and verification, but existing tools have still been lacking in providing good interfaces for interacting with, exploring, visualizing and sharing these specifications and models in a portable and effective manner. The TLA+ Web Explorer aims to address this shortcoming by providing a browser-based tool for exploring and visualizing formal specifications written in TLA+. It takes inspiration from past attempts a...| William Schultz
My personal website.| William Schultz
If we want to formally prove that a system satisfies some safety property (i.e. an invariant), we can do this by finding an inductive invariant. An inductive invariant is a particular type of invariant that is at least as strong as the target invariant to be proven, and is also inductive, meaning that it is closed under all transitions of the system.| William Schultz
Below is a high level overview of the Raft reconfiguration bug cases laid out in Diego Ongaro’s group post, which described the problematic scenarios in Raft’s single server reconfiguration (i.e. membership change) algorithm. Configurations are annotated with their terms i.e., a config \(X\) in term \(t\) is shown as \(X^t\). One add, one remove Two adds Two removes I view all of these bug cases as instances of a common problem related to config management when logs diverge (i.e., when th...| William Schultz
In practice we specify a system’s behavior as the conjunction of a safety and liveness property \(S \wedge L\). The safety-liveness decomposition is fundamental, as shown by Alpern and Schneider. Describing a system as a conjunction of arbitrary safety and liveness properties, however, can be dangerous. Motivation Imagine we have a rectangular, two dimensional grid system, with an agent that starts at the bottom left of this rectangle i.e. at point \((0,0)\). The top right corner of the rec...| William Schultz
Temporal logic properties can be broadly categorized into safety and liveness properties. Informally, safety properties state that a “bad thing” never happens whereas liveness properties state that a “good thing” must eventually happen. These informal definitions are made precise in the paper Defining Liveness (Alpern, Schneider, 1985), and are also discussed in a later paper, Decomposing Properties into Safety and Liveness using Predicate Logic (Schneider, 1987). Formalizing Safety a...| William Schultz
Temporal logic, which TLA+ is based on, provides a way to describe properties about behaviors, where a behavior is an infinite sequence of states. We could call these temporal properties or, more simply, properties. You can classify certain properties as safety or liveness properties, but those are just categorizations within the general space of properties you might care about. Roughly, a safety property is one that is violated by a finite behavior (a behavior prefix), and a liveness propert...| William Schultz