Model checking The Deadlock Empire

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. ...

August 15, 2024 · 27 min · poorlydefinedbehaviour

Consistent hashing

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. ...

October 6, 2023 · 6 min · poorlydefinedbehaviour

Thinking about failure, fair-loss links and two generals

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? ...

March 28, 2023 · 3 min · poorlydefinedbehaviour

Logs

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. ...

April 30, 2022 · 2 min · poorlydefinedbehaviour

Notes taken from the Raft paper

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. ...

March 4, 2022 · 17 min · poorlydefinedbehaviour