Consistency models, from linearisable to eventual

Python 3.14 · main.py

# A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
# So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
from collections.abc import Callable

HISTORIES = [
    "A.w1 0-2, B.r1 3-4",
    "A.w1 0-2, B.r0 3-4",
    "A.w1 0-6, B.r0 1-2, C.r1 3-5",
    "A.w1 0-6, B.r1 1-2, C.r0 3-4",
    "A.w1 0-1, A.r0 2-3",
    "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
]
Rule = Callable[[str, str], bool]  # whether operation a must come before operation b
MODELS: list[tuple[str, Rule]] = [
    ("linearisable: ", lambda a, b: a[7] < b[5]),  # a returned before b was invoked
    ("sequential:   ", lambda a, b: a[0] == b[0] and a[5] < b[5]),  # same client
]


def order(ops: list[str], first: Rule, value: str = "0") -> list[str] | None:
    """An order that keeps the rule, in which each read returns the latest write."""
    if not ops:
        return []
    for op in ops:
        rest = [o for o in ops if o != op]
        if any(first(o, op) for o in rest) or (op[2] == "r" and op[3] != value):
            continue
        tail = order(rest, first, op[3])
        if tail is not None:
            return [op[:4], *tail]
    return None


for n, history in enumerate(HISTORIES, 1):
    print(f"{n}. {history}")
    for label, first in MODELS:
        found = order(history.split(", "), first)
        print("   " + label + ("no" if found is None else " -> ".join(found)))

In Python: An operation is its notation, so op[3] is the value and op[5] and op[7] the times, and the two models are lambdas in a list of pairs.

Recorded with CPython 3.14.8 on macOS 26 arm64. It runs in your browser with Pyodide 314.0.7 (CPython 3.14.2). To run it yourself: python3 main.py

JavaScript Node 24 · main.mjs

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
const HISTORIES = [
  "A.w1 0-2, B.r1 3-4",
  "A.w1 0-2, B.r0 3-4",
  "A.w1 0-6, B.r0 1-2, C.r1 3-5",
  "A.w1 0-6, B.r1 1-2, C.r0 3-4",
  "A.w1 0-1, A.r0 2-3",
  "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
];
// Whether operation a must come before operation b.
const MODELS = [
  ["linearisable: ", (a, b) => a[7] < b[5]], // a returned before b was invoked
  ["sequential:   ", (a, b) => a[0] === b[0] && a[5] < b[5]], // same client
];

// An order that keeps the rule, in which each read returns the latest write, or null.
function order(ops, first, value = "0") {
  if (ops.length === 0) return [];
  for (const op of ops) {
    const rest = ops.filter((o) => o !== op);
    if (rest.some((o) => first(o, op)) || (op[2] === "r" && op[3] !== value)) continue;
    const tail = order(rest, first, op[3]);
    if (tail !== null) return [op.slice(0, 4), ...tail];
  }
  return null;
}

HISTORIES.forEach((history, i) => {
  console.log(`${i + 1}. ${history}`);
  for (const [label, first] of MODELS) {
    const found = order(history.split(", "), first);
    console.log(`   ${label}${found === null ? "no" : found.join(" -> ")}`);
  }
});

In JavaScript: The rules compare one-character strings, which order like the digits they hold, and order returns null when no order exists.

Recorded with Node.js 24.21.0 LTS (V8 13.6) on macOS 26 arm64. It runs in your browser with QuickJS (quickjs-emscripten 0.32.0). To run it yourself: node main.mjs

Java 25 LTS · Main.java

import java.util.ArrayList;
import java.util.List;
import java.util.function.BiPredicate;

public class Main {
  // A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
  // So op.charAt(0) is the client, 2 is w or r, 3 the value, 5 and 7 the times.
  static final String[] HISTORIES = {
    "A.w1 0-2, B.r1 3-4",
    "A.w1 0-2, B.r0 3-4",
    "A.w1 0-6, B.r0 1-2, C.r1 3-5",
    "A.w1 0-6, B.r1 1-2, C.r0 3-4",
    "A.w1 0-1, A.r0 2-3",
    "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
  };

  // first.test(a, b): whether operation a must come before operation b.
  record Model(String label, BiPredicate<String, String> first) {}

  static final List<Model> MODELS =
      List.of(
          // a returned before b was invoked
          new Model("linearisable: ", (a, b) -> a.charAt(7) < b.charAt(5)),
          // the same client invoked a first
          new Model(
              "sequential:   ", (a, b) -> a.charAt(0) == b.charAt(0) && a.charAt(5) < b.charAt(5)));

  // An order that keeps the rule, in which each read returns the latest write, or null.
  static List<String> order(List<String> ops, BiPredicate<String, String> first, char value) {
    if (ops.isEmpty()) {
      return new ArrayList<>();
    }
    for (String op : ops) {
      List<String> rest = ops.stream().filter(o -> !o.equals(op)).toList();
      if (rest.stream().anyMatch(o -> first.test(o, op))
          || (op.charAt(2) == 'r' && op.charAt(3) != value)) {
        continue;
      }
      List<String> tail = order(rest, first, op.charAt(3));
      if (tail != null) {
        tail.add(0, op.substring(0, 4));
        return tail;
      }
    }
    return null;
  }

  public static void main(String[] args) {
    for (int n = 0; n < HISTORIES.length; n++) {
      System.out.println((n + 1) + ". " + HISTORIES[n]);
      for (Model model : MODELS) {
        List<String> found = order(List.of(HISTORIES[n].split(", ")), model.first(), '0');
        System.out.println(
            "   " + model.label() + (found == null ? "no" : String.join(" -> ", found)));
      }
    }
  }
}

In Java: Each model is a record holding a BiPredicate, and charAt reads the client, the value and the times from the notation.

Recorded with OpenJDK 25.0.4.1 LTS (Eclipse Temurin) on macOS 26 arm64. It runs in your browser with a TeaVM 0.16.0 build in QuickJS (quickjs-emscripten 0.32.0). To run it yourself: java Main.java

C++23 · main.cpp

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the
// register starts at 0. So op[0] is the client, op[2] w or r, op[3] the value,
// op[5] and op[7] the times.
#include <algorithm>
#include <functional>
#include <optional>
#include <print>
#include <ranges>
#include <string>
#include <string_view>
#include <utility>
#include <vector>

using Ops = std::vector<std::string_view>;
// Whether operation a must come before operation b.
using Rule = std::function<bool(std::string_view a, std::string_view b)>;

// An order that keeps the rule, in which each read returns the latest write.
std::optional<Ops> order(const Ops &ops, const Rule &first, char value = '0') {
  if (ops.empty())
    return Ops{};
  for (const std::string_view op : ops) {
    Ops rest = ops;
    std::erase(rest, op);
    if (std::ranges::any_of(rest, [&](auto o) { return first(o, op); }) ||
        (op[2] == 'r' && op[3] != value))
      continue;
    if (auto tail = order(rest, first, op[3])) {
      tail->insert(tail->begin(), op.substr(0, 4));
      return tail;
    }
  }
  return std::nullopt;
}

int main() {
  const std::vector<std::string_view> histories = {
      "A.w1 0-2, B.r1 3-4",
      "A.w1 0-2, B.r0 3-4",
      "A.w1 0-6, B.r0 1-2, C.r1 3-5",
      "A.w1 0-6, B.r1 1-2, C.r0 3-4",
      "A.w1 0-1, A.r0 2-3",
      "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
  };
  const std::vector<std::pair<std::string_view, Rule>> models = {
      // a returned before b was invoked
      {"linearisable: ", [](auto a, auto b) { return a[7] < b[5]; }},
      // the same client invoked a first
      {"sequential:   ",
       [](auto a, auto b) { return a[0] == b[0] && a[5] < b[5]; }}};
  for (std::size_t n = 0; n < histories.size(); n++) {
    std::println("{}. {}", n + 1, histories[n]);
    Ops ops;
    for (const auto part :
         std::views::split(histories[n], std::string_view(", ")))
      ops.emplace_back(part.begin(), part.end());
    for (const auto &[label, first] : models) {
      std::string line;
      if (const auto found = order(ops, first))
        for (const std::string_view name : *found)
          line += (line.empty() ? "" : " -> ") + std::string(name);
      std::println("   {}{}", label, line.empty() ? "no" : line);
    }
  }
}

