We ran into that question with my friend Vladislav recently and it turns out to be there was already a discussion with Aphyr that basically ended with the following:
- seq-kv cas() is not linearizable - as expected
- seq-kv cas() can be reordered if it does not violate total order - which makes total sense.
I am not sure if we can talk about Serializability here, but it looks like it.
For more info pls read:
- Compare-and-swap on seq-kv · Issue #39 · jepsen-io/maelstrom · GitHub
- seq-kv reads never return final state for most recent write/cas · Issue #47 · jepsen-io/maelstrom · GitHub
Just like with a real DB, reads and even identity CAS in seq-kv can be arbitrarily stale; they can be safely reordered to execute in the past. In order to read the “current” state you can do two things. One option that I thought most people with real-world DB experience might try is to spam seq-kv with operations; since it’s sequential your client must eventually, probabilistically, converge to the most recent logical state. However there’s another, more subtle option: perform an operation that could not possibly have occurred before the ops you want your client to observe. If it succeeds, any later op your client performs must observe them! If you’d like to ponder that before the next paragraph, please do–it’s not necessarily obvious.
What ought to work (though I have not tried it due to time constraints!) is something like a write of a unique key or value–something that has never been written before. Since that write creates a state of seq-kv that could never have existed before already-completed writes, it must occur after them in the sequential timeline. Later reads by that client must then observe those already-completed writes.