[tlaplus] Examples For Draining Updates

[zacattackftw <zacattackftw@xxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a091bc01-a313-4f33-9597-b64a2d0bff07n%40googlegroups.com.