In C++: The operations are std::string_view slices of the history, std::views::split cuts it at ", ", and order returns std::optional.

Recorded with Apple clang 21.0.0 (C++23) and GCC 16.2.0 on macOS 26 arm64. It runs in your browser with Clang in WebAssembly (YoWASP) 22.0.0-git20542-10. To run it yourself: clang++ -std=c++23 -O2 -Wall -Wextra -Werror -pedantic -fsanitize=address,undefined main.cpp -o main && ./main

C# 14 · .NET 10 · app.cs

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
string[] histories =
[
    "A.w1 0-2, B.r1 3-4",
    "A.w1 0-2, B.r0 3-4",
    "A.w1 0-6, B.r0 1-2, C.r1 3-5",
    "A.w1 0-6, B.r1 1-2, C.r0 3-4",
    "A.w1 0-1, A.r0 2-3",
    "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
];
// Whether operation a must come before operation b.
(string Label, Func<string, string, bool> First)[] models =
[
    ("linearisable: ", (a, b) => a[7] < b[5]), // a returned before b was invoked
    ("sequential:   ", (a, b) => a[0] == b[0] && a[5] < b[5]), // same client
];

for (int n = 0; n < histories.Length; n++)
{
    Console.WriteLine($"{n + 1}. {histories[n]}");
    foreach (var (label, first) in models)
    {
        var found = Order([.. histories[n].Split(", ")], first, '0');
        Console.WriteLine("   " + label + (found is null ? "no" : string.Join(" -> ", found)));
    }
}

// An order that keeps the rule, in which each read returns the latest write, or null.
static List<string>? Order(List<string> ops, Func<string, string, bool> first, char value)
{
    if (ops.Count == 0)
    {
        return [];
    }
    foreach (string op in ops)
    {
        List<string> rest = [.. ops.Where(o => o != op)];
        if (rest.Any(o => first(o, op)) || (op[2] == 'r' && op[3] != value))
        {
            continue;
        }
        if (Order(rest, first, op[3]) is { } tail)
        {
            return [op[..4], .. tail];
        }
    }
    return null;
}

In C#: The models are tuples of a label and a Func, and the pattern is { } tail names the order only when one was found, because { } matches any value that is not null.

Recorded with C# 14 on .NET 10.0.12 (SDK 10.0.401) on macOS 26 arm64. It runs in your browser with the .NET runtime for WebAssembly 10.0.12. To run it yourself: dotnet run app.cs

C23 · main.c

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the
// register starts at 0. So op[0] is the client, op[2] w or r, op[3] the value,
// op[5] and op[7] the times.
#include <stdbool.h>
#include <stdio.h>
#include <string.h>

static const char *const histories[] = {
    "A.w1 0-2, B.r1 3-4",
    "A.w1 0-2, B.r0 3-4",
    "A.w1 0-6, B.r0 1-2, C.r1 3-5",
    "A.w1 0-6, B.r1 1-2, C.r0 3-4",
    "A.w1 0-1, A.r0 2-3",
    "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5"};

// Whether operation a must come before operation b.
typedef bool Rule(const char *a, const char *b);
static bool real_time(const char *a, const char *b) { return a[7] < b[5]; }
static bool same_client(const char *a, const char *b) {
  return a[0] == b[0] && a[5] < b[5];
}

// Puts into found[depth..] an order of the operations not in used that keeps
// the rule, in which each read returns the latest write.
static bool order(const char **ops, int n, Rule *first, unsigned used,
                  int depth, char value, const char **found) {
  if (depth == n)
    return true;
  for (int i = 0; i < n; i++) {
    bool waits = used >> i & 1 || (ops[i][2] == 'r' && ops[i][3] != value);
    for (int j = 0; j < n && !waits; j++)
      waits = j != i && !(used >> j & 1) && first(ops[j], ops[i]);
    found[depth] = ops[i];
    if (!waits &&
        order(ops, n, first, used | 1u << i, depth + 1, ops[i][3], found))
      return true;
  }
  return false;
}

static void show(const char *label, const char **ops, int n, Rule *first) {
  const char *found[6];
  printf("   %s", label);
  if (!order(ops, n, first, 0, 0, '0', found)) {
    printf("no\n");
    return;
  }
  for (int i = 0; i < n; i++)
    printf("%s%.4s", i ? " -> " : "", found[i]);
  printf("\n");
}

int main(void) {
  for (int h = 0; h < 6; h++) {
    printf("%d. %s\n", h + 1, histories[h]);
    const char *ops[6];
    int n = 0;
    for (const char *p = histories[h]; p; p = strchr(p, ',')) {
      if (*p == ',')
        p += 2;
      ops[n++] = p;
    }
    show("linearisable: ", ops, n, real_time);
    show("sequential:   ", ops, n, same_client);
  }
}

In C: Each operation is a pointer into its history string, used marks the operations placed as bits, and found collects the order.

Recorded with Apple clang 21.0.0 (C23) and GCC 16.2.0 on macOS 26 arm64. It runs in your browser with Clang in WebAssembly (YoWASP) 22.0.0-git20542-10. To run it yourself: clang -std=c23 -O2 -Wall -Wextra -Werror -pedantic -fsanitize=address,undefined main.c -o main && ./main

PHP 8.5 · main.php

<?php

declare(strict_types=1);

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So $op[0] is the client, $op[2] w or r, $op[3] the value, $op[5] and $op[7] the times.
const HISTORIES = [
    'A.w1 0-2, B.r1 3-4',
    'A.w1 0-2, B.r0 3-4',
    'A.w1 0-6, B.r0 1-2, C.r1 3-5',
    'A.w1 0-6, B.r1 1-2, C.r0 3-4',
    'A.w1 0-1, A.r0 2-3',
    'A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5',
];

/**
 * An order that keeps the rule, in which each read returns the latest write, or null.
 *
 * @param list<string> $ops
 * @param callable(string, string): bool $first
 * @return list<string>|null
 */
function order(array $ops, callable $first, string $value = '0'): ?array
{
    if ($ops === []) {
        return [];
    }
    foreach ($ops as $op) {
        $rest = array_values(array_filter($ops, fn(string $o): bool => $o !== $op));
        $waits = array_filter($rest, fn(string $o): bool => $first($o, $op)) !== [];
        if ($waits || ($op[2] === 'r' && $op[3] !== $value)) {
            continue;
        }
        $tail = order($rest, $first, $op[3]);
        if ($tail !== null) {
            return [substr($op, 0, 4), ...$tail];
        }
    }
    return null;
}

// Whether operation $a must come before operation $b.
$models = [
    // a returned before b was invoked
    'linearisable: ' => fn(string $a, string $b): bool => $a[7] < $b[5],
    // the same client invoked a first
    'sequential:   ' => fn(string $a, string $b): bool => $a[0] === $b[0] && $a[5] < $b[5],
];
foreach (HISTORIES as $n => $history) {
    echo ($n + 1) . ". {$history}\n";
    foreach ($models as $label => $first) {
        $found = order(explode(', ', $history), $first);
        echo "   {$label}" . ($found === null ? 'no' : implode(' -> ', $found)) . "\n";
    }
}

