jepsen.tests.adya
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
(g2-checker)
Verifies that at most one :insert completes successfully for any given key.
g2-gen
(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.