search

ahorn / linearizability-checker

Fast linearizability checker
65 stars 3 forks source link

clarify the test against etcd #1

Closed xiang90 closed 9 years ago

xiang90 commented 9 years ago

I really appreciate the work you have done to make linerizability checking faster.

I noticed the mention of etcd in the test. It is a little bit confusing. I hope you can help to clarify:

  1. the test was done against the historical records collected from etcd 0.4 one year ago
  2. the test proves a system (etcd) designed for sequential consistency is not linearizable

Moreover, etcd supports linearizable operations today. We are trying to make etcd a low cost linearizable system.

ahorn commented 9 years ago

The etcd developers were very helpful and hopefully this link can clarify things: https://groups.google.com/d/msg/etcd-dev/AslsLq2Lddk/FWRNkwOrV6IJ

In particular, these experiments used etcd 2.0 with "quorum=false".

xiang90 commented 9 years ago

@ahorn

I am the author of etcd actually. If you want to ensure linerizability in etcd, you should follow what yicheng said "set quorum=true".

It is a little bit misleading since the audience would think etcd fails to ensure its guarantees. But the fact is, as you said:

I've repeated the experiments with "quorum=true" and things seem to work nicely.
xiang90 commented 9 years ago

I understand you want to emphasize that your system is faster and more memory efficient than existing checkers.

However I think you still need to ensure that the content is clear and solid.

ahorn commented 9 years ago

My apologies if this has not come across. We did not talk about etcd in the paper so this bit was only included as extra info in the README as another interesting data point in our comparison with existing tools. I shall update the README accordingly because I agree that it could be misleading otherwise. All best wishes, Alex

ahorn commented 9 years ago

This is in commit 1a717650d2f5589bb0ca25003d429f831eaaa698. Is that okay?

xiang90 commented 9 years ago

@ahorn Not a problem at all.

We are working on a low cost linerizability mechanism in etcd recently. Also we are working closely with cockroach db guys, which is a distributed supports linerizability. /cc @spencerkimball @bdarnell

We will need your help to set up the testing environment!

Thanks again for your effort.

xiang90 commented 9 years ago

@ahorn LGTM!

xiang90 commented 9 years ago

If you can mention etcd passes the test if you set q=true, then it would be more awesome.

ahorn commented 9 years ago

Sure thing, commit 8c2a21fa797caa6e47cc468ef06a75e2462cd0c0.

Re: testing environment. All the credit for getting histories from etcd 2.0 deservedly goes to @aphyr who wrote Jepsen. I have merely written a tool that I hope is useful when testing concurrent data types such as sets and maps, which may be particularly relevant for tests with, say, cas-set-client in Jepsen [1].

[1] https://github.com/aphyr/knossos/issues/6

xiang90 commented 9 years ago

@ahorn Great! Thanks!