In PHP: The models are arrow functions keyed by their label, and $a[7] < $b[5] compares numeric strings as numbers.

Recorded with PHP 8.5.11 (CLI) on macOS 26 arm64. It runs in your browser with php-wasm 0.2.0 (PHP 8.5.2). To run it yourself: php main.php

Rust 1.99 · main.rs

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
const HISTORIES: [&str; 6] = [
    "A.w1 0-2, B.r1 3-4",
    "A.w1 0-2, B.r0 3-4",
    "A.w1 0-6, B.r0 1-2, C.r1 3-5",
    "A.w1 0-6, B.r1 1-2, C.r0 3-4",
    "A.w1 0-1, A.r0 2-3",
    "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
];

/// Whether operation a must come before operation b.
type Rule = fn(&[u8], &[u8]) -> bool;
const MODELS: [(&str, Rule); 2] = [
    ("linearisable: ", |a, b| a[7] < b[5]), // a returned before b was invoked
    ("sequential:   ", |a, b| a[0] == b[0] && a[5] < b[5]), // same client
];

/// An order that keeps the rule, in which each read returns the latest write.
fn order<'a>(ops: &[&'a str], first: Rule, value: u8) -> Option<Vec<&'a str>> {
    if ops.is_empty() {
        return Some(Vec::new());
    }
    for &op in ops {
        let rest: Vec<&str> = ops.iter().copied().filter(|&o| o != op).collect();
        let b = op.as_bytes();
        if rest.iter().any(|o| first(o.as_bytes(), b)) || (b[2] == b'r' && b[3] != value) {
            continue;
        }
        if let Some(mut tail) = order(&rest, first, b[3]) {
            tail.insert(0, &op[..4]);
            return Some(tail);
        }
    }
    None
}

fn main() {
    for (n, history) in HISTORIES.iter().enumerate() {
        println!("{}. {history}", n + 1);
        let ops: Vec<&str> = history.split(", ").collect();
        for (label, first) in MODELS {
            let found = order(&ops, first, b'0');
            println!(
                "   {label}{}",
                found.map_or("no".to_string(), |names| names.join(" -> "))
            );
        }
    }
}

In Rust: The rules are fn pointers over the notation's bytes, built from closures in a const array, and order returns an Option.

Recorded with rustc 1.99.0 (edition 2024) on macOS 26 arm64. It runs in your browser with a WebAssembly build on the WASI runner (browser_wasi_shim 0.4.2). To run it yourself: rustc --edition 2024 -O main.rs && ./main

TypeScript 6.0 · main.ts

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
const HISTORIES = [
  "A.w1 0-2, B.r1 3-4",
  "A.w1 0-2, B.r0 3-4",
  "A.w1 0-6, B.r0 1-2, C.r1 3-5",
  "A.w1 0-6, B.r1 1-2, C.r0 3-4",
  "A.w1 0-1, A.r0 2-3",
  "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
];
type Rule = (a: string, b: string) => boolean; // whether operation a must come before b
const MODELS: [string, Rule][] = [
  ["linearisable: ", (a, b) => a[7] < b[5]], // a returned before b was invoked
  ["sequential:   ", (a, b) => a[0] === b[0] && a[5] < b[5]], // same client
];

// An order that keeps the rule, in which each read returns the latest write, or null.
function order(ops: string[], first: Rule, value = "0"): string[] | null {
  if (ops.length === 0) return [];
  for (const op of ops) {
    const rest = ops.filter((o) => o !== op);
    if (rest.some((o) => first(o, op)) || (op[2] === "r" && op[3] !== value)) continue;
    const tail = order(rest, first, op[3]);
    if (tail !== null) return [op.slice(0, 4), ...tail];
  }
  return null;
}

HISTORIES.forEach((history, i) => {
  console.log(`${i + 1}. ${history}`);
  for (const [label, first] of MODELS) {
    const found = order(history.split(", "), first);
    console.log(`   ${label}${found === null ? "no" : found.join(" -> ")}`);
  }
});

In TypeScript: Rule is a function type, so both lambdas in MODELS are checked against it, and order returns null when no order exists.

Recorded with TypeScript 6.0.3 (strict), run by Node.js 24.21.0 on macOS 26 arm64. It runs in your browser with QuickJS (quickjs-emscripten 0.32.0) after Sucrase 3.35.1. To run it yourself: npx -p typescript@6.0.3 tsc --noEmit --strict main.ts && node main.ts

Go 1.27 · main.go

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
package main

import (
	"fmt"
	"slices"
	"strings"
)

var histories = []string{
	"A.w1 0-2, B.r1 3-4",
	"A.w1 0-2, B.r0 3-4",
	"A.w1 0-6, B.r0 1-2, C.r1 3-5",
	"A.w1 0-6, B.r1 1-2, C.r0 3-4",
	"A.w1 0-1, A.r0 2-3",
	"A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
}

// A rule says whether operation a must come before operation b.
type rule func(a, b string) bool

var models = []struct {
	label string
	first rule
}{
	// a returned before b was invoked
	{"linearisable: ", func(a, b string) bool { return a[7] < b[5] }},
	// the same client invoked a first
	{"sequential:   ", func(a, b string) bool { return a[0] == b[0] && a[5] < b[5] }},
}

// order finds an order that keeps the rule, in which each read returns the latest write.
func order(ops []string, first rule, value byte) ([]string, bool) {
	if len(ops) == 0 {
		return nil, true
	}
	for i, op := range ops {
		rest := slices.Delete(slices.Clone(ops), i, i+1)
		waits := op[2] == 'r' && op[3] != value
		for _, o := range rest {
			waits = waits || first(o, op)
		}
		if waits {
			continue
		}
		if tail, ok := order(rest, first, op[3]); ok {
			return append([]string{op[:4]}, tail...), true
		}
	}
	return nil, false
}

func main() {
	for n, history := range histories {
		fmt.Printf("%d. %s\n", n+1, history)
		for _, m := range models {
			found, ok := order(strings.Split(history, ", "), m.first, '0')
			result := strings.Join(found, " -> ")
			if !ok {
				result = "no"
			}
			fmt.Println("   " + m.label + result)
		}
	}
}

In Go: order returns the names and a flag, the Go way of saying "found", and slices.Delete on a clone leaves the others.

Recorded with Go 1.27.1 on macOS 26 arm64. It runs in your browser with the Go compiler in WebAssembly 1.27.1. To run it yourself: go run main.go

Swift 6.4 · main.swift

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
let histories = [
  "A.w1 0-2, B.r1 3-4",
  "A.w1 0-2, B.r0 3-4",
  "A.w1 0-6, B.r0 1-2, C.r1 3-5",
  "A.w1 0-6, B.r1 1-2, C.r0 3-4",
  "A.w1 0-1, A.r0 2-3",
  "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
]

/// Whether operation a must come before operation b, each given as its notation's bytes.
typealias Rule = ([UInt8], [UInt8]) -> Bool
let models: [(label: String, first: Rule)] = [
  ("linearisable: ", { a, b in a[7] < b[5] }),  // a returned before b was invoked
  ("sequential:   ", { a, b in a[0] == b[0] && a[5] < b[5] }),  // same client
]

/// An order that keeps the rule, in which each read returns the latest write.
func order(_ ops: [[UInt8]], _ first: Rule, _ value: UInt8 = UInt8(ascii: "0")) -> [String]? {
  if ops.isEmpty {
    return []
  }
  for (i, op) in ops.enumerated() {
    var rest = ops
    rest.remove(at: i)
    if rest.contains(where: { first($0, op) }) || (op[2] == UInt8(ascii: "r") && op[3] != value) {
      continue
    }
    if let tail = order(rest, first, op[3]) {
      return [String(decoding: op[..<4], as: UTF8.self)] + tail
    }
  }
  return nil
}

