francesco 🍥

@francesco
232 Followers
57 Following
22 Posts
bloghttps://mazzo.li/archive.html
twitterhttps://twitter.com/trascendentale
githubhttps://github.com/bitonic/
francesco 🍥Sep 18, 2025
I'm delighted to announce that we've open sourced the distributed filesystem we've been working on at XTX for the past three years! You can read about its design at https://www.xtxmarkets.com/tech/2025-ternfs/ .
TernFS: an exabyte scale, multi-region distributed filesystem | XTX Tech Blog

XTX Markets is a leading algorithmic trading firm which uses state-of-the-art machine learning technology to produce price forecasts for over 50,000 financial instruments across equities, fixed income, currencies, commodities and crypto. It uses those forecasts to trade on exchanges and alternative trading venues, and to offer differentiated liquidity directly to clients worldwide. The firm trades over $250bn a day across 35 countries and has over 250 employees based in London, Singapore, New York, Paris, Bristol, Mumbai, Yerevan and Kajaani.

francesco 🍥Jun 23, 2025

I spent a good few hours figuring out under which conditions storing Go pointers in assembly is safe. Here's a little explainer: https://mazzo.li/posts/go-asm-pointers.html

#go #assembly

How to store Go pointers from assembly

The standard Go toolchain comes with an assembler out of the box. Said assembler is highly idiosyncratic, using syntax inherited from Plan 9 and choosing its own names for platform-specific instructions and registers. But it's great to have it readily available. More mundanely, Go comes with a garbage collector. This post explains how to make these two components play nice, if we want to manipulate Go pointers from our assembly.

francesco 🍥Jun 9, 2025

Cooked up this abomination at ZuriHac 2025 -- execute Verilog circuits right from your Haskell! All the blame for the idea goes to @kmett https://mazzo.li/posts/inline-verilog.html

#haskell #verilog

Show threadfrancesco 🍥Sep 24, 2024
@shachaf @pkhuong and note that io_uring works through the futex2 API, so you can wait on multiple futexes with a single io_uring submission, if you so wish.
francesco 🍥Sep 22, 2024
I've long wanted to wait on file descriptors and futexes at the same time. I've recently realized that it is now possible through io_uring: https://mazzo.li/posts/uring-multiplex.html
Waiting for many things at once with `io_uring`

When doing systems programming we often need to wait for something to happen. Common examples might be waiting for some data to come through a socket or waiting on a lock. We also often want to wait on any of several conditions to become true. A web server might be handling many sockets at once, waiting for any number of them to become readable or writeable. This short blog post is concerned with the latter scenario in Linux. Until recently there was no generic framework which allowed us to wait on many arbitrary events, but now there is, thanks to `io_uring`.

Show threadfrancesco 🍥Jul 13, 2024

@zeux The reason why it's not the default is that it only works if you haven't fetched the remote ref, and is therefore deemed a somewhat dangerous option since many tools automatically fetch (i.e. VSCode) defeating the purpose of --force-with-lease.

Or at least, that's the answer I was given when I tried to add a config option to make it the default: https://lore.kernel.org/git/xmqqvan8jd[email protected]/ .

Re: [PATCH] push: add config option to --force-with-lease by default. - Junio C Hamano

Show threadfrancesco 🍥Jul 8, 2024
@pervognsen I'm not really saying that the Coq way is worse than the Agda way btw -- if anything tacticts seem to be winning (although I'm not up to speed with recent developments). But they are radically different approaches to elaboration.
Show threadfrancesco 🍥Jul 8, 2024
@pervognsen On the other hand the Agda/Epigram tradition is about surfacing elaboration in some way -- i.e. dependent pattern matching. In that context it turns out that most elaboration can be reduced to higher order unification, see https://arxiv.org/pdf/1609.09709 . So that might give you a sense in which elaboration itself can be fit into a single framework, which might or might not satisfy you :).
Show threadfrancesco 🍥Jul 8, 2024
@pervognsen "elaboration" means very different things in different dependently typed languages. The Coq tradition is mostly about having tactics to vomit out some script which proves what you want to prove (and I guess this is the "elaboration" you're talking about).
francesco 🍥Jul 1, 2024

Two more distributed filesystem themed blog posts:

* One on how to use CRCs and Reed-Solomon coding together effectively: https://mazzo.li/posts/rs-crc.html
* Another to explain how to implement the CRC functions mentioned in the first: https://mazzo.li/posts/crc-tips.html

These tie together with my previous post on distributed transactions ( https://mazzo.li/posts/mac-distributed-tx.html ). More posts will probably be coming on the same topic :).

CRCs and Reed-Solomon coding: better together

In my latest filesystem-themed post I discussed a technique to perform distributed resource management more safely. This time I'll explain how one might effectively combine _Reed-Solomon coding_ and _cyclic redundancy checks_. The first gives us redundancy (we can lose disks and still recover our data), the second protects us against data corruption.