I've been investigating how keyboards, mice, etc work in Linux. In this blog post we'll see how input events work, using libinput-ocaml, and then use that to write a little game. Using libinput-ocaml to make a game Table of Contents Device files Using devices directly Permissions libinput Getting a REPL Opening devices with libinput Thoughts on the C bindings Lander game Non-libinput aspects of…
The TLA Toolbox now has support for proving liveness properties (i.e. that something will eventually happen). I try it out on the Xen vchan protocol. Working on a liveness proof with the TLA+ Toolbox. Table of Contents Background A simple channel specification Specification in terms of actions Invariants Temporal logic Proving temporal claims with TLAPS Generalising Hiding definitions Proving…
Linux provides the KMS (Kernel Mode Setting) API to let applications query and configure display settings. It's used by Wayland compositors and other programs that need to configure the hardware directly. I found the C API a little verbose and hard to follow so I made libdrm-ocaml , which lets us run commands interactively in a REPL. We'll start by discovering what hardware is available and how…
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. Table of Contents Introduction Running it yourself The direct port Labelled arguments Enums and bit-fields Optional fields Loading shaders Logging Error handling Refactored version Olivine wrappers Using fibers / effects for control flow…
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. Table of Contents Introduction Overview OpenGL Vulkan Synchronisation First attempt at tracing Removing GLFW Removing Vulkan's Wayland extension Wayland walk-through Kernel details with bpftrace Start-up and…
Tamarin is a tool for checking cryptographic security protocols (such as TLS or WireGuard). In this post, I try it out on some (very old, but simple) protocols from Applied Cryptography . Table of Contents Introduction Key Exchange with Symmetric Cryptography Checking it's usable Checking it's secure Key Exchange with Public-Key Cryptography Interlock Protocol Key and Message Transmission Fixing…
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. Table of Contents The problem ThreadSanitizer perf mpstat offcputime The OCaml garbage collector statmemprof magic-trace Tuning GC parameters Simplifying further perf sched…
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. Table of Contents The problem time eio-trace strace bpftrace tcpdump ss offwaketime magic-trace Summary script Fixing it Conclusions The problem While…
"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). Even if you're not interested in…
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.…
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…
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…
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. Table of Contents Background Qubes and the vchan protocol TLA+ Is TLA useful? Basic…
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…
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…
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…
Back in July, I used MirageOS to create my first unikernel , a simple REST service for queuing file uploads, deployable as a virtual machine. While a traditional VM would be a complete Linux system (kernel, init system, package manager, shell, etc), a Mirage unikernel is a single OCaml program which pulls in just the features (network driver, TCP stack, web server, etc) it needs as libraries. Now…
Many asynchronous programs make use of promises (also known as using light-weight threads or an asynchronous monad ) to manage concurrency. I've been working on tools to collect trace data from such programs and visualise the results, to help with profiling and debugging. The diagram below shows a trace from a Mirage unikernel reading data from disk in a loop. You should be able to pan around by…
After converting 0install to OCaml , I've been looking at using more of OCaml's features to further clean up the APIs. In this post, I describe how using OCaml functors has made 0install's dependency solver easier to understand and more flexible. ( this post also appeared on Hacker News and Reddit ) Table of Contents Introduction How dependency solvers work Optimising the result The current solver…
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. That's fast enough for my use (it's faster than my Internet connection), but I was curious why it was slower than the Linux guest, which serves files with nc at 20 MB/s. ( this post also appeared on Hacker News and Reddit ) Table of Contents The TCP…