tarantool / jepsen.tarantool

Jepsen tests for Tarantool
https://www.tarantool.io/en/
Other
7 stars 0 forks source link

Add test with checks for anomalies described in Adya's PhD #56

Closed ligurio closed 3 years ago

ligurio commented 4 years ago

Adya’s formalization of transactional isolation levels provides a more thorough summary of the preventative interpretation of the ANSI levels, defining serializability as the absence of four phenomena. Serializability prohibits:

P0 (Dirty Write): w1(x) … w2(x)
P1 (Dirty Read): w1(x) … r2(x)
P2 (Fuzzy Read): r1(x) … w2(x)
P3 (Phantom): r1(P) … w2(y in P)

Here w denotes a write, r denotes a read, and subscripts indicate the transaction which executed that operation. The notation “…” indicates a series of micro-operations except for a commit or abort. P indicates a predicate.

As Adya notes, the preventative interpretation of the ANSI specification is overly restrictive: it rules out some histories which are legally serializable.

ligurio commented 3 years ago

Duplicate of #8