𝔇𝔒𝔱𝔒𝔯π”ͺ𝔦𝔫𝔦𝔰𝔱𝔦𝔠 𝔰𝔦π”ͺπ”²π”©π”žπ”±π”¦π”¬π”« 𝔱𝔒𝔰𝔱𝔦𝔫𝔀

𝔇𝔒𝔱𝔒𝔯π”ͺ𝔦𝔫𝔦𝔰𝔱𝔦𝔠 𝔰𝔦π”ͺπ”²π”©π”žπ”±π”¦π”¬π”« 𝔱𝔒𝔰𝔱𝔦𝔫𝔀 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. ...

December 3, 2024 Β· 22 min Β· poorlydefinedbehaviour

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