Circular information flow test misses transitive cycles #7
Description
From the paper,
Informally, a Circular Information Flow (Adya’s G1c) anomaly occurs when two transactions affect each other; i.e. both transactions write information the other reads. For example, transaction Ti reads a write by transaction Tj and transaction Tj reads a write by Ti.
The current test works by concurrently executing transactions that (i) set version of some person1 to the (unique) transaction id, then (ii) reads version of some person2; person1 != person2. Returning the tuple (transaction id, version read).
For each pair of tuples an anomaly has occurred if (transaction id 1, version read = 2) and (transaction id 2, version read = 1). I.e., there is a direct cycle between T1 and T2 consists of write-read edges.
Under the current check transitive cycles are missed, e.g., (transaction id 1, version read = 2), (transaction id 2, version read = 3), and (transaction id 3, version read = 1).
A solution to this is to construct a dependency graph from the result tuples and check it is acyclic.
The above example would result in the graph: T1 -> T2 -> T3 -> T1