[HN Gopher] Formal Verification of Zero-Downtime Database Migrat...
       ___________________________________________________________________
        
       Formal Verification of Zero-Downtime Database Migration in PlusCal
        
       Author : code_monk666
       Score  : 37 points
       Date   : 2025-03-09 06:31 UTC (2 days ago)
        
 (HTM) web link (biradarganesh25.github.io)
 (TXT) w3m dump (biradarganesh25.github.io)
        
       | pwnna wrote:
       | Neat! I worked on a similar formal verification of Ghostferry,
       | which is a zero downtime data migration tool that powers the
       | shard balancing tool at Shopify, also using TLA+:
       | 
       | https://github.com/Shopify/ghostferry/blob/main/tlaplus/ghos...
       | 
       | I also was able to find an concrrency bug before a single line of
       | code was written with the TLC which saved a lot of time. It took
       | about 4 weeks to design and verify the system in spec and about 2
       | weeks to write the initial code version, which mostly survived to
       | this day and reasonably resembles the TLA+ spec. To my knowledge
       | (I no longer work there) the correctness of the system was never
       | violated and it never had any sort of data corruption. Would be a
       | much harder feat without TLA+.
        
       | asah wrote:
       | for fun, I popped it into ChatGPT o3-mini-high, had it generate
       | the TLA+ code then compare its version to the human-written
       | version:
       | 
       | https://chatgpt.com/share/67d0390c-4208-8007-a39d-8d9bfa7886...
        
         | hwayne wrote:
         | I see at least a few errors with the TLA+ code:
         | 
         | - It says that `olddb = [k \in Keys |-> CHOOSE v \in Values:
         | TRUE]` initializes olddb nondeterministically. This is NOT
         | true: `CHOOSE` is guaranteed to be a deterministic expression.
         | The actual thing is `olddb \in [Keys -> Values]`.
         | 
         | - `key \in Keys; val \in Values; newdb[key] := val;` is a
         | syntax error. I _think_ what it meant was `with key \in Keys,
         | val \in Values { newdb[key] := val;`
         | 
         | - `newdb[key] := val` is an error anyway, because `newdb` was
         | initialized as a set.
         | 
         | - ` for key \in DOMAIN(olddb) do` is straight up a syntax
         | error, there's no for loop in PlusCal.
         | 
         | - It's mixing p-syntax (`if then end if`) with c-syntax (`if
         | {}`).
        
         | code_monk666 wrote:
         | When I wrote this, I had tried getting help from several
         | different chat models. None of them produced anything remotely
         | useful--but they did help me learn formal verification, as well
         | as syntax when writing in PlusCal
        
       | agentultra wrote:
       | I recall learning TLA+ around 2015/2016 to solve a hard bug in an
       | OpenStack deployment. I was miffed that I was some 17 years into
       | my career and had only learned about it then. It was so useful!
       | 
       | Since then I've used it for similar purposes as this. I try to
       | share with my team when I do this kind of work. But often folks
       | are highly resistant to it so I use it on my own when I'm working
       | on a hard project.
       | 
       | Spending the time up-front to work out the design is often more
       | cost effective in terms of time and money than iterating in
       | production towards a, "more correct design." Getting it right
       | first sounds hard, and it's challenging, but it's worth it for
       | the kinds of projects where mistakes are costly, difficult to
       | diagnose and to fix.
       | 
       | And I think more software developers are starting to realize this
       | [0] (even if they're using different methods).
       | 
       | [0]: https://www.youtube.com/watch?v=w3WYdYyjek4&t=1333s
       | 
       |  _Update_ : grammar/spelling
        
       ___________________________________________________________________
       (page generated 2025-03-11 23:02 UTC)