for (n, history) in histories.enumerated() {
  print("\(n + 1). \(history)")
  let ops = history.split(separator: ",").map { item in Array(item.drop(while: { $0 == " " }).utf8)
  }
  for (label, first) in models {
    print("   " + label + (order(ops, first)?.joined(separator: " -> ") ?? "no"))
  }
}

In Swift: Swift strings have no integer index, so each operation is kept as the bytes of its notation, and order returns an optional.

Recorded with Apple Swift 6.4 on macOS 26 arm64. It runs in your browser with a WebAssembly build on the WASI runner (browser_wasi_shim 0.4.2). To run it yourself: swiftc -O main.swift -o main && ./main

Ruby 4.0 · main.rb

# frozen_string_literal: true

# A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
# So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
HISTORIES = [
  'A.w1 0-2, B.r1 3-4',
  'A.w1 0-2, B.r0 3-4',
  'A.w1 0-6, B.r0 1-2, C.r1 3-5',
  'A.w1 0-6, B.r1 1-2, C.r0 3-4',
  'A.w1 0-1, A.r0 2-3',
  'A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5'
].freeze

# Whether operation a must come before operation b.
MODELS = {
  'linearisable: ' => ->(a, b) { a[7] < b[5] }, # a returned before b was invoked
  'sequential:   ' => ->(a, b) { a[0] == b[0] && a[5] < b[5] } # same client
}.freeze

# Whether an operation may come next: nothing it must follow is left, and a read is current.
def ready?(operation, rest, first, value)
  rest.none? { |o| first.call(o, operation) } && (operation[2] == 'w' || operation[3] == value)
end

# An order that keeps the rule, in which each read returns the latest write, or nil.
def order(ops, first, value = '0')
  return [] if ops.empty?

  ops.each do |op|
    rest = ops - [op]
    next unless ready?(op, rest, first, value)

    tail = order(rest, first, op[3])
    return [op[0, 4], *tail] if tail
  end
  nil
end

HISTORIES.each.with_index(1) do |history, n|
  puts "#{n}. #{history}"
  MODELS.each do |label, first|
    found = order(history.split(', '), first)
    puts "   #{label}#{found ? found.join(' -> ') : 'no'}"
  end
end

In Ruby: RuboCop keeps methods short, so ready? says whether an operation may come next, and the models are lambdas in a hash.

Recorded with CRuby 4.0.7 on macOS 26 arm64. It runs in your browser with ruby.wasm 2.10.1 (Ruby 4.0.0). To run it yourself: ruby main.rb

Kotlin 2.4 · Main.kt

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
val histories =
    listOf(
        "A.w1 0-2, B.r1 3-4",
        "A.w1 0-2, B.r0 3-4",
        "A.w1 0-6, B.r0 1-2, C.r1 3-5",
        "A.w1 0-6, B.r1 1-2, C.r0 3-4",
        "A.w1 0-1, A.r0 2-3",
        "A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5",
    )

// Whether operation a must come before operation b.
val models =
    listOf<Pair<String, (String, String) -> Boolean>>(
        "linearisable: " to { a, b -> a[7] < b[5] }, // a returned before b was invoked
        "sequential:   " to { a, b -> a[0] == b[0] && a[5] < b[5] }, // same client
    )

// An order that keeps the rule, in which each read returns the latest write, or null.
fun order(
    ops: List<String>,
    first: (String, String) -> Boolean,
    value: Char = '0',
): List<String>? {
    if (ops.isEmpty()) return emptyList()
    for (op in ops) {
        val rest = ops - op
        if (rest.any { first(it, op) } || (op[2] == 'r' && op[3] != value)) continue
        val tail = order(rest, first, op[3]) ?: continue
        return listOf(op.take(4)) + tail
    }
    return null
}

fun main() {
    histories.forEachIndexed { n, history ->
        println("${n + 1}. $history")
        for ((label, first) in models) {
            println("   $label${order(history.split(", "), first)?.joinToString(" -> ") ?: "no"}")
        }
    }
}

In Kotlin: ops - op is a new list without the operation, and ?: continue moves on when no order follows it.

Recorded with Kotlin 2.4.20 on Java 25.0.4.1 on macOS 26 arm64. It runs in your browser with a WebAssembly build on the WASI runner (browser_wasi_shim 0.4.2). To run it yourself: kotlinc Main.kt -include-runtime -d main.jar && java -jar main.jar

Dart 3.13 · main.dart

// A.w1 0-2: client A writes 1, invoked at 0 ms and returned at 2 ms; the register starts at 0.
// So op[0] is the client, op[2] w or r, op[3] the value, op[5] and op[7] the times.
const histories = [
  'A.w1 0-2, B.r1 3-4',
  'A.w1 0-2, B.r0 3-4',
  'A.w1 0-6, B.r0 1-2, C.r1 3-5',
  'A.w1 0-6, B.r1 1-2, C.r0 3-4',
  'A.w1 0-1, A.r0 2-3',
  'A.w1 0-1, B.w2 0-1, C.r1 2-3, C.r2 4-5, D.r2 2-3, D.r1 4-5',
];

/// Whether operation a must come before operation b.
typedef Rule = bool Function(String a, String b);
final List<(String, Rule)> models = [
  // a returned before b was invoked
  ('linearisable: ', (a, b) => a.codeUnitAt(7) < b.codeUnitAt(5)),
  // the same client invoked a first
  (
    'sequential:   ',
    (a, b) => a[0] == b[0] && a.codeUnitAt(5) < b.codeUnitAt(5),
  ),
];

/// An order that keeps the rule, in which each read returns the latest write, or null.
List<String>? order(List<String> ops, Rule first, [String value = '0']) {
  if (ops.isEmpty) return [];
  for (final op in ops) {
    final rest = [...ops]..remove(op);
    if (rest.any((o) => first(o, op)) || (op[2] == 'r' && op[3] != value))
      continue;
    final tail = order(rest, first, op[3]);
    if (tail != null) return [op.substring(0, 4), ...tail];
  }
  return null;
}

void main() {
  for (final (n, history) in histories.indexed) {
    print('${n + 1}. $history');
    for (final (label, first) in models) {
      print(
        '   $label${order(history.split(', '), first)?.join(' -> ') ?? 'no'}',
      );
    }
  }
}

In Dart: Dart strings cannot be compared with <, so the rules compare code units, and order returns null when no order exists.

Recorded with Dart 3.13.5 on macOS 26 arm64. It runs in your browser with a WebAssembly build by dart2wasm 3.13.5. To run it yourself: dart run main.dart

Python 3.14 · main.py

# Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
SENT_MS = [0, 12, 14]
DELAY_MS = [
    [0, 10, 40],
    [10, 0, 3],
    [16, 6, 0],
]  # from the row's replica to the column's
CLOCKS = [[1, 0, 0], [1, 1, 0], [0, 0, 1]]  # Ben had seen Asha's post, Chen neither
TEXTS = ["Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"]


def ready(post: int, seen: list[int]) -> bool:
    """Whether a replica that has shown seen may show the post."""
    return all(c <= s + (x == post) for x, (c, s) in enumerate(zip(CLOCKS[post], seen)))


def run(causal: bool) -> None:
    seen = [[0, 0, 0] for _ in range(3)]  # how many posts of each replica r has shown
    held = [[False] * 3 for _ in range(3)]
    shown = [[] for _ in range(3)]
    for t, p, r in sorted(
        (SENT_MS[p] + DELAY_MS[p][r], p, r) for p in range(3) for r in range(3)
    ):
        held[r][p] = True
        while free := [
            q for q in range(3) if held[r][q] and (not causal or ready(q, seen[r]))
        ]:
            held[r][free[0]] = False
            shown[r].append(TEXTS[free[0]])
            seen[r][free[0]] += 1
        if held[r][p]:
            print(f'  R{r + 1} at {t} ms holds "{TEXTS[p]}"')
    for r in range(3):
        print(f"  R{r + 1}: {' | '.join(shown[r])}")


