Thomas Leonard's blog

OCaml 5 Performance Part 2

The last post looked at using various tools to understand why an OCaml 5 program was waiting a long time for IO. In this post, I'll be trying out some tools to investigate a compute-intensive program that uses multiple CPUs.

OCaml 5 Performance Problems

Linux and OCaml provide a huge range of tools for investigating performance problems. In this post I try using some of them to understand a network performance problem. In part 2, I'll investigate a problem in a CPU-intensive multicore program.

Lambda Capabilities

"Is this software safe?" is a question software engineers should be able to answer, but doing so can be difficult. Capabilities offer an elegant solution, but seem to be little known among functional programmers. This post is an introduction to capabilities in the context of ordinary programming (using plain functions, in the style of the lambda calculus).

Isolating Xwayland in a VM

In my last post, Qubes-lite with KVM and Wayland, I described setting up a Qubes-inspired Linux system that runs applications in virtual machines. A Wayland proxy running in each VM connects its applications to the host Wayland compositor over virtwl, allowing them to appear on the desktop alongside normal host applications. In this post, I extend this to support X11 applications using Xwayland.

Qubes-lite with KVM and Wayland

I've been running QubesOS as my main desktop since 2015. It provides good security, by running applications in different Xen VMs. However, it is also quite slow and has some hardware problems. I've recently been trying out NixOS, KVM, Wayland and SpectrumOS, and attempting to create something similar with more modern/compatible/faster technology.

This post gives my initial impressions of these tools and describes my current setup.

CI/CD Pipelines: Monad, Arrow or Dart?

In this post I describe three approaches to building a language for writing CI/CD pipelines. My first attempt used a monad, but this prevented static analysis of the pipelines. I then tried using an arrow, but found the syntax very difficult to use. Finally, I ended up using a light-weight alternative to arrows that I will refer to here as a dart (I don't know if this has a name already). This allows for static analysis like an arrow, but has a syntax even simpler than a monad.

Using TLA+ to Understand Xen Vchan

The vchan protocol is used to stream data between virtual machines on a Xen host without needing any locks. It is largely undocumented. The TLA Toolbox is a set of tools for writing and checking specifications. In this post, I'll describe my experiences using these tools to understand how the vchan protocol works.

A Unikernel Firewall for QubesOS

QubesOS provides a desktop operating system made up of multiple virtual machines, running under Xen. To protect against buggy network drivers, the physical network hardware is accessed only by a dedicated (and untrusted) "NetVM", which is connected to the rest of the system via a separate (trusted) "FirewallVM". This firewall VM runs Linux, processing network traffic with code written in C.

In this blog post, I replace the Linux firewall VM with a MirageOS unikernel. The resulting VM uses safe (bounds-checked, type-checked) OCaml code to process network traffic, uses less than a tenth of the memory of the default FirewallVM, boots several times faster, and should be much simpler to audit or extend.

CueKeeper Internals: Experiences with Irmin, React, TyXML and IndexedDB

In CueKeeper: Gitting Things Done in the browser, I wrote about CueKeeper, a Getting Things Done application that runs client-side in your browser. It stores your actions in a Git-like data-store provided by Irmin, allowing you to browse the history, revert changes, and sync (between tabs and, once the server backend is available, between devices). Several people asked about the technologies used to build it, so that's what this blog will cover.

CueKeeper: Gitting Things Done in the Browser

Git repositories store data with history, supporting replication, merging and revocation. The Irmin library lets applications use Git-style storage for their data. To try it out, I've written a GTD-based action tracker that runs entirely client-side in the browser.

CueKeeper uses Irmin to handle history and merges, with state saved in the browser using the new IndexedDB standard (requires a recent browser; Firefox 37, Chromium 41 and IE 11.0.9600 all work, but Safari apparently has problems if you open the page in multiple tabs).