Elle may miss two types of transaction anomalies:

[Tsunaou]

During my testing, I found the following two anomalies may be ignored by elle.

1. Cycle of wr-process-wr
   This case comes from transactional causal consistency:

(def h
  [{:process 1, :type :invoke, :f :txn, :value [[:r :x] [:append :y 1]], :index 0}
   {:process 1, :type :ok, :f :txn, :value [[:r :x [1]] [:append :y 1]], :index 1}
   {:process 2, :type :invoke, :f :txn, :value [[:r :y]], :index 2}
   {:process 2, :type :ok, :f :txn, :value [[:r :y [1]]], :index 3}
   {:process 2, :type :invoke, :f :txn, :value [[:append :x 1]], :index 4}
   {:process 2, :type :ok, :f :txn, :value [[:append :x 1]], :index 5}])

Here is my REPL screenshot

It is obvious that there is a cycle and I think this cycle should be prohibited by stong-session-snapshot-isolation

2. Future Read
   This case is about the internal consistency for a transaction.

I know elle do something special for internal-cases for read-your-writes condition, but maybe elle does not check for the future read.

I would appreciate it if you could give a prompt reply.

Sincerely,
Young

[aphyr]

Case 1 looks like a bug to me too! No idea why that one's happening--probably needs a test case and digging in to the version & txn graphs generated.

Case 2, agreed, I think we can and should detect this. I'm not exactly sure whether this still qualifies as an internal anomaly--it's actually an external read! But because we assume writes are unique, we know it's reading a value from later in the same transaction, and we should still be able to pick that up in a single pass. If you want to work on this, take a look at elle.list-append/op-internal-case.

[siliunobi]

We are going to publish some of our experimental results sooner or later. Based on your reply on the above two issues, would it be fair to say that Elle misses these two anomalies?

[aphyr]

Elle detects both of these anomalies.

[siliunobi]

We originally tested version 0.1.6 (and further up to 0.1.8) which couldn't find these anomalies. Now with 0.1.9 and beyond, Elle indeed detects both anomalies. I think that's attributed to the following two commits:

• 5f9618c
• bd0f26c
  Thanks for the effort!