Could Elle tell the difference between snapshot isolation and strong-session-snapshot-isolation?

[Tsunaou]

In the consistency models you provided in README, I found that you have distinguished PL-SI (snapshot-isolation), strong-session-snapshot-isolation and strong-snapshot-isolation. However, it seems that you have not implemented this in Elle?

I constructed this history of 4 transactions running in 3 processes. There is a cycle as shown in the picture above. In other words, strong-session-snapshot-isolation is violated by this history.

(def h [{:type :invoke, :value [[:r :x nil] [:r :z nil]], :process 0, :index 0}
        {:type :ok, :value [[:r :x nil] [:r :z [1]]], :process 0, :index 1}
        {:type :invoke, :value [[:append :x 1]], :process 1, :index 2}
        {:type :ok, :value [[:append :x 1]], :process 1, :index 3}
        {:type :invoke, :value [[:r :z nil]], :process 1, :index 4}
        {:type :ok, :value [[:r :z nil]], :process 1, :index 5}
        {:type :invoke, :value [[:append :z 1]], :process 2, :index 6}
        {:type :ok, :value [[:append :z 1]], :process 2, :index 7}])

However, when I cloned the latest release v0.1.5, and checked this history by Elle, the result is valid.

Did I miss any key steps or did not set any key parameters when checking?

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

Sincerely, Young

[aphyr]

Yes, strong-session-SI is implemented, and it does work! However, it looks like Elle can't catch this particular anomaly just yet. I should note that in general Elle aims to be correct but (for efficiency) not sound; there are in general anomalies it cannot detect. This one should be inferrable, though! I've added a (presently commented-out) test if you'd like to experiment. Note also a test just above which does detect a strong-session-SI violation.

https://github.com/jepsen-io/elle/blob/0511c4f5e796261bb4266c2adc2d5c5fd5245f20/test/elle/list_append_test.clj#L655-L691

[aphyr]

Aha! An email from Alexey Gotsman got me looking at the right part of the code by accident--I wasn't certain, when I implemented g-nonadjacent, whether it could be properly generalized to realtime and process variants. Your example is not g-single-process, but g-nonadjacent-process, and because of my earlier caution I didn't implement that particular checker. After a few years of experience with nonadjacent, and your issue, I think it's probably reasonable for us to consider this a strong session SI violation. I've added support for it to elle, and the test now passes. :-)

[Tsunaou]

Thanks!

[aphyr]

If I had known you were planning to [write a paper](https://arxiv.org/pdf/2301.07313.pdf) based on this issue which claimed to invalidate the core claim of our work, I would have spent more time on my response. "Efficient but not sound" is obviously a typo: that should be "Efficient but not complete". I am also baffled at how "strong-session-SI is implemented, and it does work" became "we have confirmed with the developer that Elle does not [check strong session SI]". Like... that's the exact opposite of what I said. What the fuck.

[siliunobi]

We very much appreciate and respect the work of Elle. In fact, we are big fans of Elle. We also believe that it is a groundbreaking art which has stimulated the recent torrent of testing database systems. During our study, we tried to provide high-quality issue reports here and sought clarification and help from you and the community. For this particular issue, anything we claim in the manuscript is based on our understanding of the communication here. Overall, we think that the above comment of yours is not fair. See details below.

First, we knew that Elle is incomplete (at least in practice); that's why we said "Elle’s actual implementation ... and there are also anomalies it cannot detect." What we were not aware of was that Elle was not sound for efficiency. Therefore, we simply quoted what you said in the comment as we believed that you would be the right person to know Elle the best. Given that soundness and completeness are absolutely different concepts, we never thought it would be a typo, but just something we didn't know about Elle.

Second, we did not claim that Elle does not check strong session SI. Instead, we say "Elle does not fulfll this functionality in its latest release", meaning that Elle does not fully support strong session SI in the release for which we report this issue. In particular, this claim is based on the follow-up comment of yours, which explicitly says "... I didn't implement that particular checker ... I've added support for it to elle, and the test now passes. :-)" This sounds controversial to the earlier comment of yours "Yes, strong-session-SI is implemented, and it does work!" However, since the follow-up comment came later, our understanding is that you had not implemented "g-nonadjacent-process" checking, which is, however, fundamental to strong session SI.

However, although it is in general not mandatory, we think that having good communications here before publishing could've been better. We will have us improved in the future.

[aphyr]

we simply quoted what you said in the comment

Had you quoted the comment, it would have been obvious that this was not a soundness property.

What we were not aware of was that Elle was not sound for efficiency.

Again, this is not true. Our paper discussed soundness and completeness in depth. "[T]here are in general anomalies it cannot detect" is obviously referring to completeness.

In general: I get so, so many support requests. I try my best to respond, but I'm not paid for any of this work--I'm often squeezing responses to GH issues in between sets at the gym or during breakfast. I'm not always gonna get that right. If you're gonna publish a paper refuting the central claim of a work, and think a sentence seems completely bonkers, double-check first.

[siliunobi]

We have clarified the above discussed issues; see the updated version.