Likes breaking ideas and systems, writing, picking systems apart @confluentinc Ex @Splunk, @VMware jack-vanlightly.com Credit: ESO/B. Tafreshi
Barcelona, Spain
- Tweets 1,761
- Following 251
- Followers 4,993
- Likes 1,089
Another WAL-on-S3 design verified, Objwal.
That's 4 single-writer WALs and 4 multi-writer WALs so far. Gonna add a few more before I do a classification and write-up.
github.com/Vanlightly/s3-wal…
3
20
1,017
Even though I've specified 6 WAL-on-S3 designs (plus 2 variants), the backlog keeps growing. Luckily, I'm starting to see more and more overlap and I can reuse major parts of already written specs. So maybe, I might be able to speed things up, though I only get 2-3 hours a day to work on this. This morning I've started on objwal, which on the surface looks like my OpenData Buffer single-writer variant, so hopefully I can lean on that spec for this one.
1
1
15
1,222
The Walgit spec is done, bringing the number of designs covered to 6 plus 2 variants. More to go before I start writing up the survey results and start classifying WAL-on-S3 patterns. github.com/Vanlightly/s3-wal…
Which next?
4
2
25
2,108
Jack Vanlightly retweeted
Unfortunately, you can’t outsource understanding any more than you can outsource sleeping. You can, of course, pay someone else to do it. But that doesn’t accomplish your goal.
4
4
33
1,111
I'm finalizing the work on my Walgit spec. The source repo has very detailed TLA+ specs already. My spec is a simplified version, which discards the git stuff, some of the ambiguous CAS write failure handling, to reduce behavior to the core WAL mechanics.
1
10
1,097
Jack Vanlightly retweeted
Want to get better at (or started with) formal methods? Surround yourself with experts @hillelogram @DominikTornow @k0nn0v @muratdemirbas @lemmster @ilyasergey @ankushpd @Leonard41111588 @MarcJBrooker @vanlightly @immadnaseer
You're welcome.
3
7
44
5,568
Yeah we just wrote a paper (LogDrive) about some of the internals of K2. Oh wait, this is another K2...
Cloudflare is working on K2, a durable event-stream primitive.
It's a named, append-style log of "records" you produce to and consume from, with a configurable retention window, writable from a Worker binding or over HTTP.
Basically Cloudflare Kafka.
1
5
79
7,910
My TLA+ spec for Cursor's Continuity is done. github.com/Vanlightly/s3-wal…
Next I will evaluate Tobias Lütke's walgit to see if it makes any interesting changes to the design.
3
2
46
2,004
I'm looking at Cursor's Continuity blog post (cursor.com/blog/git-at-any-s…). It seems very similar to OpenData Buffer, with compaction added on. Though the packfiles also look like they're numbered? Though that seems unnecessary as the reference file determines the ordering. Are there any more details than the blog post? I think I'll take my Buffer spec and add compaction (WAL GC) to it.
2
2
22
1,695
Just putting finishing touches in the Continuity spec. I implemented a simplified compaction via snapshotting the repo and updating the wal index with the snapshot id (which represents the position of the snapshot in history and the compaction frontier).
I've mostly left out GC of packfiles (it uses some magic to determine which can be deleted), as Cursor's blog post doesn't cover that.
I'll look at walgit next as that is an implementation inspired by the Cursor blog post.
3
1
9
905
Continuity compaction is very hand-wavy in the blog post. Only the primary does it, but at the same time, it's a soft "primary", more like multi-master with soft affinity. There is a compaction frontier. Adjacent pack files get merged. That's about it. I'll just have to figure something out.
1
4
567
I made good progress on the Cursor Continuity TLA+ spec. Reads and writes done. Next compaction. The visualizations in Cursor's blog post are helpful, but it's still not quite enough to fully describe the protocol.
For example, as far as I can figure, a rebase is not only needed after a write conflict. Two replicas can write their pack file concurrently but then update the WAL index serially (without a CAS conflict):
1. r1 writes pack file p1
2. r2 writes pack file p2
3. r1 reads the wal index
4. r1 appends p1 to the index, CAS writes it and commits locally
5. r2 reads the wal index
6. r2 see's that a new entry was added and must now rebase
7. r2 appends p2 to the wal index, CAS writes it and commits locally
Ultimately, very similar to OSWALD which is also multi-writer. If a replica sees that it is behind, it must catch up before appending its own op.
2
15
873
Hmmm, numbering the packfiles may help with GC as one of the problems with Buffer is knowing when an object can be deleted. How does a GC tell the difference between a newly updated object not yet added to the manifest and a previously commit object that was removed from the manifest? Buffer relies on time: it encodes a timestamp into the object ids and uses a deletion grace period. So not strictly safe as far as dist sys protocols go but probably fine given a large enough grace period.
1
351
Looks like I can't write a spec for S2.dev as the code is closed source. There is s2-lite which is open and uses SlateDB, so I'm going to assess whether there's a serious protocol there or not.
2
15
1,388
Ok, S2 Lite delegates single-writer enforcement to SlateDB’s fenced WAL, so acknowledged appends should remain linearizable with competing Lite nodes.
But Lite assumes a single node: nodes answer check-tail from cached state (so a stale node wouldn't discover it's fenced), which then impacts reads (stale tail can cause a node to say an address is Unwritten when it is actually Written). So Lite isn't linearizable under multi-node use. Any automation trying to keep one node running would need to be careful so that the worst case would be stale prefix reads (monotonic, prefix-consistent failover), which "can" be ok for streams. SlateDB does the heavy lifting and that's already modeled so I'm moving on.
2
2
334