Posts

Highly Available Transactions: Virtues and Limitations (2013)

Overview

The CAP theorem’s trilemma of consistency, availability, and partition tolerance does not require sacrificing one property entirely but rather prioritizing among the three. Given a specific consistency model, how much availability is feasible? The paper Highly Available Transactions: Virtues and Limitations explores the relationship between consistency models and their achievable availability. It organizes each consistency-availability pair into a partial order based on their strengths.

January 30, 2025

Jepsen: A framework for distributed systems verification, with fault injection

Overview

Jepsen is a Clojure testing framework for distributed systems. A Jepsen test case defines operations on a system, expected responses to the operations, and a schedule for injecting faults to inject and the operations. The test case executes the operations, introduces faults as scheduled, and validates whether the system’s response meets expectations.

Jepsen appears to be well-regarded in the field of distributed systems. Tests results for major distributed systems using Jepsen are published on its official website. Additionally, A Jepsen test result for etcd, a key-value store used within Kubernetes, is available on its official website.

Despite its recognition, the tutorial of Jepsen wasn’t informative enough for me to learn the basic usage of Jepsen. For instance, while the tutorial uses etcd as an example, the client library for etcd is outdated, making it impossible to execute the tutorial as instructed. Instead, by researching Jepsen’s source code, I implemented an application with two-phase commits and a test case for it. The implemented application and test caseare available in one of my GitHub repository.

Despite of the insufficent reference, using Jepsen to implement test cases is still more efficient than building them from scratch. For a future reference, I will explore an advanced usage of Jepsen compared with the tutorial.

January 26, 2025

The Origins of Type Theory

Type theory began as an effort to resolve Russell’s Paradox, an issue discovered by Bertrand Russell. The precise events that mark the origin of type theory can be a matter of debate. Cantor, who developed set theory, independently discovered a similar paradox around the same time. In correspondence with Russell, Frege replied that in his conceptual notation, predicates do not take other predicates as arguments. Considering Russell’s approach that employs the hierarchical elements in the conceptual notation to resolve the paradox, one might argue that Frege’s predicate logic can be seen as an origin of type theory.

#Type Theory

December 30, 2024

Implementation of runc as of November 2024

runc is a container runtime with a command-line interface tool. Although runc was separated from Docker in 2015, Docker still uses runc because the Docker Engine is built on top of containerd, which incorporates runc. In this post, I will explain some Linux features used in the implementation of runc.

December 8, 2024

Back of Envelope Calculations

In system design interviews, back of envelope calculation is a task to estimate required comuputing resources based on the given requirement.

September 24, 2024

System design case study: video streaming service

Youtube is an example of a video streaming service where users upload, stream, search, and review videos. This post presents common designs for processing and hosting uploaded videos across several case studies of video streaming services for system design interviews.

#System Design Interview

September 18, 2024

REALM Retrieval Augmented Language Model Pre Training (2020)

REALM is a language model for open-domain question answering. REALM is composed of two components: the neural knowledge retriever and the knowledge-augmented encoder. The neural knowledge retriever finds documents related to the input. The knowledge-augmented encoder generates responses from the found documents and the input. In pre-training, the REALM employs masked language modeling, and it is trained to predict the original tokens that are maked in the given sentences. In fine-tuning, the model is trained to produce the answer of the given input. The authors experimented the model with Open-domain QA tasks under the assumption that the answer can be found as a contiguous sequence of tokens in some documents.

#Retrieval Augmented Generation

May 27, 2024

Distributed GraphLab: a Framework for Machine Learning and Data Mining in the Cloud (2012)

GraphLab is a programming model for machine learning and data mining. GraphLab takes a direct graph, a set of vertices, and update functions as input. Every update function accepts a vertex and returns a set of vertices. GraphLab selects a vertex from the set, applies a function to it, and adds the resulting set of vertices back intothe set, repeating this process until the set is empty. GraphLab supports parallel execution of update functions on multi-processor machines. Distributed GraphLab extends GraphLab by distributing parts of a graph across machines that are memory, utilizing Chandy-Lamport’s snapshot algorithm for fault tolerance.

#Distributed System

May 7, 2024

Policy Gradient Methods for Reinforcement Learning With Function Approximation (1999)

Policy gradient methods approximate stochastic policies using function approximators, which are independent of value functions. They update the policies according to the gradient of expected reward with respect to the policy parameters. Policy Gradient Methods for Reinforcement Learning With Function Approximation shows that a form of policy iteration with function approximation converges to a locally optimal policy.

April 27, 2024

Spark SQL: Relational Data Processing in Spark (2015)

Spark SQL provides a DataFrame API, an abstract data type equivalent to a table in a relational database. The DataFrame objects can be manipulated in a manner consistent with relational algebra. For example, the API includes various relational operators such as where and group by, similar to data frames in R and Python. The DataFrame objects are evaluated lazily, meaning they are not evaluated until certain output operations, like count, are performed. Catalyst, an optimizer written in Scala, optimizes these lazy queries and then compiles them into Java bytecode.

#SQL
#Spark

April 14, 2024