print("as messages arrive:")
run(False)
print("with causal delivery:")
run(True)

In Python: The arrivals are tuples, sorted by time, post and replica, and the walrus loop shows held posts while one may be shown.

Recorded with CPython 3.14.8 on macOS 26 arm64. It runs in your browser with Pyodide 314.0.7 (CPython 3.14.2). To run it yourself: python3 main.py

JavaScript Node 24 · main.mjs

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
const SENT_MS = [0, 12, 14];
const DELAY_MS = [
  [0, 10, 40],
  [10, 0, 3],
  [16, 6, 0],
]; // from the row's replica to the column's
const CLOCKS = [
  [1, 0, 0],
  [1, 1, 0],
  [0, 0, 1],
]; // Ben had seen Asha's post, Chen neither
const TEXTS = ["Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"];

// Whether a replica that has shown seen may show the post.
const ready = (post, seen) => CLOCKS[post].every((c, x) => c <= seen[x] + (x === post ? 1 : 0));

function run(causal) {
  const seen = [0, 1, 2].map(() => [0, 0, 0]); // how many posts of each replica r has shown
  const held = [0, 1, 2].map(() => [false, false, false]);
  const shown = [[], [], []];
  const arrivals = [0, 1, 2].flatMap((p) =>
    [0, 1, 2].map((r) => [SENT_MS[p] + DELAY_MS[p][r], p, r]),
  );
  arrivals.sort((a, b) => a[0] - b[0] || a[1] - b[1] || a[2] - b[2]);
  for (const [t, p, r] of arrivals) {
    held[r][p] = true;
    let q;
    while (
      (q = [0, 1, 2].find((x) => held[r][x] && (!causal || ready(x, seen[r])))) !== undefined
    ) {
      held[r][q] = false;
      shown[r].push(TEXTS[q]);
      seen[r][q] += 1;
    }
    if (held[r][p]) console.log(`  R${r + 1} at ${t} ms holds "${TEXTS[p]}"`);
  }
  shown.forEach((list, r) => console.log(`  R${r + 1}: ${list.join(" | ")}`));
}

console.log("as messages arrive:");
run(false);
console.log("with causal delivery:");
run(true);

In JavaScript: find returns undefined when no held post may be shown, which ends the while loop.

Recorded with Node.js 24.21.0 LTS (V8 13.6) on macOS 26 arm64. It runs in your browser with QuickJS (quickjs-emscripten 0.32.0). To run it yourself: node main.mjs

Java 25 LTS · Main.java

import java.util.ArrayList;
import java.util.Comparator;
import java.util.List;
import java.util.stream.IntStream;

public class Main {
  // Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
  static final int[] SENT_MS = {0, 12, 14};
  // From the row's replica to the column's.
  static final int[][] DELAY_MS = {{0, 10, 40}, {10, 0, 3}, {16, 6, 0}};
  // Ben had seen Asha's post, Chen neither.
  static final int[][] CLOCKS = {{1, 0, 0}, {1, 1, 0}, {0, 0, 1}};
  static final String[] TEXTS = {"Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"};

  // Whether a replica that has shown seen may show the post.
  static boolean ready(int post, int[] seen) {
    return IntStream.range(0, 3).allMatch(x -> CLOCKS[post][x] <= seen[x] + (x == post ? 1 : 0));
  }

  static void run(boolean causal) {
    int[][] seen = new int[3][3]; // how many posts of each replica r has shown
    boolean[][] held = new boolean[3][3];
    List<List<String>> shown = List.of(new ArrayList<>(), new ArrayList<>(), new ArrayList<>());
    List<int[]> arrivals = new ArrayList<>();
    for (int p = 0; p < 3; p++) {
      for (int r = 0; r < 3; r++) {
        arrivals.add(new int[] {SENT_MS[p] + DELAY_MS[p][r], p, r});
      }
    }
    arrivals.sort(
        Comparator.<int[]>comparingInt(a -> a[0])
            .thenComparingInt(a -> a[1])
            .thenComparingInt(a -> a[2]));
    for (int[] a : arrivals) {
      int r = a[2];
      held[r][a[1]] = true;
      for (int q = 0; q < 3; q++) {
        if (held[r][q] && (!causal || ready(q, seen[r]))) {
          held[r][q] = false;
          shown.get(r).add(TEXTS[q]);
          seen[r][q]++;
          q = -1; // look again from the first post
        }
      }
      if (held[r][a[1]]) {
        System.out.println("  R" + (r + 1) + " at " + a[0] + " ms holds \"" + TEXTS[a[1]] + "\"");
      }
    }
    for (int r = 0; r < 3; r++) {
      System.out.println("  R" + (r + 1) + ": " + String.join(" | ", shown.get(r)));
    }
  }

  public static void main(String[] args) {
    System.out.println("as messages arrive:");
    run(false);
    System.out.println("with causal delivery:");
    run(true);
  }
}

In Java: A Comparator built with thenComparingInt sorts the arrivals, and setting q back to -1 starts the scan again from the first post.

Recorded with OpenJDK 25.0.4.1 LTS (Eclipse Temurin) on macOS 26 arm64. It runs in your browser with a TeaVM 0.16.0 build in QuickJS (quickjs-emscripten 0.32.0). To run it yourself: java Main.java

C++23 · main.cpp

// Post p is written on replica p, with a vector clock: the posts of each
// replica its author saw.
#include <algorithm>
#include <array>
#include <print>
#include <string>
#include <tuple>
#include <vector>

using Row = std::array<int, 3>;
constexpr Row sent_ms = {0, 12, 14};
// From the row's replica to the column's.
constexpr std::array<Row, 3> delay_ms = {{{0, 10, 40}, {10, 0, 3}, {16, 6, 0}}};
// Ben had seen Asha's post, Chen neither.
constexpr std::array<Row, 3> clocks = {{{1, 0, 0}, {1, 1, 0}, {0, 0, 1}}};
const std::array<std::string, 3> texts = {"Asha: Lunch at 1?", "Ben: Yes!",
                                          "Chen: Late today"};

// Whether a replica that has shown seen may show the post.
bool ready(int post, const Row &seen) {
  for (int x = 0; x < 3; x++)
    if (clocks[post][x] > seen[x] + (x == post))
      return false;
  return true;
}

void run(bool causal) {
  std::array<Row, 3> seen{}; // how many posts of each replica r has shown
  std::array<std::array<bool, 3>, 3> held{};
  std::array<std::string, 3> shown;
  std::vector<std::tuple<int, int, int>> arrivals;
  for (int p = 0; p < 3; p++)
    for (int r = 0; r < 3; r++)
      arrivals.emplace_back(sent_ms[p] + delay_ms[p][r], p, r);
  std::ranges::sort(arrivals);
  for (const auto &[t, p, r] : arrivals) {
    held[r][p] = true;
    for (int q = 0; q < 3; q++)
      if (held[r][q] && (!causal || ready(q, seen[r]))) {
        held[r][q] = false;
        shown[r] += (shown[r].empty() ? "" : " | ") + texts[q];
        seen[r][q]++;
        q = -1; // look again from the first post
      }
    if (held[r][p])
      std::println("  R{} at {} ms holds \"{}\"", r + 1, t, texts[p]);
  }
  for (int r = 0; r < 3; r++)
    std::println("  R{}: {}", r + 1, shown[r]);
}

int main() {
  std::println("as messages arrive:");
  run(false);
  std::println("with causal delivery:");
  run(true);
}

