Christian Kissig

A Contract says more than a Verdict

Rust’s memory model, litmus tests, and concurrency tools — towards code patterns correct by design

Fri 30 Oct 2026 - 29 minutes read

In a post following up from the introduction of the Relaxed Memory Model Zoo, I run the litmus tests from the Zoo’s corpus through Rust the common concurrency tools Miri and loom. The search yields a gap between the tooling and the “memory model” as documented. This may be fine today, as neither the compiler frontend as implemented today nor common target architectures will produce the bug, but any layer of the stack exhausting its liberties will make the gap bite.

What Mojo's Optimiser Leaves Out

A first look at the compiler and some learnings about Mojo’s design choices

Thu 20 Aug 2026 - 18 minutes read

Modular open-sourced Mojo this week — the language that promises the ease-of-use of Python with the performance of C++. That performance has to come from somewhere, and the compiler is where to look for it. So I read the optimiser: which passes it runs, which it pointedly does not, and what that choice suggests about where Mojo goes next.

The Relaxed Memory Model Zoo

Mapping the space of weak memory models

Sat 15 Aug 2026 - 28 minutes read

Comparing two memory models means reading two papers and reconstructing a containment argument nobody wrote down. The Relaxed Memory Model Zoo is a map of 101 models and 145 relations where every edge states how it is known — machine-run litmus test, by construction, or cited — and a consistency gate refuses to ship a map that contradicts itself. This post covers the motivation, the evidence discipline, how the dataset was built (including where AI was used and where it was not trusted), the principles that kept it small, and how to submit corrections. A follow-up post will use the same litmus tests to locate real Rust in the lattice.

Mitigating ABA for Compare-and-Swap: a Survey

Fri 6 Sep 2024 - 10 minutes read

Compare-and-swap (CAS) is a central part of many implementations of lock-free algorithms synchronizing values in shared data structures. Without further scaffolding, CAS is inherently prone to the ABA problem. In this post I survey solutions mitigating ABA in the context of CAS towards a high-level classification.