Re:Learn TLA+ (2018)
by mcpherrinm on Saturday February 22, 2020 @10:06PM
(#22394822)
One of my coworkers used TLA+ to prove a change to a service my teams runs was correct.
The service was essentially a key/value store. If one region didn't know about a key, it would recursively ask the other regions in parallel for the data.
Eventually we needed to add support for deleting data. We deleted data that hadn't been read in a few months.
We used TLA+ to prove our region-sync code and deletion code interacted properly along with regular get/put operations.
The service was essentially a key/value store. If one region didn't know about a key, it would recursively ask the other regions in parallel for the data.
Eventually we needed to add support for deleting data. We deleted data that hadn't been read in a few months.
We used TLA+ to prove our region-sync code and deletion code interacted properly along with regular get/put operations.