In C++: The arrivals are std::tuple values, which std::ranges::sort orders by time, post and replica, as the other languages do.

Recorded with Apple clang 21.0.0 (C++23) and GCC 16.2.0 on macOS 26 arm64. It runs in your browser with Clang in WebAssembly (YoWASP) 22.0.0-git20542-10. To run it yourself: clang++ -std=c++23 -O2 -Wall -Wextra -Werror -pedantic -fsanitize=address,undefined main.cpp -o main && ./main

C# 14 · .NET 10 · app.cs

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
int[] sentMs = [0, 12, 14];
int[][] delayMs = [[0, 10, 40], [10, 0, 3], [16, 6, 0]]; // from the row's replica to the column's
int[][] clocks = [[1, 0, 0], [1, 1, 0], [0, 0, 1]]; // Ben had seen Asha's post, Chen neither
string[] texts = ["Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"];

Console.WriteLine("as messages arrive:");
Run(false);
Console.WriteLine("with causal delivery:");
Run(true);

// Whether a replica that has shown seen may show the post.
bool Ready(int post, int[] seen) =>
    Enumerable.Range(0, 3).All(x => clocks[post][x] <= seen[x] + (x == post ? 1 : 0));

void Run(bool causal)
{
    // How many posts of each replica r has shown.
    int[][] seen = [new int[3], new int[3], new int[3]];
    bool[][] held = [new bool[3], new bool[3], new bool[3]];
    List<string>[] shown = [[], [], []];
    var arrivals =
        from p in Enumerable.Range(0, 3)
        from r in Enumerable.Range(0, 3)
        let t = sentMs[p] + delayMs[p][r]
        orderby t, p, r
        select (t, p, r);
    foreach (var (t, p, r) in arrivals)
    {
        held[r][p] = true;
        for (int q = 0; q < 3; q++)
        {
            if (held[r][q] && (!causal || Ready(q, seen[r])))
            {
                held[r][q] = false;
                shown[r].Add(texts[q]);
                seen[r][q]++;
                q = -1; // look again from the first post
            }
        }
        if (held[r][p])
        {
            Console.WriteLine($"  R{r + 1} at {t} ms holds \"{texts[p]}\"");
        }
    }
    for (int r = 0; r < 3; r++)
    {
        Console.WriteLine($"  R{r + 1}: {string.Join(" | ", shown[r])}");
    }
}

In C#: A query expression builds and sorts the arrivals, with let naming the time once.

Recorded with C# 14 on .NET 10.0.12 (SDK 10.0.401) on macOS 26 arm64. It runs in your browser with the .NET runtime for WebAssembly 10.0.12. To run it yourself: dotnet run app.cs

C23 · main.c

// Post p is written on replica p, with a vector clock: the posts of each
// replica its author saw.
#include <stdbool.h>
#include <stdio.h>

static const int sent_ms[3] = {0, 12, 14};
// From the row's replica to the column's.
static const int delay_ms[3][3] = {{0, 10, 40}, {10, 0, 3}, {16, 6, 0}};
// Ben had seen Asha's post, Chen neither.
static const int clocks[3][3] = {{1, 0, 0}, {1, 1, 0}, {0, 0, 1}};
static const char *const texts[3] = {"Asha: Lunch at 1?", "Ben: Yes!",
                                     "Chen: Late today"};

// Whether a replica that has shown seen may show the post.
static bool ready(int post, const int seen[3]) {
  for (int x = 0; x < 3; x++)
    if (clocks[post][x] > seen[x] + (x == post))
      return false;
  return true;
}

static void run(bool causal) {
  int seen[3][3] = {0}; // how many posts of each replica r has shown
  bool held[3][3] = {0};
  int shown[3][3], n_shown[3] = {0};
  for (int t = 0; t < 50; t++) // the arrivals in order of time, post, replica
    for (int p = 0; p < 3; p++)
      for (int r = 0; r < 3; r++) {
        if (sent_ms[p] + delay_ms[p][r] != t)
          continue;
        held[r][p] = true;
        for (int q = 0; q < 3; q++)
          if (held[r][q] && (!causal || ready(q, seen[r]))) {
            held[r][q] = false;
            shown[r][n_shown[r]++] = q;
            seen[r][q]++;
            q = -1; // look again from the first post
          }
        if (held[r][p])
          printf("  R%d at %d ms holds \"%s\"\n", r + 1, t, texts[p]);
      }
  for (int r = 0; r < 3; r++) {
    printf("  R%d:", r + 1);
    for (int i = 0; i < n_shown[r]; i++)
      printf("%s %s", i ? " |" : "", texts[shown[r][i]]);
    printf("\n");
  }
}

int main(void) {
  printf("as messages arrive:\n");
  run(false);
  printf("with causal delivery:\n");
  run(true);
}

In C: The loop over every millisecond, post and replica visits the arrivals in the same order as the others sort them.

Recorded with Apple clang 21.0.0 (C23) and GCC 16.2.0 on macOS 26 arm64. It runs in your browser with Clang in WebAssembly (YoWASP) 22.0.0-git20542-10. To run it yourself: clang -std=c23 -O2 -Wall -Wextra -Werror -pedantic -fsanitize=address,undefined main.c -o main && ./main

PHP 8.5 · main.php

<?php

declare(strict_types=1);

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
const SENT_MS = [0, 12, 14];
const DELAY_MS = [[0, 10, 40], [10, 0, 3], [16, 6, 0]]; // from the row's replica to the column's
const CLOCKS = [[1, 0, 0], [1, 1, 0], [0, 0, 1]]; // Ben had seen Asha's post, Chen neither
const TEXTS = ['Asha: Lunch at 1?', 'Ben: Yes!', 'Chen: Late today'];

/**
 * Whether a replica that has shown $seen may show the post.
 *
 * @param list<int> $seen
 */
function ready(int $post, array $seen): bool
{
    foreach (CLOCKS[$post] as $x => $count) {
        if ($count > $seen[$x] + ($x === $post ? 1 : 0)) {
            return false;
        }
    }
    return true;
}

function run(bool $causal): void
{
    $seen = array_fill(0, 3, [0, 0, 0]); // how many posts of each replica r has shown
    $held = array_fill(0, 3, [false, false, false]);
    $shown = [[], [], []];
    $arrivals = [];
    foreach ([0, 1, 2] as $p) {
        foreach ([0, 1, 2] as $r) {
            $arrivals[] = [SENT_MS[$p] + DELAY_MS[$p][$r], $p, $r];
        }
    }
    sort($arrivals);
    foreach ($arrivals as [$t, $p, $r]) {
        $held[$r][$p] = true;
        for ($q = 0; $q < 3; $q++) {
            if ($held[$r][$q] && (!$causal || ready($q, $seen[$r]))) {
                $held[$r][$q] = false;
                $shown[$r][] = TEXTS[$q];
                $seen[$r][$q]++;
                $q = -1; // look again from the first post
            }
        }
        if ($held[$r][$p]) {
            echo '  R' . ($r + 1) . " at {$t} ms holds \"" . TEXTS[$p] . "\"\n";
        }
    }
    foreach ($shown as $r => $list) {
        echo '  R' . ($r + 1) . ': ' . implode(' | ', $list) . "\n";
    }
}

echo "as messages arrive:\n";
run(false);
echo "with causal delivery:\n";
run(true);

In PHP: sort orders arrays item by item, so the arrivals sort by time, then post, then replica.

Recorded with PHP 8.5.11 (CLI) on macOS 26 arm64. It runs in your browser with php-wasm 0.2.0 (PHP 8.5.2). To run it yourself: php main.php

