Engineer Readings – Telegram
[article]

Low-Latency, High-Throughput Garbage Collection

https://users.cecs.anu.edu.au/~steveb/pubs/papers/lxr-pldi-2022.pdf
[article][db] Let's build a distributed Postgres proof of concept

By the end of this post, in around 600 lines of code, we'll have a distributed "Postgres implementation" that will accept writes (CREATE TABLE, INSERT) on the leader and accept reads (SELECT) on any node. All nodes will contain the same data.

https://notes.eatonphil.com/distributed-postgres.html
👍3
[article][distributed]

We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and imple- mented in MongoDB, a distributed database whose replica- tion protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, Leader- Completeness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system.

https://will62794.github.io/assets/papers/cpp22-formal-verification-reconfig.pdf