Thomas Leonard's blog

I've been investigating how keyboards, mice, etc work in Linux.

The TLA Toolbox now has support for proving liveness properties (i.e. that something will eventually happen).

Linux provides the KMS (Kernel Mode Setting) API to let applications query and configure display settings.

I convert my Vulkan test program from C to OCaml and compare the results, then continue the Vulkan tutorial in OCaml, adding 3D, textures and depth buffering.

I learn how to draw a triangle with a GPU, and then trace the code to find out how the graphics system works (or doesn't), looking at Mesa3D, GLFW, OpenGL, Vulkan, Wayland and Linux DRM.

Tamarin is a tool for checking cryptographic security protocols (such as TLS or WireGuard).

The last post looked at using various tools to understand why an OCaml 5 program was waiting a long time for IO.

Linux and OCaml provide a huge range of tools for investigating performance problems.

"Is this software safe?"

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.

I've been running QubesOS as my main desktop since 2015.

In this post I describe three approaches to building a language for writing CI/CD pipelines.

The vchan protocol is used to stream data between virtual machines on a Xen host without needing any locks.

QubesOS provides a desktop operating system made up of multiple virtual machines, running under Xen.

In CueKeeper: Gitting Things Done in the browser, I wrote about CueKeeper, a Getting Things Done application that runs client-side in your browser.

Git repositories store data with history, supporting replication, merging and revocation.

Back in July, I used MirageOS to create my first unikernel, a simple REST service for queuing file uploads, deployable as a virtual machine.

Many asynchronous programs make use of promises (also known as using light-weight threads or an asynchronous monad) to manage concurrency.

After converting 0install to OCaml, I've been looking at using more of OCaml's features to further clean up the APIs.

After creating my REST queuing service as a Mirage unikernel, I reported that it could serve the data at 2.46 MB/s from my ARM CubieTruck dev board.