Hypermnesia: Eventual Consistency in Mnesia

Motivation Mnesia is a soft real-time embedded Database Management System written for Erlang, a programming language that powers the infrastructures of various organisations such as Cisco, Ericsson and the NHS. Due to Mnesia’s tight integration with Erlang, it is also impactful in open source projects such as RabbitMQ and ejabberd. However, the development of Mnesia has remained stagnant for years, resulting in the lack of features such as automatic conflict resolution: Mnesia leaves the handling of conflicts after network partitions entirely to the developer....

June 6, 2023 · Shuntian Liu

Erlog: A Distributed Datalog Engine

Introduction In this blogpost we build a distributed datalog engine that can process datalog queries such as the one below in a distributed fashion. The key idea mimics the usual dataflow programming idea such as MapReduce where we shard our data and create a dataflow-graph to specify the computation we want. link("a","b"). link("b","c"). link("c","c"). link("c","d"). link("d","e"). link("e","f"). reachable(X, Y) :- link(X, Y). reachable(X, Y) :- link(X, Z), reachable(Z, Y). We will build our engine from first principle by looking at how we perform single node evaluation of datalog queries, and then extend it to multiple nodes....

April 16, 2023 · Shuntian Liu

Equivalence of proof techniques in proving the fixpoint properties

Denotational Semantics is a unique course offered by the Computer Lab at UoC. It can be intimidating at first glance but at the same time bring you lots of fun and frustration at the same time. In this blog post we will look at three proof techniques in domain theory and investigate the connections between them. In this blog we look at three techniques that can be used to prove the fixpoint of a function, namely, Tarski’s fixpoint theorem, lfp1 + lfp2 and Scott induction....

June 30, 2022 · Shuntian Liu