Distributed Systems

Formal methods Formal methods are techniques – usually based on mathematics – used for the specification, analysis and verification of software and hardware. Why would anyone be interested in formal methods? The main reasons to consider formal methods are verifying that a design is correct, verifying that a change is correct, analysing a system to learn about it and developing an intuition about the system. Formal methods is the umbrella term that contains several techniques inside of it We’ll be considering only model checking because I believe it is the easiest to get started with and get a return on the investment quickly. ...

𝔇𝔢𝔱𝔢𝔯𝔪𝔦𝔫𝔦𝔰𝔱𝔦𝔠 𝔰𝔦𝔪𝔲𝔩𝔞𝔱𝔦𝔬𝔫 𝔱𝔢𝔰𝔱𝔦𝔫𝔤 deterministic: of or relating to a process or model in which the output is determined solely by the input and initial conditions, thereby always returning the same results ( stochastic ): The algorithms are simple and deterministic, so the results are predictable and reproducible. Example based testing Example based testing works fine for simple cases where there’s only a small number of actions that matter. let%test_unit "append entries: truncates the log on entry conflict" = let storage = make { dir = Test_util.temp_dir () } in (* Leader adds some entries to the replica's log. *) append_entries storage (last_log_index storage) [ { term = 1L; data = "1" }; { term = 2L; data = "2" }; { term = 3L; data = "3" }; ]; (* Another leader overrides the replica's log. *) append_entries storage 2L [ { term = 4L; data = "3" }; { term = 4L; data = "4" } ]; assert (entry_at_index storage 1L = Some { term = 1L; data = "1" }); assert (entry_at_index storage 2L = Some { term = 2L; data = "2" }); (* Entry at index 3 has been overwritten. *) assert (entry_at_index storage 3L = Some { term = 4L; data = "3" }); (* Entry at index 4 is new. *) assert (entry_at_index storage 4L = Some { term = 4L; data = "4" }) It becomes way harder to think of and write the examples when the bugs you’re looking for only happen after several events that need to happen in a specific order. ...

This post contains TLA+ solutions for The Deadlock Empire which is a collection of challenges where the objective is to break multithreaded programs by playing the role of a scheduler that can context switch at any time. Non atomic instructions There’s two threads executing the following code: a = a + 1; if (a == 1) { critical_section(); } Since the a increment is not atomic, conceptually, it is like setting a temporary variable to the value of a– tmp = a and then setting a to the temporary variable value incremented by 1 – a = tmp + 1. ...

As the World Wide Web became more popular all of sudden a server could receive way more traffic than it could handle causing the server to service requests slowly or to not be able to serve them at all1. An intuitive solution to this problem is to cache2 the content served by the servers and allow the clients to fetch content from the caches instead of going to the original server. Several clients communicate with the same cache servers which means that if client 1 fetches the contents for the page example.com, client 2 can fetch the same contents from the cache instead of going to the oirignal server if it decides to visit example.com as well. ...

It feels like most people are not used to thinking about how things can fail, programming as if things always work as expected is the default modus operandi of most engineers i have talked to. Some examples that come to mind: http requests without handling responses that don’t have status 200, no timeouts, no retries, publishing a message to kafka and them updating a database, having a web client orchestrate a transaction across several systems without thinking: what if the user closes the browser tab? ...

What is a log A log is just a immutable sequence of records wih strong ordering semantics that can be used to provide durability, replication and to model consensus. It is usually a 0 indexed file that new entries are appended to because expensive disk seeks can usually be avoided when appending to a file1. Not to be confused with the type of logs most people are used to: application logs that are meant to be read by humans although application logs are a degenerative case of the log we are talking about2. ...

Replicated And Fault Tolerant Raft is a consensus algorithm for managing a replicated log. The authors claim Raft to be more understandable than Paxos because Raft separates the key elements of consensus Leader election Log replication Safety and enforces a stronger degree of coherency to reduce the number of states that must be considered. Raft also includes a new mechanism for changing cluster membership. What is a consensus algorithm Consensus algorithms allow a collection of machines to work as a coherent group that can survive the failures of some of its members. ...