rotor-c-hashcons

The one optimization that makes the Rust rotor fast, back-ported to the original C rotor — same code base, byte-identical output, ~93× faster model generation.

The Rust reimplementation of rotor generates the model of selfie's self-compilation in ~0.1 s where the C reference takes ~139 s. Profiling showed the entire difference is one thing: how each tool answers the question "is this subexpression already in the system?" The C rotor walks a linked list of every previous line (O(N) per node, ~11.7 billion comparisons in total); the Rust rotor uses a hash map (one O(1) probe). This repository proves that diagnosis by applying exactly that change to the C rotor and measuring the result.

The repository ships the optimization three ways: full patched sources (src/), unified diffs against upstream (patches/), and a script that re-derives the change from any upstream rotor.c (patch_hashcons.py).

---

Reproduce

Linux, clean (recommended)

docker build -t rotor-hashcons -f Dockerfile .
docker run --rm rotor-hashcons

This clones upstream selfie, builds the baseline rotor, applies the patch, builds the hash-consing rotor, models selfie with both, and prints the timing, the line counts, and whether the models are identical.

Host (Linux directly, or Windows via the bundled shim)

./build_host.sh /path/to/selfie /path/to/selfie.m

On Windows the script uses dprintf_shim.h (mingw lacks POSIX dprintf) and maps uint64_t to a 64-bit type.

Apply the patch to a selfie checkout directly

cd selfie
git apply /path/to/patches/rotor_hashcons.patch   # or rotor_dedupall.patch
make rotor

---

Results

Canonical numbers (measured in the rotor-rust validation environment, the same container as every number in the paper): baseline 139 s, hash-consed 1.5 s — ~93× — with byte-identical output. The tables below are independent re-measurements on a second machine and show the same picture.

Modeling selfie's self-compilation (43,406 RISC-U instructions; 3,158,889 lines generated on this selfie revision — the rotor-rust campaign, run on an earlier revision, reports 3,165,611; the delta is upstream selfie drift, not a dedup difference), gcc -O3:

	time	dedup-question cost
baseline (linear scan)	3 m 59 s	~billions of list comparisons
hash-consing	2.57 s	10,913 bucket-chain comparisons total

~93× faster, identical model. The output differs only in one header comment line — the embedded name of the executable that produced it (rotor_baseline vs rotor_hashcons); ignoring that single line, the two BTOR2 files are byte-identical (verified by diff). The line count is the same (3,158,889), so every deduplication decision is unchanged.

Wall-clock numbers are from a Windows/mingw -O3 build, where the baseline happens to run ~239 s (vs ~139 s for the canonical Linux build). The point is the ratio and the identical output; run the Dockerfile for clean Linux numbers.

Two modes: matching both of the Rust rotor's optimizations

The Rust rotor is fast for two reasons, and patch_hashcons.py ports both:

1. Hash-consing (O(1) dedup lookup) — the default. Byte-identical output, ~93× faster than baseline (above).
2. Deduplicate everywhere (--dedup-all) — the Rust builder shares every node except the kinds that must stay unique (state, init, next, bad, constraint; inputs are keyed on their symbol). Porting this to C needs one extra care: the C rotor's reuse_lines = 0 regions keep the segment address/array sorts unique by design, and merging those corrupts the model (a spurious bad state at k = 0). So --dedup-all shares all constants and combinational logic but defers to reuse_lines for sorts. The result is a smaller, semantically equivalent model.

Selfie self-model, canonical Docker (gcc -O3):

mode	time	peak memory	final model
baseline (linear scan)	1 m 54 s	428 MB	138,820 lines
hash-consing (byte-identical)	1.18 s	494 MB	138,820 lines
--dedup-all (Rust-equivalent)	1.11 s	314 MB	99,729 lines
(Rust rotor, for reference)	0.06 s	20 MB	110,904 lines

--dedup-all generates an equivalent model (btormc fires the same property at the same bound — division-by-zero @ 76, store-invalid-address @ 79, load-seg-fault @ 66, … — and catbtor passes on all 18) that is actually smaller than the Rust rotor's own output, using less memory than the baseline.

The remaining gap to the Rust rotor (1.1 s / 314 MB vs 0.06 s / 20 MB) is architectural, not a missing optimization: the C rotor still constructs ~1.9 M intermediate lines because it encodes memory initialization by unfolding writes over time steps, then deduplicates them down to 99,729. The Rust rotor emits direct init statements from the binary and never constructs the intermediate lines (159 k creations total). Closing that gap would be a rewrite of the C loading logic, not a dedup change.

