[tlaplus] Re: Examples For Draining Updates

On Monday, June 3, 2024 at 9:05:40 PM UTC-7 Andrew Helwer wrote:

It's a fairly general problem that admits a lot of different designs depending on what they want. I have modeled something similar for a contract but that spec is not open source. Generally database partitioning schemes are associated with a monotonically increasing epoch counter that increments on every partition change. You can attach this counter to the transactions at some point as the expected partition epoch. If the writes arrive at the database and the expected epoch is different from the actual epoch, there are a number of options available to you like sending the write back for a retry with the new epoch or translating it to the new partition scheme. Unfortunately I don't have any specs to give you as an example but that's how I've modeled it in the past.

Andrew Helwer

On Friday, May 31, 2024 at 5:02:45 PM UTC-4 zacattackftw wrote:
Hey folks!

I have a few teams that I'm assisting in their spec writing. A common pattern I've noticed is that they have a need to wait for writes to 'drain'. And knowing when all writes have drained is an integral part of the correctness for their specs.

As an example, one such spec involves splitting a database partition while it takes active writes. At a high level, this involves reading recent updates in a queue and applying them to a new destination. Then, once enough data has been consumed, new writes are directed to the new destination. Then comes a question on how long we should wait for writes on the original source to percolate through (or by what means can we deploy to know for certain that we've gotten all the writes sent to the destination?).

This seems to me like something that has likely been modeled before? So what I'm looking for are prior examples that I can use to share with these teams. My goal is to teach not just do it for them, and I'm hoping existing examples could help me to that end.

Thanks!

-Zac