Draft · Systems + coding agents

# Porting a research checker from Java to C with a coding agent

Boomslang-C: what it took, what came out, and what C looks like when an agent writes it

Boomslang is a checker for database isolation levels, published at ATC 2026 with a Java artifact. I asked Claude Code to rewrite it in C. Twenty-two hours later, with no message from me in between, there was a dependency-free C implementation that ran every experiment in the paper's artifact. It agreed with Java on every verdict but one. It was 38 times faster. Four days later it was 60 times faster, checked all of Adya's isolation levels, and had grown a specification language.

**60×**faster than Java (geometric mean wall time, 78 artifact runs)

**48×**less peak memory

**4.9K**lines of C replaced 23.9K lines of Java and a 98K-line C++ SMT solver

**22 h**from the first prompt to a full port, unattended

## What Boomslang does

A database promises an isolation level such as serializability or snapshot isolation. Boomslang checks that promise from the outside. You give it a trace of what clients sent and received. It asks whether some order of the transactions, and some choice of which write each read observed, explains the trace under the promised level. If no such explanation exists, the database broke its promise.

Answering that is NP-complete in general, so the checker is a small compiler. It parses traces in eight formats, builds a graph of what is known and what is uncertain, prunes the graph with reachability, and hands the rest to a SAT solver with a graph-acyclicity theory. The Java artifact (SOSH) has 229 Java files and 23,928 lines. For the solver it calls MonoSAT, about 98,000 lines of C++, through JNI.

## Why C, and why now

The usual case against C is about people. Memory management, undefined behaviour and the boilerplate of hash maps and growable arrays all cost developer time. Java, with a garbage collector, a JIT and a mature SMT library, is cheaper to write in.

A coding agent moves those costs. It writes the boilerplate in seconds. It also runs the tools that keep C honest without being asked twice: AddressSanitizer, ThreadSanitizer, UndefinedBehaviorSanitizer, differential fuzzers and brute-force oracles. What C still gives you is the part a checker like this needs: control over memory layout, no garbage collector, no JIT warm-up, no JNI boundary, plain threads and a straight path to CUDA. So this project tests a simple bet: with an agent paying the costs of C, you get its benefits nearly for free.

## How it went

The port itself took two prompts, and the whole project about twenty, most of them a few words long. These are the ones that shaped the work, in order:

1. Oct 10, 10:11

   **The port.** I attached the paper and wrote Implement Boomslang in C language. Compare performance with github.com/winddd/SOSH. Thirty minutes later I added a loop: /loop 10min continue the work, until the implementation in C can run the same tests as the Java version.
2. overnight

   **Unattended.** Every ten minutes the agent picked up where it had stopped. It built the Java artifact (Gradle, GMP, MonoSAT) so it could compare outputs, and downloaded the artifact's data. It wrote parsers for Cobra, EDN, Tapir, Plume, JuiceFS, Eiger and two binary formats, the last one through a hand-written decoder for Java object serialization. It also wrote the solver, and fuzzers that compare C and Java on random traces.
3. Oct 11, 08:42

   **First result.** write a report in a html page and commit. All 84 runs of the artifact executed on the C version. It was 38× faster (geometric mean) and used 32× less memory.
4. Oct 11, 10:10

   **Scope growth.** Check Atul Adya phd thesis (MIT), implement all mentioned isolation levels. That covers all thirteen levels, including those for aborted transactions, the per-operation graphs of PL-2L and the time-based ones. It was done (about 1,600 changed lines), tested against a brute-force oracle of the thesis, and pushed in 78 minutes.
5. Oct 11, 11:46

   **Performance.** Anything to improve? produced a list of twelve items. I picked three: prune while generating the graph, use threads, and add the paper's "unsat search". Then I asked for a GPU path for very large traces.
6. Oct 11, 19:44

   **A language.** I attached a design document for Isola, a specification language for isolation levels. The agent implemented the parser, a compiler to SAT, a solver and an independent reference implementation. Two days later it argued experimentally how complete the language is.