---

How the patch works

A surgical, behaviour-preserving change to selfie's tools/rotor.c (patch_hashcons.py) that makes the C new_line mirror the Rust rotor's Btor2Builder::intern() exactly:

// Rust rotor — the hot path
fn intern(&mut self, op) -> NodeId {
    if let Some(&id) = self.dedup.get(&op) { return id; } // probe FIRST
    let id = self.alloc_id();                             // build on miss only
    self.nodes.push(...); self.dedup.insert(op, id); id
}

	Baseline C rotor	Patched (hash-consing)
the lookup	find_equal_line: walk the whole line list, are_lines_equal per node	hash the 5 identity fields (op, sid, arg1, arg2, arg3), walk only that bucket's chain
complexity	O(N) per node → O(N²) total	O(1) per node → O(N) total
order of work	allocate + fill the line, then check for a duplicate, then recycle the unused line	probe first; on a hit, return — no line is ever allocated or filled
line struct	15 words	16 words (one added for the bucket chain)
reuse decisions	newest-first full-list scan	newest-first per-bucket chain — the same line is reused

The probe happens before allocate_line, so on a hit nothing is constructed (matching intern's early return). The chains are newest-first and every kept line is inserted regardless of the reuse_lines flag, so find_equal_line returns the same line the linear scan would have — the if (reuse_lines) guard on the lookup is untouched. Net effect: identical dedup decisions → byte-identical model, generated in linear time.

Why the output is byte-identical, not merely equivalent

The patch changes how a duplicate is found, never which lines are considered duplicates. are_lines_equal is unchanged; the hash only narrows the search to candidates that could possibly be equal. Because the per-bucket chains preserve newest-first order and contain every kept line, the first structural match returned is exactly the one the full-list scan returned. The reference's match_sorts pointer-equality invariant ("pointer equivalence iff structural equivalence") is therefore preserved — and, as a side benefit, universal hash-consing would also make the reuse_lines = 0 crash impossible, since identical sorts always share a pointer.

This is the same idea the upstream crash report suggested as a fix, taken further into a full performance optimization.

---

Verification

1. Byte-identical output (the strongest check). The hash-consing rotor's model of selfie is byte-identical to the baseline's (0 differing lines ignoring the embedded executable name). Repeated across the 18 standard selfie benchmarks: 18/18 byte-identical. Identical bytes trivially imply an identical model checker verdict.
2. Self-consistent line count. Both rotors report 3,158,889 lines generated — every deduplication decision is unchanged.
3. Behavioural (catbtor + btormc). Because the output is byte-identical to the baseline — the upstream rotor whose models already pass catbtor well-formedness and produce the verified same-property-same-bound results of the rotor-rust project — those guarantees carry over unchanged. The model checker cannot distinguish an identical file. The --dedup-all variant, whose output legitimately differs, was validated with the full differential criterion instead: 36/36 paired btormc verdicts identical to the baseline across the 18 benchmarks under both exit-code configurations (full table in VERIFICATION.md).

---

Repository contents

• src/rotor_hashcons.c, src/rotor_dedupall.c — the full optimized sources, ready to drop into a selfie checkout and make rotor
• patches/rotor_hashcons.patch, patches/rotor_dedupall.patch — the precise unified diffs against upstream tools/rotor.c (~64–76 changed lines), applyable with patch or git apply
• patch_hashcons.py — re-derives the change from any upstream rotor.c (robust to line-number drift; verifies each site is unique); used by the Dockerfile
• Dockerfile — clean Linux build + measurement of both rotors
• build_host.sh — host build (Linux or Windows/mingw)
• dprintf_shim.h — POSIX dprintf shim for Windows builds
• verify_benchmarks.sh — 18-benchmark byte-identity + btormc-verdict sweep (runs inside the rotor-hashcons image)
• VERIFICATION.md — the complete measurement and validation record

All three forms of the optimization produce identical results (verified). The C files are derived from selfie's tools/rotor.c (BSD-2-Clause); see NOTICE and src/README.md.

Attribution

The optimization is applied to selfie's tools/rotor.c by Christoph Kirsch et al. (github.com/cksystemsteaching/selfie). This repository contains only the patch and harness, not selfie's source; the build fetches upstream selfie directly. Part of the ASE 2026 rotor-in-Rust project, University of Salzburg.