MirageOS retreat in October

After 2.5 years of silent period due to Covid 19, we re-started the MirageOS retreats in early October 2022. This time 15 people gathered in Mirleft (southern Morocco) since it is directly at the sea side, less crowded and stressful than Marrakesh. We had a very nice venue with excellent food and a swimming pool. The group was diverse with the majority from Western Europe, but also attendees from the USA and Nigeria. Some participated for the first time, while others were regular participants. This is great, because it creates a good atmosphere with a shared knowledge of organization, i.e. that we have a daily circle, we do our own dishes, the network setup is run by MirageOS unikernels.

The journey to Mirleft is slightly longer than to Marrakesh, a large group met a day earlier in Agadir and shared a 2.5 hours Taxi ride 130km south. Another group met in the afternoon in Agadir and did the same trip. There is as well public transport by bus every other day to Marrakesh, which some people took on the way back.

The great food and local organization was done again by our hosts who are usually in Marrakesh, but who were happy to host us in Mirleft. Big thanks to the Queens collective.

We plan to have again more regular retreats in the future, they will be announced on the MirageOS developer mailing list, and likely on the discussion forum, and on the retreat website.

Network setup

Once again we used a 4G modem as uplink. One gigabyte of data was 10 Dirham (roughly one Euro), which we collected when the data volume was close to being exceeded. The 4G connectivity was much better than in Marrakesh, likely due to less congestion on the countryside. An APU (tiny x86 computer from PC Engines APU with a serial connection) running FreeBSD was at the heart of our network: the 4G modem was connected via USB, and some TP link access points for wireless connectivity. The routing and network address translation (NAT), which allowed all the laptops and mobile phones to connect to the Internet via the 4G modem was done by the FreeBSD host system (due to lack of a unikernel just doing this, something to prepare for the next event).

For network address configuration and domain name resolution we used DNS Vizor, a MirageOS unikernel on the FreeBSD system with solo5 hvt. We also deployed two other MirageOS unikernels: a local bob relay for sharing files, and used a local opam mirror to reduce our bandwidth use.

While the retreat developed, the DNS resolution was not very stable since the resolver on the 4G modem was sometimes overloaded by lots of requests via a single TCP connection. In the first days we developed UDP support for the MirageOS dns-client and the local connectivity experience greatly improved.

Day to day activities

Apart from talking to old and new friends face-to-face, which we haven't done for some time, we also worked on various projects to improve the MirageOS ecosystem. Below is a collection of projects that wouldn't come to existance without the retreat. Please excuse if there's some project missing.

In the day time we discussed various topics, including performance considerations and how to write protocol implementations with GADTs. Next to that people were going to the beach, while others were pairing up for some projects or reading code together. Others worked alone on finishing some code, but whenever a question of another library appeared, it was easy to approach the original author or someone who has used that library extensively and discuss some questions. In the evenings we had some impromptu talks about various topics, such as the opam repository CI, Lwt do's and dont's, BGP, monitoring, Raspberry pi PWM.

One afternoon we did a long dragon dreaming session to figure out the ideas and dreams for the future of MirageOS. Apart from bare-metal and MirageOS as hypervisor, we also dreamed about running your own digital infrastructure with MirageOS (with increased decentralization and security). Another afternoon we had a cocktail party at the pool.

Some participants already wrote articles about their journey and activities, take a look at their writings: Raphaël Proust, Jules, Sayo, Enguerrand, Sonja, Jan, Lucas, Pierre.

OCaml 5 support

OCaml 5 will soon be published, which has most of the runtime code being rewritten. The runtime also has many more dependencies. We worked on getting ocaml-solo5 (the piece consisting of a math library, a C library, and the OCaml compiler for MirageOS unikernels) to use OCaml 5. This is still work in progress, but already lead to some upstream PRs that are merged into the 5 branch as well.

A Verified File System for MirageOS

FSCQ is a formally verified file system developed in the Coq proof assistant. So far MirageOS has a variety of read/write file systems: chamelon (LittleFS) tar (append-only), fat (FAT16 with its limitations), and one file FS (supporting only one file). We wanted to add FSCQ to the list, by making it usable from MirageOS (currently it compiles to Haskell code).

At the retreat, we first repaired some FSCQ proofs to work with recent Coq releases, and then added OCaml wrapper code and revised the OCaml extraction. The current state is that the most obvious bugs have been fixed, the filesystem is usable from FUSE and underwent basic testing, but performance needs to be improved. FSCQ was developed with lazyness in mind targeting Haskell; for instance, it uses lots of lists in a way that does not go well with OCaml's strict evaluation. The progress is tracked in this issue.

Uint128

A long-standing issue in our IP address library is to use a different memory presentation for IPv6 addresses. As foundation we developed a uintb128 package.

Qubes firewall

Originally developed in 2016, over the last months we revived the QubesOS (an OS that executes applications each in a separate virtual machine for improved security) MirageOS firewall and removed mutable state and improved performance. Read more in Pierre's article.

Music bare-metal on Raspberry Pi 4

Based on gilbraltar (which now works with newer gcc versions), a jack port driver was developed. With this program we now listen to music with MirageOS all day and night. Read further in Tarides blog We also made some music and recorded an EP, read further in Tarides blog.

HTTP client for MirageOS

The earlier mentioned opam mirror contained a HTTP client (using HTTP/AF and H2, supporting both HTTP1 and HTTP2 and also IPv4 and IPv6) to download archives - and we had similar code in other projects. That's why we decided to create the http-mirage-client opam package to reuse that code.

DNS resolver with filtering advertisement

This package is already picked up and used by Mirage Hole, a DNS stub resolver that filters advertisement domains (based on a domain lists downloaded via HTTP using the above HTTP client), which was developed from scratch in Mirleft. Read further in Tarides blog.

Albatross meets NixOS

Albatross is an orchestration system for MirageOS unikernels using solo5 (spt or hvt). Apart from console output, statistics, and resource policies, it supports remote management using TLS. Now albatross supports NixOS and there is a tutorial how to set it up. Read further in Tarides blog.

Memory leaks

We chased some memory leaks on this website, using Grafana and mirage-monitoring. This lead to a PR in paf. We are still investigating another memory issue. Read further details in Tarides blog.

Opam cache

Apart from the opam mirror, sometimes only the caching part is very useful, especially since the git interaction is quite expensive for the network and CPU. We developed a cache-only version in a branch.

Fixing the DNS resolver in the mirage tool

The default DNS resolver in MirageOS is uncensoreddns, which discontinued plaintext DNS requests and replies, and instead supports DNS-over-TLS. We fixed our code to delay parsing of nameservers and update the mirage tool. Now, with the release 4.3.1, name resolution with conduit's resolver works fine again.

Caqti and pgx

We conducted some work on integrating the pure OCaml PostgreSQL client pgx with caqti.

Lwt

Quite some discussion was for how to use exceptions in lwt, leading to a proposed PR not to capture out of memory and stack overflow exceptions, and export reraise. Read further in Raphaël's blog.

Tarides Map

A map showing the geographic distribution of Tarides collaborators was developed as a unikernel, see the code. Read further in Tarides blog article.

Slack bot

The coffee chat bot earlier worked as an executable on Unix, now it can be executed as a MirageOS unikernel. Read further in Tarides blog article.