Rust 1.99 · main.rs

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
const SENT_MS: [u32; 3] = [0, 12, 14];
// From the row's replica to the column's.
const DELAY_MS: [[u32; 3]; 3] = [[0, 10, 40], [10, 0, 3], [16, 6, 0]];
// Ben had seen Asha's post, Chen neither.
const CLOCKS: [[u32; 3]; 3] = [[1, 0, 0], [1, 1, 0], [0, 0, 1]];
const TEXTS: [&str; 3] = ["Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"];

/// Whether a replica that has shown seen may show the post.
fn ready(post: usize, seen: &[u32; 3]) -> bool {
    (0..3).all(|x| CLOCKS[post][x] <= seen[x] + u32::from(x == post))
}

fn run(causal: bool) {
    let mut seen = [[0; 3]; 3]; // how many posts of each replica r has shown
    let mut held = [[false; 3]; 3];
    let mut shown: [Vec<&str>; 3] = Default::default();
    let mut arrivals: Vec<(u32, usize, usize)> = (0..3)
        .flat_map(|p| (0..3).map(move |r| (SENT_MS[p] + DELAY_MS[p][r], p, r)))
        .collect();
    arrivals.sort();
    for (t, p, r) in arrivals {
        held[r][p] = true;
        while let Some(q) = (0..3).find(|&q| held[r][q] && (!causal || ready(q, &seen[r]))) {
            held[r][q] = false;
            shown[r].push(TEXTS[q]);
            seen[r][q] += 1;
        }
        if held[r][p] {
            println!("  R{} at {t} ms holds \"{}\"", r + 1, TEXTS[p]);
        }
    }
    for (r, list) in shown.iter().enumerate() {
        println!("  R{}: {}", r + 1, list.join(" | "));
    }
}

fn main() {
    println!("as messages arrive:");
    run(false);
    println!("with causal delivery:");
    run(true);
}

In Rust: Tuples compare item by item, so sort orders the arrivals, and while let with find shows held posts until none may be shown.

Recorded with rustc 1.99.0 (edition 2024) on macOS 26 arm64. It runs in your browser with a WebAssembly build on the WASI runner (browser_wasi_shim 0.4.2). To run it yourself: rustc --edition 2024 -O main.rs && ./main

TypeScript 6.0 · main.ts

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
const SENT_MS = [0, 12, 14];
const DELAY_MS = [
  [0, 10, 40],
  [10, 0, 3],
  [16, 6, 0],
]; // from the row's replica to the column's
const CLOCKS = [
  [1, 0, 0],
  [1, 1, 0],
  [0, 0, 1],
]; // Ben had seen Asha's post, Chen neither
const TEXTS = ["Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"];

// Whether a replica that has shown seen may show the post.
const ready = (post: number, seen: number[]): boolean =>
  CLOCKS[post].every((c, x) => c <= seen[x] + (x === post ? 1 : 0));

function run(causal: boolean): void {
  const seen = [0, 1, 2].map(() => [0, 0, 0]); // how many posts of each replica r has shown
  const held = [0, 1, 2].map(() => [false, false, false]);
  const shown: string[][] = [[], [], []];
  const arrivals = [0, 1, 2].flatMap((p) =>
    [0, 1, 2].map((r) => [SENT_MS[p] + DELAY_MS[p][r], p, r]),
  );
  arrivals.sort((a, b) => a[0] - b[0] || a[1] - b[1] || a[2] - b[2]);
  for (const [t, p, r] of arrivals) {
    held[r][p] = true;
    let q: number | undefined;
    while (
      (q = [0, 1, 2].find((x) => held[r][x] && (!causal || ready(x, seen[r])))) !== undefined
    ) {
      held[r][q] = false;
      shown[r].push(TEXTS[q]);
      seen[r][q] += 1;
    }
    if (held[r][p]) console.log(`  R${r + 1} at ${t} ms holds "${TEXTS[p]}"`);
  }
  shown.forEach((list, r) => console.log(`  R${r + 1}: ${list.join(" | ")}`));
}

console.log("as messages arrive:");
run(false);
console.log("with causal delivery:");
run(true);

In TypeScript: The arrivals are number arrays sorted with a comparator, and q is number | undefined until find has an answer.

Recorded with TypeScript 6.0.3 (strict), run by Node.js 24.21.0 on macOS 26 arm64. It runs in your browser with QuickJS (quickjs-emscripten 0.32.0) after Sucrase 3.35.1. To run it yourself: npx -p typescript@6.0.3 tsc --noEmit --strict main.ts && node main.ts

Go 1.27 · main.go

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
package main

import (
	"fmt"
	"slices"
	"strings"
)

var (
	sentMs = [3]int{0, 12, 14}
	// From the row's replica to the column's.
	delayMs = [3][3]int{{0, 10, 40}, {10, 0, 3}, {16, 6, 0}}
	// Ben had seen Asha's post, Chen neither.
	clocks = [3][3]int{{1, 0, 0}, {1, 1, 0}, {0, 0, 1}}
	texts  = [3]string{"Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"}
)

// ready says whether a replica that has shown seen may show the post.
func ready(post int, seen [3]int) bool {
	for x := range 3 {
		own := 0
		if x == post {
			own = 1
		}
		if clocks[post][x] > seen[x]+own {
			return false
		}
	}
	return true
}

func run(causal bool) {
	var seen [3][3]int // how many posts of each replica r has shown
	var held [3][3]bool
	var shown [3][]string
	var arrivals [][3]int
	for p := range 3 {
		for r := range 3 {
			arrivals = append(arrivals, [3]int{sentMs[p] + delayMs[p][r], p, r})
		}
	}
	slices.SortFunc(arrivals, func(a, b [3]int) int { return slices.Compare(a[:], b[:]) })
	for _, a := range arrivals {
		t, p, r := a[0], a[1], a[2]
		held[r][p] = true
		for q := 0; q < 3; q++ {
			if held[r][q] && (!causal || ready(q, seen[r])) {
				held[r][q] = false
				shown[r] = append(shown[r], texts[q])
				seen[r][q]++
				q = -1 // look again from the first post
			}
		}
		if held[r][p] {
			fmt.Printf("  R%d at %d ms holds %q\n", r+1, t, texts[p])
		}
	}
	for r, list := range shown {
		fmt.Printf("  R%d: %s\n", r+1, strings.Join(list, " | "))
	}
}

func main() {
	fmt.Println("as messages arrive:")
	run(false)
	fmt.Println("with causal delivery:")
	run(true)
}

In Go: slices.Compare orders two arrival arrays item by item, and %q prints the held post in quotes.

Recorded with Go 1.27.1 on macOS 26 arm64. It runs in your browser with the Go compiler in WebAssembly 1.27.1. To run it yourself: go run main.go

Swift 6.4 · main.swift

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
let sentMs = [0, 12, 14]
let delayMs = [[0, 10, 40], [10, 0, 3], [16, 6, 0]]  // from the row's replica to the column's
let clocks = [[1, 0, 0], [1, 1, 0], [0, 0, 1]]  // Ben had seen Asha's post, Chen neither
let texts = ["Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today"]

/// Whether a replica that has shown seen may show the post.
func ready(_ post: Int, _ seen: [Int]) -> Bool {
  (0..<3).allSatisfy { clocks[post][$0] <= seen[$0] + ($0 == post ? 1 : 0) }
}

func run(causal: Bool) {
  var seen = Array(repeating: [0, 0, 0], count: 3)  // how many posts of each replica r has shown
  var held = Array(repeating: [false, false, false], count: 3)
  var shown: [[String]] = [[], [], []]
  let arrivals = (0..<3).flatMap { p in (0..<3).map { r in (sentMs[p] + delayMs[p][r], p, r) } }
  for (t, p, r) in arrivals.sorted(by: { $0 < $1 }) {
    held[r][p] = true
    while let q = (0..<3).first(where: { held[r][$0] && (!causal || ready($0, seen[r])) }) {
      held[r][q] = false
      shown[r].append(texts[q])
      seen[r][q] += 1
    }
    if held[r][p] {
      print("  R\(r + 1) at \(t) ms holds \"\(texts[p])\"")
    }
  }
  for (r, list) in shown.enumerated() {
    print("  R\(r + 1): \(list.joined(separator: " | "))")
  }
}

