jepsen.tests.adya — jepsen 0.1.14

Generators and checkers for tests of Adya's proscribed behaviors for weakly-consistent systems. See http://pmg.csail.mit.edu/papers/adya-phd.pdf

g2-checker clj

(g2-checker)

Verifies that at most one :insert completes successfully for any given key.

g2-gen clj

(g2-gen)

With concurrent, unique keys, emits pairs of :insert ops of the form [key [a-id b-id]], where one txn has a-id and the other has b-id. a-id and b-id are globally unique. Only two insert ops are generated for any given key. Keys and ids are positive integers.

G2 clients use two tables:

create table a (
  id    int primary key,
  key   int,
  value int
);
create table b (
  id    int primary key,
  key   int,
  value int
);

G2 clients take operations like {:f :insert :value [key [a-id nil]]}, and in a single transaction, perform a read of tables a and b like so:

select * from a where key = ? and value % 3 = 0
select * from b where key = ? and value % 3 = 0

and fail if either query returns more than zero rows. If both tables are empty, the client should insert a row like

{:key key :id a-id :value 30}

into table a, if a-id is present. If b-id is present, insert into table b instead. Iff the insert succeeds, return :type :ok with the operation value unchanged.

We're looking to detect violations based on predicates; databases may prevent anti-dependency cycles with individual primary keys, but selects based on predicates might observe stale data. Clients should feel free to choose predicates and values in creative ways.