Very cool! I’ve spent the last few months implementing a production MVCC system that’s completely lock-free. It’s really quite simple, but there were initially

Very cool! I’ve spent the last few months implementing a production MVCC system that’s completely lock-free. It’s really quite simple, but there were initially bugs in all the concurrent algorithms I designed. I wish I had time to learn TLA+ and properly model-check the algorithms, but for now I have to gain confidence just from stress testing and thinking hard about interleavings. The main thing I’ve learned is not to over-optimize. Keeping the algorithms as simple as possible is the only way I can reason about them.