The agent did not work in the dark during the overnight stretch. Its first task was to make the comparison possible: build the Java artifact, fetch the data, and write scripts that run both implementations on the same inputs. Once those existed, every later change had a judge.

## What came out

Lines of code. The Java column counts the artifact's application sources by package, without its baselines. The C component rows are today's sources. The Java code also has encoders for other checkers (Cobra, Viper, PolySI) that were not ported.

| Component | Java | C |
| --- | --- | --- |
| Trace parsers (8 formats, incl. a Java-serialization decoder) | 3,441 | 1,964 |
| Graph construction and IR | 6,386 | 1,364 |
| Optimizations (pruning, prioritization) | 1,677 | 469 |
| SAT solver with acyclicity theory | 98K C++ (MonoSAT) + 2,741 glue | 887 |
| Whole checker at the first commit | 23,928 | 4,926 |
| Whole checker today, with threads, GPU filter and unsat search |  | 6,319 |

The C build has no dependencies beyond libc and pthreads. CUDA is optional. The solver deserves a note. MonoSAT is a general SMT solver with graph theories. Boomslang needs one theory, acyclicity, and the agent wrote a CDCL solver around exactly that. It uses Pearce–Kelly incremental topological ordering, branches only on the choices the checker actually has to make, and learns conflict clauses from cycles. That solver is 887 lines.

### Speed and memory on the artifact's own experiments

Median of three runs per case, same machine (32 cores, 62 GB RAM), Java with a 40 GB heap. The C version uses up to 16 threads, only for graph generation.

| Experiment | Java | C |
| --- | --- | --- |
| TPC-C, 50K transactions, snapshot isolation (the paper reports Java running out of memory) | 173 s, 62 GB | 1.2 s, 0.63 GB |
| BlindW, 80K transactions, serializability | 96 s, 32 GB | 0.40 s, 0.23 GB |
| TiKV RandomBench, snapshot isolation | 300 s | 0.45 s |
| All 78 runs where both finish (geometric mean) | 1 | 60× faster, 48× less memory |
| Runs where Java needs more than 10 s (22 runs) | 1 | 159× faster |
| Total wall time over the 78 runs | 1,703 s | 11.9 s |

### Where the speed comes from

A port that changes language and algorithm at the same time makes it hard to credit either. Boomslang-C has a flag, `-full_edges`, that makes it build exactly the graph Java builds. Comparing the two settings splits the gain:

Same graph as Java

30×

C's own algorithms

60×

Same graph, runs >10 s

35×

C's algorithms, runs >10 s

159×

1×10×100×400×

About 30× comes from the implementation alone: same graph, same answers, different language and data structures. Part of it on small runs is the JVM's start-up cost of about 0.3 s. The rest, 2× overall and 4.5× on large runs, comes from algorithmic changes the agent made once it had a reference to check them against:

- **A chain-compressed closure** instead of a full reachability bitmap. Each node stores the earliest reachable position on each session chain, which takes O(n · sessions) memory instead of O(n²).
- **Transitively reduced write dependencies.** Consecutive versions only, with the same reachability. This is what fixes TPC-C 50K.
- **Pruning while generating.** Most chain pairs on blind-write workloads are resolved by reachability as soon as they are created, so the 4.4 million candidate constraints on BlindW 80K never reach memory.
- **A pair filter on the CPU or GPU.** A table lookup per candidate pair decides most of them without building anything. On a generated trace with a million transactions and 800 million candidate pairs, graph construction went from 153 s to 9.7 s on one thread, 2.4 s on 16 threads, and 1.9 s with an RTX 4090.

These are not things only C can do. They are things that are cheap to try when allocation, layout and threads are under your control, and when an agent writes the variant, runs the benchmark and checks the answers in a few minutes.

## How you trust 10,000 lines of agent-written C

This is the part that matters most, and where I spent the least effort, because the agent built the checks itself. Every claim of correctness rests on comparison with something independent:

Counts after the fixes described below.

