Git’s merge algorithm seems to have inexplicable semantics leading to some interesting cases. I describe a couple of examples below. The bottom line is that: Git merge is inconsistent: Merge result seems to depend not just on what versions were merged, but also how they were merged. Thus two branches...
I was pleasantly surprised to discover that OCaml has been supporting modules as first-class objects since v3.12 (2011). Intuition suggests that first-class modules should be expressive enough to simulate Haskell-style typeclasses in OCaml. Turns out this is the route taken by Leo White et al to introduce adhoc polymorphism via...
This post is a collection of my notes on Lucas Brutschy et al’s paper “Effective Serializability for Eventual Consistency”. A later version of this paper has been accepted to POPL’17. Introduction Serializability is a well-understood criterion to reason about concurrent transactions. Enforcing serializability via pessimistic concurrency control techniques, such as...
In this post, I discuss DeCandia et al’s Dynamo paper, and Amazon’s DynamoDB service based on the paper. Dynamo DeCandia et al’s Dyanamo is a distributed key-value store remarkable for it’s entirely decentralized architecture, SLAs that focus on 99.9th percentile latency, emphasis on never losing writes, and the notorious sloppy...
Today, in our reading group, we read an interesting paper titled “Disciplined Inconsistency” by Brandon Holt et al from UW CSE. This post is my notes on the paper. Background Modern day web-services often trade consistency for availability and performance. However, there exist some data and operations for which stronger...
Extraction erases Props Extraction in Coq works by erasing Props. For example, consider the following definition of div: Definition div (m n : nat)(H : n<>0): nat := NPeano.div m n. div expects a proof that its second argument is non-zero. Indeed, in coq, it is impossible for div to...
This post is the compilaton of my notes on Terry et al’s PDIS’94 paper: Session Guarantees for Weakly Consistent Replicated Data. System Model From what I understand, the paper is the first to describe the abstract system model of a weakly consistent replicated database that now serves as a frame...
If you are ever into making debian packages to distribute your software, check out this great package management tool called fpm by @jordansissel. FPM is no-nonsense package manager that lets you create packages by simply specifying dependencies, and source and destination paths for your binaries, libraries and includes. Example Let...
In my previous post I have noted that Rails encourages application developers to rely on feral mechanisms, such as validations and associations, to ensure application integrity. In this post, I first explore various feral mechanisms in Rails, and how they are being used by some sample applications. Next, I will...
Quelea is our eventually consistent data store with an associated programming framework intended to simplify programming under eventual consistency. In this post, I describe how various applications written in Quelea employ a combination of highly available and serializable transactions to enforce application integrity. Three applications participate in this survey: BankAccount:...
This post is a compilation of my notes on Peter Bailis et al’s SIGMOD’15 paper: Feral Concurrency Control: An Empirical Investigation of Modern Application Integrity. Background Modern relational DBMs offer a range of primitives to help the developer ensure application integrity, even under the presence of concurrency: built-in integrity constraints...
One of the most useful features of ML-family languages (OCaml, Standard ML, F# etc) is the type inference. This post contains the notes I took when I was trying to understand the foundational principles of ML type inference. Damas-Milner Algorithm for Type Inference Let us take a look at the...
Few months ago, Cheryl birthday puzzle has has been an internet phenomenon. If you found the puzzle tricky to solve, we are in the same boat. However, if you observe, the puzzle only requires us to apply simple logic; not number theory or complex arithmetic, just simple logic. What, then,...
This post contains my notes on Rahul Sharma et al’s ESOP’13 paper: A Data-Driven Approach for Algebraic Loop Invariants. The paper proposes a neat approach of inferring algebraic loop invariants by observing concrete program states, and making use of techniques from linear algebra to gain insights. Following is an example...
A natural view of execution of a multi-threaded program is as follows: exn = [] while (there is an unfinished thread) { t = select an unfinished thread; instr = first(t); exn := exn ++ [instr]; t := rest(t); } return exn; Observe that exn preserves program order of all...
Sequential consistency requires that all data operations appear to have executed atomically in some sequential order that is consistent with the order seen at every individual process. If instead of individual data operations, we apply sequential consistency to transactions, the resultant condition is called serializability in database theory. Linearizability imposes...
This post is a compilation of my notes on two landmark papers: The Lisp paper: McCarthy J, Recursive Functions of Symbolic Expressions and Their Execution by Machine, CACM’60 Interpreters paper: Reynolds J C, Definitional Interpreters for Higher-Order Programming Languages, ACM’72 1.The Lisp Paper This paper by John McCarthy introduces the...
My intention in writing this note is to understand the relation between conventional model of distributed systems that they usually teach in the distributed systems course and the the distributed web services hosting replicated datatypes. Fault tolerance is a concern in the former, and it is studied separately from communication...