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

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

elle/test/elle/list_append_test.clj

Lines 655 to 691 in 0511c4f

	; TODO: We're not clever enough to catch this anomaly yet.
	#_ (testing "Strong Session SI violation 2"
	; This one was submitted by Tsunaou:
	; https://github.com/jepsen-io/elle/issues/17
	(let [; wr: observes t3's append on z
	t0 {:process 0, :index 0, :type :invoke, :value [[:r :x nil] [:r :z nil]]}
	t0' {:process 0, :index 1, :type :ok, :value [[:r :x nil] [:r :z [1]]]}
	; rw: t0 did not see the append to x
	t1 {:process 1, :index 2, :type :invoke, :value [[:append :x 1]]}
	t1' {:process 1, :index 3, :type :ok, :value [[:append :x 1]]}
	; process: still p1
	t2 {:process 1, :index 4, :type :invoke, :value [[:r :z nil]]}
	t2' {:process 1, :index 5, :type :ok, :value [[:r :z nil]]}
	; rw: t2 did not observe append of z.
	t3 {:process 2, :index 6, :type :invoke, :value [[:append :z 1]]}
	t3' {:process 2, :index 7, :type :ok, :value [[:append :z 1]]}
	; Unnecessary read, but just to help make sure this isn't an issue
	; with the nil -> any write rw inference rule...
	t4 {:process 3, :index 8, :type :invoke, :value [[:r :x nil] [:r :z nil]]}
	t4' {:process 3, :index 9, :type :ok, :value [[:r :x [1]] [:r :z [1]]]}
	[t0 t0' t1 t1' t2 t2' t3 t3' :as h]
	(h/history [t0 t0' t1 t1' t2 t2' t3 t3' t4 t4'])]
	; A serializable checker won't catch this
	(is (= {:valid? true}
	(c {:consistency-models [:serializable]} h)))
	; But it will if we ask for strict-serializable.
	(is (= {:valid? false
	:anomaly-types [:G-single-process]
	:not #{:strong-session-snapshot-isolation
	:strong-session-serializable}
	:anomalies
	{:G-single-process
	[{:cycle [:todo]
	:steps :todo
	:type :G-single-process}]}}
	(c {:consistency-models [:strong-session-snapshot-isolation]}
	h)))))

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