| Check | Compared against | Runs | Mismatches |
| --- | --- | --- | --- |
| Random traces at 4 levels, 4 flag settings | The Java artifact | 5,200 | 0 |
| Random traces with duplicate values and range queries | Brute-force serializability oracle | 40,000 | 0 |
| All 13 of Adya's levels | A literal brute-force reading of the thesis | 35,100 | 0 |
| PL-2+ | Brute-force PL-2+ oracle | 4,500 | 0 |
| All 84 experiment runs of the artifact | The Java artifact | 84 | 1 |
| Hand-written anomaly traces | Expected verdicts | 730 | 0 |
| Every satisfying answer | An independent check of the model the solver found | all | 0 |

The comparisons also caught the agent's own bugs.

### Bugs the agent made, and caught

- **A solver bug present since the first commit.** Clause minimization left internal marks set on literals it dropped, so later conflict analyses could learn clauses that were too strong. No test had shown a wrong verdict. It surfaced a day later as a heap overflow under AddressSanitizer, once the parallel unsat search exercised the solver differently. This is exactly the kind of bug C is feared for, and exactly the kind sanitizers find.
- **Strings without terminators** in the specification-language front end. The first run printed every model name glued together, so it was obvious and quickly fixed.
- **Three compiler bugs in optimizations,** found by a fuzzer that generates random specifications rather than reusing the library.
- **A false alarm.** A benchmark that normally takes one second ran for over ten minutes, and the agent started treating it as a regression. The run was missing the `-session` flag the benchmarks always use. It found its own mistake within minutes, but it is a reminder to read numbers with care.

### The pattern that made this work

The agent never had to be right on the first try. It had to be checkable. Every stage had an independent judge before it was written: the Java artifact, a brute-force oracle, an earlier version of the C code, or a sanitizer. With that in place, C's sharp edges stop being a reason to avoid it, because the failures show up as a mismatch or a sanitizer report instead of a wrong answer in a paper.

## Beyond the port

Once the base was fast and trusted, extending it was cheap:

- **Adya's thesis in full.** Thirteen levels, including the executing-transaction levels for aborted transactions, unfolded per-operation graphs and time-precedes orders, in 78 minutes.
- **Isola, a specification language for isolation levels.** About 4,000 lines of C for the parser, the compiler to SAT and graph constraints, and a solver, plus a 750-line Python reference that it is fuzzed against. Writing the doc's own levels in it uncovered four bugs in the levels as written in the design doc. Writing all of Adya's levels and Cerone et al.'s axioms in it showed that one language holds three different styles of definition. They agreed with independent references on tens of thousands of traces.
- **Scale.** A trace with a million transactions now checks for serializability in about 8 seconds end to end.

## What did not work, or not yet

- **The paper's unsat search rarely pays off.** With pruning on, every injected violation was rejected before the solver started. With pruning off, it won once in twelve traces and slowed the others by 20–75% through contention.
- **One deliberately hard case is still slow.** With every optimization off, the C solver takes 168 s, where Java times out. Its branching heuristic is simpler than MonoSAT's.
- **The agent's output still needs a reader.** Most of my prompts were short ("push", "Anything to improve?", "status?"), but each result came with numbers I could check, and I did. The one benchmark mix-up would have been easy to publish.

## Takeaways

- **Give the agent a judge first.** A reference implementation, an oracle or a test suite turns "rewrite this in C" from a risk into a loop that converges.
- **Ask for the boring safety nets explicitly.** Sanitizers, differential fuzzers and an independent check of every answer cost the agent minutes and saved this project from shipping a solver bug.
- **Let it run.** The port needed one loop prompt and a night. Long autonomous stretches work when progress is measured against something objective.
- **C is a reasonable default again for performance-critical tools.** With an agent writing it, the remaining cost is review, and review is easier when the code is 5,000 lines instead of 24,000 plus a dependency.

Numbers are from the Boomslang-C repository: `bench/RESULTS.md` for the artifact runs, `README.md` for the test counts, and `isola/COMPLETENESS.md` for the specification-language experiments. Line counts are from `wc -l` on the sources at each commit.