Reading

Distributed system && Database reading list

Formal method

Formally Verified Systems

An Empirical Study on the Correctness of Formally Verified Distributed Systems [pdf]

The seL4 Microkernel

Sel4 is a high-assurance, high-performance operating system microkernel which uses formal verification. The seL4 verification uses formal proof in the theorem prover Isabelle/HOL

Chapar: certified causally consistent distributed key-value stores [link]

TLA+

Lamport. Learning TLA+ [link]

Hillel. Learn TLA+ [link]

Hillel Wayne. Practical TLA+ Planning Driven Development [link]

Industrial use

Formal Development of a Network-Centric RTOS [pdf]

How Amazon Web Services Uses Formal Methods [pdf]

Model-based for Testing

Andrey Kupriyanov, Igor Konnov. Model-based testing with TLA+ and Apalache [pdf] [video]

A. Jesse Jiryu Davis, Max Hirschhorn, Judah Schvimer. Extreme modelling in practice [pdf]

Model Checking Guided Testing for Distributed Systems [pdf]

Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 [pdf]

Kayfabe: Model-based program testing with TLC - Star Dorminey [video]

State explosion problem

Xiaosong Gu, Wei Cao, Yicong Zhu, Xuan Song, Yu Huang, Xiaoxing Ma. Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction [pdf]

Using compositional model to check Raft and avoid the state explosion problem.

A. Methni, B. Ben Hedia, M. Lemerre, S. Haddad, K. Barkaoui. State Space Reduction Strategies for Model Checking Concurrent C Programs [pdf]

Distributed System Theory

Distributed Algorithms, Nancy A. Lynch [link]

Distributed System Testing

Greybox Fuzzing of Distributed Systems[pdf]

Fuzzing Raft Testing[fuzzing-raft]

Database

NVME

What Modern NVMe Storage Can Do, And How To Exploit It: High-Performance I/O for High-Performance Storage Engines Gabriel Haas, Viktor Leis [pdf]

Exploiting Directly-Attached NVMe Arrays in DBMS Gabriel Haas, Michael Haubenschild, Viktor Leis [pdf]

MVCC

Memory-Optimized Multi-Version Concurrency Control for Disk-Based Database Systems [pdf]

Coroutine + Aschronous IO

The Art of Latency Hiding in Modern Database Engines [pdf]

System Tech

io_uring

Efficient IO with io_uring [pdf]

Rust io_uring wrapper, tokio-uring

io_uring example, io_uring-by-example

awesome-iouring

PostgreSQL io_uring support Discussion

[What Are You Waiting For? ] (https://db.in.tum.de/~fent/papers/coroutines.pdf?lang=en)

Rust programming language

Rust

Rust, The Book

Rust, The Async Book