Potential readers, not sure whether or not to make the slog: Do.
This is the most effective explanation (for me, anyway) of the difference between "serializable" and "linearizable" of any of aphyr's blogs so far. They've been keywords in that little cladistic tree of consistency models he draws for a while now, but with this explanation and the examples, I finally grok what they mean.
I'm not so sure. The definition of strict serializable/linearizable given in this post is weaker than what most people use. Most people require that linearizable execution must happen as-if it matches a global clock. Simply requiring that the effects of a transaction happen within the start/end time of the partition executing the transaction does not guarantee this. Most distributed databases (from what I can tell, including voltdb) only guarantee that for operations which read/write the same keys. Non-conflicting transactions execute without any synchronization overhead - and that's a good thing! But in the presence of side channels, you need a truly global clock (like spanner) to achieve strict serializablility.
Most people require that linearizable execution must happen as-if it matches a global clock. Simply requiring that the effects of a transaction happen within the start/end time of the partition executing the transaction does not guarantee this.
I'm not sure what you mean by "within the start/end time of the partition executing the transaction". Nothing in the informal definition I provided mentioned partitions, or even process-local orders (that'd be sequential consistency) so ... yeah, I dunno where you got this from. I agree that linearizability is a global real-time constraint, and I use that sense in the post and in the Knossos verifier.
Most distributed databases (from what I can tell, including voltdb) only guarantee that for operations which read/write the same keys.
You raise an interesting question: if I verify only that operations on a single key are linearizable, have I also verified that operations on systems of independent keys are linearizable? The answer, as far as I know, is yes: linearizability is a local (or "composable") property. From Herlihy & Wing (https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf):
Unlike alternative correctness conditions such as sequential consistency [31] or serializability [40], linearizability is a local property: a system is linearizable if each individual object is linearizable. Locality enhances modularity and concurrency, since objects can be implemented and verified independently, and run-time scheduling can be completely decentralized.
This is a commonly cited property in the literature, and has been proven several ways--for instance, see Lin's recent constructive proof (http://arxiv.org/abs/1412.8324). There is research showing linearizable systems vary in the probability distribution of outcomes (https://arxiv.org/pdf/1103.4690.pdf), but this does not affect safety.
However, your comment led me to Charron-Bost & Cori 2003 (http://www.worldscientific.com/doi/abs/10.1142/S012962640300...), whose abstract claims a counterexample system of two linearizable objects whose composed system is nonlinearizable. I haven't found the full text yet, and I'm not familiar with their sense of "The Global Time Axiom", so it's possible their finding is still consistent with "linearizability is composable". Not sure.
In any case, the multi-key tests in this analysis do perform single-key transactions (as well as multi-key transactions), and verify that their composed system is fully linearizable. Because the state space for composed systems is larger, these tests aren't as good at finding bugs--but if composability turns out not to hold, I can use this strategy more often.
But in the presence of side channels, you need a truly global clock (like spanner) to achieve strict serializablility.
As I understand it, Spanner's global clocks are a performance optimization, not a correctness condition. If linearizability required a global clock, Zookeeper (http://static.cs.brown.edu/courses/cs227/archives/2012/paper...) and Raft (https://raft.github.io/raft.pdf) wouldn't be able to provide linearizable semantics. It is, of course, possible that these papers are wrong, in which case I encourage you to publish!
(I've since skimmed Charron-Bost & Cori, and it shows that linearizability is not composable when there does not exist a total order of invocation and response events. This might be of use in relativistic scenarios with... accelerating spacecraft which still need to perform linearizable computation? I don't think it's particularly relevant to clocks down here on the geoid.)
I will update the docs to acknowledge that consistency guarantees may be compromised if the relative speed between servers in a cluster or clients is a nontrivial fraction of the speed of light.
This is the most effective explanation (for me, anyway) of the difference between "serializable" and "linearizable" of any of aphyr's blogs so far. They've been keywords in that little cladistic tree of consistency models he draws for a while now, but with this explanation and the examples, I finally grok what they mean.
Thanks, aphyr.