Posts

This blogpost is the second part of a trilogy of formal verification on computer systems. Here we will take a quick tour of what formal verification means, with a particular focus on verifying systems software and examples of verifying some file system. If you have not read the previous post on system verification, feel free to jump there first for an introduction! Case studies CompCert CompCert1 is probably one of the first and most famous verified compilers (and perhaps also computer systems). It is itself a significant piece of work which took around 15 years. It is a rather important corner stone, however, that is achieved by the verification community, with tools/frameworks available in 2009, it is already possible to formally verify a complex system such as a compiler. ...

This blogpost is the first part of a trilogy of formal verification on computer systems. Here we will take a quick tour of what formal verification means, with a particular focus on verifying systems software and examples of verifying some file system. What do you mean by formally verified systems? Sometimes we hear people say we have built this formally verified system that is provably correct, and does all sorts of amazing things without bugs. But what we mean by having a system formally verified? At a high level, a formally verified system often has a formal specification which mathematically stipulates what the system ought (and ought not) to do, followed by a proof that such a concrete realisation of the system meets such a spec. ...

This is a very high level summary of the experience attending S-REPLS 14. Feel free to look at the respective website of the speakers for more details. To keep this blog concise, I thought I would just use introductory examples where possible to illustrate the idea rather than going into the actual theory behind them. Graded types and algebraic effects Graded type system is based on the idea of linear types. Linear types essentially allows one to restrict the usage of variables exactly once, which can be useful for resource management such as IO. Graded types go further than this and allows one to specify the number of times a variable can be used. For example, in the following code1, the variable a needs to be used exactly twice. ...

When I first encountered the concept of an adjunction, I got quite confused as to what it is, and why it is useful: Just how on earth is a left adjoint of a functor? What’s the matter of a free and forgetful functor, why is free left to forgetful but not the other way round. That’s where this blog comes from. I hope this blogpost can help demystify adjunction for you a little bit. ...

This article is very much my attempt to understand monad as a design pattern in programming languages and why on earth it is useful. There are tons of monad tutorials online, but I found relatively few ones argue for the usefulness of a monad by having side by side code examples that achieve similar functionalties. If you found one, please do let me know! I try to draw connections between monads’ original mathematical definition and its actual usage so that this mysterious concept does not come out of the blue. ...

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. Moreover, as a distributed database, Mnesia only provides two extreme forms of consistency guarantee: transactions and weak consistency. Existing solutions to this problem are either external libraries or commercial standalone products, none of which is integrated into Mnesia natively. This means Erlang developers often have to introduce new dependencies into their codebase or resort to less ideal alternative databases. ...

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

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. We will show that they are equivalent to each other by working on an example. ...