print("as messages arrive:")
run(causal: false)
print("with causal delivery:")
run(causal: true)

In Swift: Tuples of comparable values compare with <, which sorts the arrivals, and while let with first(where:) shows held posts.

Recorded with Apple Swift 6.4 on macOS 26 arm64. It runs in your browser with a WebAssembly build on the WASI runner (browser_wasi_shim 0.4.2). To run it yourself: swiftc -O main.swift -o main && ./main

Ruby 4.0 · main.rb

# frozen_string_literal: true

# Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
SENT_MS = [0, 12, 14].freeze
DELAY_MS = [[0, 10, 40], [10, 0, 3], [16, 6, 0]].freeze # from the row's replica to the column's
CLOCKS = [[1, 0, 0], [1, 1, 0], [0, 0, 1]].freeze # Ben had seen Asha's post, Chen neither
TEXTS = ['Asha: Lunch at 1?', 'Ben: Yes!', 'Chen: Late today'].freeze

# The posts arriving at three replicas, shown as they arrive or with causal delivery.
class Run
  def initialize(causal)
    @causal = causal
    @seen = Array.new(3) { [0, 0, 0] } # how many posts of each replica r has shown
    @held = Array.new(3) { [false, false, false] }
    @shown = [[], [], []]
  end

  # Whether replica r may show the post now.
  def ready?(post, replica)
    @held[replica][post] && (!@causal || (0..2).all? do |x|
      CLOCKS[post][x] <= @seen[replica][x] + (x == post ? 1 : 0)
    end)
  end

  def arrive(time, post, replica)
    @held[replica][post] = true
    while (q = (0..2).find { |x| ready?(x, replica) })
      show(q, replica)
    end
    puts %(  R#{replica + 1} at #{time} ms holds "#{TEXTS[post]}") if @held[replica][post]
  end

  def show(post, replica)
    @held[replica][post] = false
    @shown[replica] << TEXTS[post]
    @seen[replica][post] += 1
  end

  def play
    (0..2).to_a.product((0..2).to_a).map { |p, r| [SENT_MS[p] + DELAY_MS[p][r], p, r] }.sort
      .each { |time, post, replica| arrive(time, post, replica) }
    @shown.each_with_index { |list, r| puts "  R#{r + 1}: #{list.join(' | ')}" }
  end
end

puts 'as messages arrive:'
Run.new(false).play
puts 'with causal delivery:'
Run.new(true).play

In Ruby: RuboCop keeps methods short, so one Run object holds the state and arrive, show and play each take one step.

Recorded with CRuby 4.0.7 on macOS 26 arm64. It runs in your browser with ruby.wasm 2.10.1 (Ruby 4.0.0). To run it yourself: ruby main.rb

Kotlin 2.4 · Main.kt

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
val sentMs = intArrayOf(0, 12, 14)

// From the row's replica to the column's.
val delayMs = listOf(intArrayOf(0, 10, 40), intArrayOf(10, 0, 3), intArrayOf(16, 6, 0))

// Ben had seen Asha's post, Chen neither.
val clocks = listOf(intArrayOf(1, 0, 0), intArrayOf(1, 1, 0), intArrayOf(0, 0, 1))
val texts = listOf("Asha: Lunch at 1?", "Ben: Yes!", "Chen: Late today")

// Whether a replica that has shown seen may show the post.
fun ready(
    post: Int,
    seen: IntArray,
) = (0..2).all { clocks[post][it] <= seen[it] + if (it == post) 1 else 0 }

fun run(causal: Boolean) {
    val seen = List(3) { IntArray(3) } // how many posts of each replica r has shown
    val held = List(3) { BooleanArray(3) }
    val shown = List(3) { mutableListOf<String>() }
    val arrivals =
        (0..2)
            .flatMap { p -> (0..2).map { r -> Triple(sentMs[p] + delayMs[p][r], p, r) } }
            .sortedWith(compareBy({ it.first }, { it.second }, { it.third }))
    for ((t, p, r) in arrivals) {
        held[r][p] = true
        while (true) {
            val q = (0..2).firstOrNull { held[r][it] && (!causal || ready(it, seen[r])) } ?: break
            held[r][q] = false
            shown[r] += texts[q]
            seen[r][q]++
        }
        if (held[r][p]) println("  R${r + 1} at $t ms holds \"${texts[p]}\"")
    }
    shown.forEachIndexed { r, list -> println("  R${r + 1}: ${list.joinToString(" | ")}") }
}

fun main() {
    println("as messages arrive:")
    run(false)
    println("with causal delivery:")
    run(true)
}

In Kotlin: compareBy with three selectors sorts the Triples, and firstOrNull with ?: break ends the loop when no held post may be shown.

Recorded with Kotlin 2.4.20 on Java 25.0.4.1 on macOS 26 arm64. It runs in your browser with a WebAssembly build on the WASI runner (browser_wasi_shim 0.4.2). To run it yourself: kotlinc Main.kt -include-runtime -d main.jar && java -jar main.jar

Dart 3.13 · main.dart

// Post p is written on replica p, with a vector clock: the posts of each replica its author saw.
const sentMs = [0, 12, 14];
const delayMs = [
  [0, 10, 40],
  [10, 0, 3],
  [16, 6, 0],
]; // from the row's replica to the column's
const clocks = [
  [1, 0, 0],
  [1, 1, 0],
  [0, 0, 1],
]; // Ben had seen Asha's post, Chen neither
const texts = ['Asha: Lunch at 1?', 'Ben: Yes!', 'Chen: Late today'];

/// Whether a replica that has shown [seen] may show the post.
bool ready(int post, List<int> seen) =>
    [0, 1, 2].every((x) => clocks[post][x] <= seen[x] + (x == post ? 1 : 0));

void run(bool causal) {
  final seen = List.generate(
    3,
    (_) => [0, 0, 0],
  ); // how many posts of each replica r has shown
  final held = List.generate(3, (_) => [false, false, false]);
  final shown = List.generate(3, (_) => <String>[]);
  final arrivals =
      [
        for (var p = 0; p < 3; p++)
          for (var r = 0; r < 3; r++) (sentMs[p] + delayMs[p][r], p, r),
      ]..sort(
        (a, b) => a.$1 != b.$1
            ? a.$1 - b.$1
            : (a.$2 != b.$2 ? a.$2 - b.$2 : a.$3 - b.$3),
      );
  for (final (t, p, r) in arrivals) {
    held[r][p] = true;
    for (var q = 0; q < 3; q++) {
      if (held[r][q] && (!causal || ready(q, seen[r]))) {
        held[r][q] = false;
        shown[r].add(texts[q]);
        seen[r][q]++;
        q = -1; // look again from the first post
      }
    }
    if (held[r][p]) print('  R${r + 1} at $t ms holds "${texts[p]}"');
  }
  for (var r = 0; r < 3; r++) {
    print('  R${r + 1}: ${shown[r].join(' | ')}');
  }
}

void main() {
  print('as messages arrive:');
  run(false);
  print('with causal delivery:');
  run(true);
}

In Dart: The arrivals are records built by a collection for, and the comparator compares their fields one after another.

Recorded with Dart 3.13.5 on macOS 26 arm64. It runs in your browser with a WebAssembly build by dart2wasm 3.13.5. To run it yourself: dart run main.dart