Generators and checkers for tests of Adya's proscribed behaviors for weakly-consistent systems. See http://pmg.csail.mit.edu/papers/adya-phd.pdf
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)
Verifies that at most one :insert completes successfully for any given key.
Verifies that at most one :insert completes successfully for any given key.
(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
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.
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 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.
cljdoc is a website building & hosting documentation for Clojure/Script libraries
× close