Linearizability algorithms

[ahorn]

I read your blog post with great interest. I had a few questions on how Knossos compares with other related work on linearizability that is not mentioned in the blog post, and so set out to experiment with a variant of the Wing and Gong algorithm, including later extensions by Lowe. This is work-in-progress but the results seem promising. You seem to enjoy fun problems, so I only wanted to share that link in case you feel like bouncing off ideas or providing any feedback, questions etc.

PS Thanks for the Jepsen infrastructure by the way.

[aphyr]

Cool! :)

[ahorn]

Hey, I've now completed more experiments and the results are pretty interesting. The implementation in https://github.com/ahorn/linearizability-tester is evaluated against histories collected from three sources: Intel's TBB library, Siemens's EMBB library, and etcd.

Out of 100 etcd benchmarks (histories collected using Jepsen), the new tool successfully checks linearizability in a few seconds, whereas Knossos times out on benchmarks 7 and 99, and runs out of memory on benchmarks 40, 57, 85 and 97.

I am purposefully avoiding drawing conclusions from the other benchmarks because Knossos runs on the JVM, whereas the new implementation does not, and so the other speedups are not reported. Instead I focused on timeouts and out-of-memory errors. I am curious to find out whether you agree with this evaluation, or if there are any other things you think should be taken into consideration. It would be cool if these findings could further advance Jepsen.

[aphyr]

Not knowing C++ (wait, is this C++?) it's hard for me to say, but I can tell you that Knossos is literally Shit I Made Up After Reading A Bunch Of Papers And Not Knowing What Existing Tools To Use, so I wouldn't be at all surprised if you could beat it. Knossos does hang on some real-world histories, and I'd be delighted to use an off-the-shelf tool or rewrite/expand the algo.

Got a lot going on at the moment, but tl;dr is thanks for working on this; I don't understand it yet but I can definitely read the papers and try to adapt their techniques. If your checker can read histories from stdin or whatever I could also just call out to it from Jepsen, though I suppose we'd need a way to represent model transitions as well.

[ahorn]

Yes, the tool is written in a recently standardized version of C++, known as C++11. The rationale behind the choice of language is the need to experiment with various techniques, and for this it is good to rule out interference from the JVM such as garbage collection etc. It would be interesting to re-implement the tool in your favourite language and measure the performance of both implementations but time to do so is the limiting factor for me right now.

I am planning to write a paper where I discuss some of the insights gained in trying out various algorithms (some known ones, some new) and possible ways of implementing these. For example, a constant-time hash function for bitsets makes several orders of magnitude difference. On the algorithmic front, I found a new partitioning scheme for associative containers that is very effective, but quite restrictive for the kinds of operations it supports.

In principle, it should be possible to integrate Jepsen with the new tool because it merely reads the output produced by say lein with-profile +etcd test jepsen.system.etcd-test. You are right in thinking that the models may pose problems. Currently, there is only support for stacks, sets and registers. These data structures must be persistent, and ideally they should support fast equality checks. So things like queues may require a bit more thought to get optimal performance (if so desired). What models would you need?

[aphyr]

Ideally, SQL, haha. I want to build up to linearizability verification of stuff like Postgres eventually; ad-hoc subsets of the query language should do the trick though.

[ahorn]

I don't understand it yet but I can definitely read the papers [...]

Here's a temporary link to an RFC draft paper: https://www.cs.ox.ac.uk/people/alex.horn/linearizability-p-compositionality-draft.pdf (use FORTE'15 paper instead: http://arxiv.org/abs/1504.00204)

When ready, I'll update the above link to a permanent link. To get there, I'd appreciate if you could have a look at the draft if you have time.

[aphyr]

(Reading the Lowe paper right now)

[ahorn]

Awesome

[aphyr]

Apologies if you're already following recent commits, @ahorn, but I wanted to let you know that the symmetry reduction for the world cache was horribly broken in 0.2.0 and should yield much, much faster results now. Histories that used to take multiple days can now complete in under a second.

(guess who didn't remember the right key name in a map and doesn't use core.typed: DIS GUYYYYY)

[ahorn]

I presume this is about commit aa86178f0a3c7af3649ce4c73841cba1a2541a67 from today. Thanks for letting me know (I do not follow recent commits and would have missed this). Is it possible to feed into Knossos its own output? For experiments, I have several histories from etcd that I could use to quantify the benefits of the fix.

Once I can rerun the experiments, I could get in touch with Gavin about that one sentence in the related works section in his paper, which in turn is related to Section 5.3 in the P-compositionality draft paper above. I think that sentence is based mostly on our previous discussion offline and he would be interested if this has to be changed due to commit aa86178f0a3c7af3649ce4c73841cba1a2541a67.

[ahorn]

The experimental results with P-compositionality are now published in FORTE'15. Here's a link to the paper: http://arxiv.org/pdf/1504.00204v1.pdf

This work may be particularly relevant if you wanted to take it a notch up with, say, your "cas-set-client".

[ahorn]

Hi @aphyr. Two short questions. Q1: I'll present our experiments next week at a distributed systems conference and I would like to find out whether you agree with the above "cas-set-client" remark in the context of Jepsen. Q2: Related to the upcoming conference, do you have a preferred existing (paper) reference (experiments, blog post, paper or what not) that should be cited for Jepsen (in case there are more recent publications under review or just recently accepted)?

[aphyr]

Q1: not sure what remark you're talking about probably because I am super jetlagged and dumb :(

Q2: No papers, sadly. https://aphyr.com/posts/314-computational-techniques-in-knossos

[aphyr]

Oh hey, I went and implemented the WGL checker as well here! We can close now :D

[ahorn]

Great! How about the P-compositionality extension?

[aphyr]

Ah, we do that at a higher level; Jepsen breaks up independent components before Knossos gets involved. Might be worth adding just for grins though.