Elle may miss two types of transaction anomalies: about elle

[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!