Elle is a transactional consistency checker for black-box databases. Based purely on client observations of transactions, and given some minimal constraints on datatypes and operations, it can tell you whether that observation exhibits a variety of transactional anomalies. Like a clever lawyer, Elle looks for a sequence of events in a story which couldn't possibly have happened in that order, and uses that inference to prove the story can't be consistent.

In a nutshell, Elle is:

• General: Elle works over a variety of datatypes and places only minimal, practical constraints on transaction structure.
• Efficient: Elle is ~linear in history length, and ~constant, rather than exponential, with respect to concurrency.
• Effective: Elle has found unexpected anomalies in every database we've checked, ranging from internal consistency violations to anti-dependency cycles to dirty read to lost updates to realtime violations.
• Sound: Elle can find every (non-predicate) anomaly from Adya, Liskov, & O'Neil's Generalized Isolation Level Definitions.
• Elucidative: Elle can point to a minimal set of transactions which witness a consistency violation; its conclusions are easy to understand and verify.

This repository encompasses a Clojure implementation of the Elle consistency checker and its accompanying test suite, which you can use to check your own histories. Our paper provides deep insight into the goals and intuition behind Elle, and a rough formalization of its soundness proof. A nowhere-near-complete formal proof sketch is written in the Isabelle/HOL proof language.

If you want to check a database using Elle, see Jepsen; Elle comes built-in. If you want to use Elle to check your own histories without using Jepsen, you can add Elle as a dependency to any JVM project, and invoke its checker functions directly. If you're working in a non-JVM language, you can write your history to a file or stream, and call a small wrapper program to produce output.

Elle is still under active development, and we're not 100% confident in its inference rules yet. Jepsen recommends checking reported anomalies by hand to make sure they're valid. If you'd like to contribute, we'd especially welcome your help in the formal proof, and in rigorously defining consistency models.

Questions? Read the paper!

First, you'll need a copy of Graphviz installed.

Imagine a database where each object (identified by keys like :x or :y) is a list of numbers. Transactions are made up of reads [:r :x [1 2 3]], which return the current value of the given list, and writes [:append :y 4], which append a number to the end of the list.

=> (require '[elle.list-append :as a]
            '[jepsen.history :as h])
nil

We construct a history of three transactions, each of which is known to have committed (:type :ok). The first transaction appends 1 to :x and observes :y = [1]. The second appends 2 to :x and 1 to :y. The third observes x, and sees its value as [1 2].

=> (def h (h/history
            [{:process 0, :type :ok, :value [[:append :x 1] [:r :y [1]]]}
             {:process 1, :type :ok, :value [[:append :x 2] [:append :y 1]]}
             {:process 2, :type :ok, :value [[:r :x [1 2]]]}]))
h

Now, we ask Elle to check this history, expecting it to be serializable, and have it dump anomalies to a directory called out/.

=> (pprint (a/check {:consistency-models [:serializable], :directory "out"} h))
{:valid? false,
 :anomaly-types (:G1c),
 :anomalies
 {:G1c
  [{:cycle
    [{:process 1,
      :type :ok,
      :f nil,
      :value [[:append :x 2] [:append :y 1]],
      :index 1,
      :time -1}
     {:process 0,
      :type :ok,
      :f nil,
      :value [[:append :x 1] [:r :y [1]]],
      :index 0,
      :time -1}
     {:process 1,
      :type :ok,
      :f nil,
      :value [[:append :x 2] [:append :y 1]],
      :index 1,
      :time -1}],
    :steps
    ({:type :wr, :key :y, :value 1, :a-mop-index 1, :b-mop-index 1}
     {:type :ww,
      :key :x,
      :value 1,
      :value' 2,
      :a-mop-index 0,
      :b-mop-index 0}),
    :type :G1c}]},
 :not #{:read-committed},
 :also-not
 #{:consistent-view :cursor-stability :forward-consistent-view
   :monotonic-atomic-view :monotonic-snapshot-read :monotonic-view
   :repeatable-read :serializable :snapshot-isolation :strong-serializable
   :strong-session-serializable :strong-session-snapshot-isolation
   :strong-snapshot-isolation :update-serializable}}

Here, Elle can infer the write-read relationship between T1 and T2 on the basis of their respective reads and writes. The write-write relationship between T2 and T1 is inferrable because T3 observed x = [1,2], which constrains the possible orders of appends. This is a G1c anomaly: cyclic information flow. The :cycle field shows the operations in that cycle, and :steps shows the dependencies between each pair of operations in the cycle.

On the basis of this anomaly, Elle has concluded that this history is not read-committed---this is the weakest level Elle can demonstrate is violated. In addition, several stronger isolation levels, such as consistent-view and update-serializable, are also violated by this history.

Let's see the G1c anomaly in text:

$ cat out/G1c.txt
G1c #0
Let:
  T1 = {:index 1, :time -1, :type :ok, :process 1, :f nil,
        :value [[:append :x 2] [:append :y 1]]}
  T2 = {:index 0, :time -1, :type :ok, :process 0, :f nil,
        :value [[:append :x 1] [:r :y [1]]]}


Then:
  - T1 < T2, because T2 observed T1's append of 1 to key :y.
  - However, T2 < T1, because T1 appended 2 after T2 appended 1 to :x: a contradiction!

In the out/G1c directory, you'll find a corresponding plot.

In addition to rendering a graph for each individual cycle, Elle generates a plot for each strongly-connected component of the dependency graph. This can be helpful for getting a handle on the scope of an anomalous behavior, whereas cycles show as small a set of transactions as possible. Here's a plot from a more complex history, involving realtime edges, write-write, write-read, and read-write dependencies:

As a user, your main entry points into Elle will be elle.list-append/check and elle.rw-register/check. Both namespaces also have code for generating sequences of transactions which you can apply to your database; see, for example, elle.list-append/gen.

Elle has a broad variety of anomalies and consistency models; see elle.consistency-model for their definitions. Not every anomaly is detectable, but we aim for completeness.

If you'd like to define your own relationships between transactions, see elle.core.