diff --git a/.github/workflows/benchmark-history.yml b/.github/workflows/benchmark-history.yml new file mode 100644 index 0000000..e9f0bab --- /dev/null +++ b/.github/workflows/benchmark-history.yml @@ -0,0 +1,88 @@ +name: benchmark-history + +# Accumulate a reference-normalized benchmark time-series so slow creep (which the +# per-PR head-vs-base gate is blind to) becomes visible. On every push to master +# we run the bench, append one sample to an append-only NDJSON on the ORPHAN +# `bench-history` branch (isolated from master/PR history — no churn), and check +# the new sample against a rolling baseline. Creep is a SOFT-fail + commit comment. +on: + push: + branches: [master] + +permissions: + contents: write + +concurrency: + group: bench-history + cancel-in-progress: false + +jobs: + accumulate: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + + - uses: actions/setup-node@v4 + with: + node-version: 20 + + - name: Build and run bench (interleaved) + run: | + make -C native bench >/dev/null 2>&1 + cp /tmp/mf_test_bench /tmp/bench + for i in $(seq 1 7); do /tmp/bench > "/tmp/run_$i.json"; done + + - name: Aggregate one normalized sample + run: | + R=$(ls /tmp/run_*.json | paste -sd,) + node scripts/bench-aggregate.mjs --runs "$R" \ + --sha "$GITHUB_SHA" --date "$(date -u +%FT%TZ)" > /tmp/sample.ndjson + cat /tmp/sample.ndjson + + - name: Append to bench-history + creep check + id: creep + run: | + git config user.name "github-actions[bot]" + git config user.email "github-actions[bot]@users.noreply.github.com" + git fetch origin bench-history || true + if git rev-parse --verify origin/bench-history >/dev/null 2>&1; then + git worktree add /tmp/hist origin/bench-history + else + git worktree add --detach /tmp/hist + git -C /tmp/hist checkout --orphan bench-history + git -C /tmp/hist rm -rf . >/dev/null 2>&1 || true + fi + touch /tmp/hist/history.ndjson + # creep check: new sample vs the EXISTING history (before appending) + set +e + node scripts/bench-creep.mjs --history /tmp/hist/history.ndjson --sample /tmp/sample.ndjson > /tmp/creep.md + echo "rc=$?" >> "$GITHUB_OUTPUT" + set -e + cat /tmp/creep.md + # append + push (one retry if the branch advanced under us) + cat /tmp/sample.ndjson >> /tmp/hist/history.ndjson + git -C /tmp/hist add history.ndjson + git -C /tmp/hist commit -m "bench: sample for ${GITHUB_SHA}" + git -C /tmp/hist push origin HEAD:bench-history || { + git -C /tmp/hist fetch origin bench-history + git -C /tmp/hist reset --soft origin/bench-history + cat /tmp/sample.ndjson >> /tmp/hist/history.ndjson + git -C /tmp/hist add history.ndjson + git -C /tmp/hist commit -m "bench: sample for ${GITHUB_SHA} (retry)" + git -C /tmp/hist push origin HEAD:bench-history + } + + - name: Comment creep on commit + if: steps.creep.outputs.rc != '0' + uses: actions/github-script@v7 + with: + script: | + const fs = require('fs'); + const body = '\n' + fs.readFileSync('/tmp/creep.md', 'utf8'); + await github.rest.repos.createCommitComment({ ...context.repo, commit_sha: context.sha, body }); + + - name: Soft-fail on creep + if: steps.creep.outputs.rc != '0' + run: | + echo "::warning::Benchmark slow-creep detected vs rolling baseline — see the commit comment. (soft-fail)" + exit 1 diff --git a/.github/workflows/benchmark.yml b/.github/workflows/benchmark.yml new file mode 100644 index 0000000..8182312 --- /dev/null +++ b/.github/workflows/benchmark.yml @@ -0,0 +1,88 @@ +name: benchmark + +# Per-op graph-store microbenchmark, base vs head, on ONE runner — no committed +# baseline values (nothing for git to churn). Builds the SAME harness against the +# base and head store sources, runs them interleaved, frequency-corrects head to +# base via a fixed-work reference op, and diffs the medians. SOFT-fail: a +# regression turns the check red and posts a PR comment, but this check is not +# meant to be a required status, so it never hard-blocks a merge. +on: + pull_request: + +permissions: + contents: read + pull-requests: write + +jobs: + op-bench: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + + - uses: actions/setup-node@v4 + with: + node-version: 20 + + - name: Build head benchmark + run: | + make -C native bench >/dev/null 2>&1 + cp /tmp/mf_test_bench /tmp/bench_head + + - name: Build base benchmark (head harness, base store sources) + id: base + run: | + BASE_SHA="${{ github.event.pull_request.base.sha }}" + git worktree add --detach /tmp/base "$BASE_SHA" + mkdir -p /tmp/base/native + # Overlay the head harness so ONLY the measured store code differs. + cp native/op_bench.c /tmp/base/native/op_bench.c + cp native/Makefile /tmp/base/native/Makefile + if make -C /tmp/base/native bench >/tmp/base_build.log 2>&1; then + cp /tmp/mf_test_bench /tmp/bench_base + echo "ok=1" >> "$GITHUB_OUTPUT" + else + echo "ok=0" >> "$GITHUB_OUTPUT" + echo "Base build failed — base likely has no comparable benchmark/store. Skipping comparison." + tail -25 /tmp/base_build.log || true + fi + + - name: Run interleaved and compare + if: steps.base.outputs.ok == '1' + id: cmp + run: | + for i in $(seq 1 5); do + /tmp/bench_head > "/tmp/head_$i.json" + /tmp/bench_base > "/tmp/base_$i.json" + done + H=$(ls /tmp/head_*.json | paste -sd,) + B=$(ls /tmp/base_*.json | paste -sd,) + set +e + node scripts/bench-compare.mjs --base "$B" --head "$H" > /tmp/report.md + echo "rc=$?" >> "$GITHUB_OUTPUT" + set -e + cat /tmp/report.md + + - name: Comment results on PR + if: steps.base.outputs.ok == '1' + uses: actions/github-script@v7 + with: + script: | + const fs = require('fs'); + const body = '\n' + fs.readFileSync('/tmp/report.md', 'utf8'); + const { owner, repo } = context.repo; + const issue_number = context.payload.pull_request.number; + const comments = await github.paginate(github.rest.issues.listComments, { owner, repo, issue_number }); + const existing = comments.find((c) => c.body && c.body.includes('')); + if (existing) { + await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body }); + } else { + await github.rest.issues.createComment({ owner, repo, issue_number, body }); + } + + - name: Soft-fail on regression + if: steps.base.outputs.ok == '1' && steps.cmp.outputs.rc != '0' + run: | + echo "::warning::Per-op benchmark regression detected — see the op-bench PR comment. (soft-fail: not a required check)" + exit 1 diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml new file mode 100644 index 0000000..e1516a2 --- /dev/null +++ b/.github/workflows/proofs.yml @@ -0,0 +1,49 @@ +name: proofs + +# Frama-C/WP proofs of the v3 store's tractable algorithms: allocator size +# quantization + open-addressing probe (fc_proofs), name-index traversal bounds +# (fc_index), free-list descent memory-safety (fc_tree), and the adjacency edge +# encoding round-trip/injectivity + edge-iteration bounds (fc_graph). These prove +# memory-model-clean abstractions of the real algorithms — no mmap region for WP +# to reason about. Only runs when the proofs (or their build) change. +on: + pull_request: + paths: + - 'native/fc_*.c' + - 'native/fc_stubs.h' + - 'native/Makefile' + - '.github/workflows/proofs.yml' + push: + branches: [master] + paths: + - 'native/fc_*.c' + - 'native/fc_stubs.h' + - 'native/Makefile' + - '.github/workflows/proofs.yml' + +permissions: + contents: read + +jobs: + wp: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: "5.2" + + - name: Install Frama-C + Alt-Ergo + run: opam install -y frama-c alt-ergo + + - name: Detect provers + run: | + eval $(opam env) + why3 config detect + + - name: Run WP proofs + run: | + eval $(opam env) + frama-c -version + make -C native proofs diff --git a/native/Makefile b/native/Makefile index 85c870d..e580290 100644 --- a/native/Makefile +++ b/native/Makefile @@ -11,7 +11,7 @@ CFLAGS = -std=c11 -g -O1 -Wall -Wextra -fsanitize=address,undefined \ LIBS = -lm OUT = /tmp/mf_test -.PHONY: test verify-detector test_memfile test_stringtable test_graph test_entity clean +.PHONY: test verify-detector test_memfile test_stringtable test_graph test_entity bench proofs proofs-eva clean # `make test` = prove the detector fires, then run every harness with it active. test: verify-detector test_memfile test_stringtable test_graph test_entity @@ -34,5 +34,28 @@ test_graph: test_graph.c graph.c stringtable.c memoryfile.c test_entity: test_entity.c $(CC) $(CFLAGS) $^ $(LIBS) -o $(OUT)_entity && $(OUT)_entity +# Per-op graph benchmark: optimized build (NO ASan / NO double-free-check — those +# skew timing). Emits per-op rdtsc cycle stats as JSON; CI compares base vs head. +BENCH_CFLAGS = -std=c11 -O2 -march=native -Wall -D_GNU_SOURCE -I. +bench: op_bench.c graph.c stringtable.c memoryfile.c + $(CC) $(BENCH_CFLAGS) $^ -lm -o $(OUT)_bench && $(OUT)_bench + +# ---- Frama-C/WP + EVA proofs ---------------------------------------------- +# Memory-model-clean abstractions in fc_*.c (NEVER compiled into the build): +# allocator size-quantization + open-addressing probe (fc_proofs), name-index +# traversal bounds (fc_index), free-list descent safety (fc_tree), adjacency +# edge encoding + edge-iteration bounds (fc_graph), and an EVA pass over the +# real allocator (fc_harness). frama-c + alt-ergo + z3 (CI installs via opam). +FRAMAC ?= frama-c + +# frama-c exits 0 even with unproved goals, so the gate (scripts/run-proofs.sh) +# parses the "Proved goals: P / T" summary: clean files must be 100%, fc_tree is +# safety-only (termination = documented acyclicity frontier). +proofs: + @FRAMAC="$(FRAMAC)" bash ../scripts/run-proofs.sh + +proofs-eva: fc_harness.c memoryfile.c + $(FRAMAC) -eva -main fc_main -cpp-extra-args="-include fc_stubs.h -I." $^ + clean: rm -f $(OUT)_* diff --git a/native/fc_graph.c b/native/fc_graph.c new file mode 100644 index 0000000..c4c00ed --- /dev/null +++ b/native/fc_graph.c @@ -0,0 +1,86 @@ +/* + * ACSL/WP: adjacency edge ENCODING + edge-iteration bounds for the v3 graph store. + * Every traversal (neighbors, find_path, edges, remove_edge) decodes adjacency + * entries via this packing and walks the adjacency block, so both are load-bearing. + * + * frama-c -wp -wp-rte -wp-prover alt-ergo,z3 fc_graph.c + * + * 1) adj_pack / adj_pack_injective: a target offset and a 2-bit direction share one + * u64, ((target<<2)|dir). Proved a ROUND-TRIP (unpack o pack == identity) and + * INJECTIVE, given target fits in 62 bits and dir < 4 — no high-offset truncation, + * no two distinct (target,dir) pairs aliasing to the same packed word. + * 2) read_edges_model: iterating n = min(count,max) 24-byte entries at + * adj + 8 + i*24 (the real ADJ_HEADER_SIZE / ADJ_ENTRY_SIZE) is memory-safe — + * every 24-byte access in-bounds — and terminating, given the block fits. + * + * Reads go through spec'd accessors (rd32/rd64); the real code reads via memcpy for + * aliasing safety, so modeling the read with an in-bounds contract keeps the proof + * about the OFFSET ARITHMETIC, not libc memcpy separation (same idiom as fc_index). + */ +#include + +#define ADJ_HEADER_SIZE 8u +#define ADJ_ENTRY_SIZE 24u +#define DIR_MASK 3u +#define TARGET_MAX 0x3fffffffffffffffULL /* 2^62 - 1: survives << 2 losslessly */ + +/* ---- 1. adjacency encoding: round-trip + injectivity (pure arithmetic) ---- */ + +/* The real encoding is ((target<<2)|(dir&3u)). With dir < 4 the two fields occupy + * disjoint bit ranges, so it equals target*4 + dir exactly — and target < 2^62 + * means the shift never truncates. We prove the ALGORITHM (lossless round-trip + + * injectivity) over that arithmetic form; decode >>2 / &3 are the unsigned /4 / %4 + * proved below. Same abstraction boundary as fc_index modeling hash32 % bc. */ +/*@ requires target <= TARGET_MAX; + @ requires dir <= DIR_MASK; + @ assigns \nothing; + @ ensures \result == target * 4 + dir; + @ ensures \result / 4 == target; // decode target (== packed >> 2) + @ ensures \result % 4 == dir; // decode direction(== packed & 3) + @*/ +uint64_t adj_pack(uint64_t target, uint64_t dir) { + return target * 4 + dir; +} + +/*@ requires t1 <= TARGET_MAX && d1 <= DIR_MASK; + @ requires t2 <= TARGET_MAX && d2 <= DIR_MASK; + @ assigns \nothing; + @ ensures \result != 0 <==> (t1 == t2 && d1 == d2); + @*/ +int adj_pack_injective(uint64_t t1, uint64_t d1, uint64_t t2, uint64_t d2) { + return adj_pack(t1, d1) == adj_pack(t2, d2); +} + +/* ---- 2. edge-iteration bounds (real adj-block offset arithmetic) ---- */ + +/*@ requires o + 8 <= msize; + @ requires \valid_read(mem + (0 .. msize - 1)); + @ assigns \nothing; */ +uint64_t rd64(unsigned char *mem, uint64_t msize, uint64_t o); + +/*@ requires o + 4 <= msize; + @ requires \valid_read(mem + (0 .. msize - 1)); + @ assigns \nothing; */ +uint32_t rd32(unsigned char *mem, uint64_t msize, uint64_t o); + +/*@ requires \valid_read(mem + (0 .. msize - 1)); + @ requires n <= count; + @ requires adj + ADJ_HEADER_SIZE + (uint64_t)count * ADJ_ENTRY_SIZE <= msize; + @ assigns \nothing; + @*/ +void read_edges_model(unsigned char *mem, uint64_t msize, uint64_t adj, + uint32_t count, uint32_t n) { + /*@ loop invariant 0 <= i <= n; + @ loop assigns i; + @ loop variant n - i; + @*/ + for (uint32_t i = 0; i < n; i++) { + uint64_t base = adj + ADJ_HEADER_SIZE + (uint64_t)i * ADJ_ENTRY_SIZE; + //@ assert base + ADJ_ENTRY_SIZE <= msize; + uint64_t packed = rd64(mem, msize, base + 0); + uint32_t rel = rd32(mem, msize, base + 8); + uint64_t mtime = rd64(mem, msize, base + 16); + //@ assert (packed >> 2) <= TARGET_MAX; // decoded target always in packable range + (void)packed; (void)rel; (void)mtime; + } +} diff --git a/native/op_bench.c b/native/op_bench.c new file mode 100644 index 0000000..db48a39 --- /dev/null +++ b/native/op_bench.c @@ -0,0 +1,197 @@ +/* + * Per-op microbench for the v3 graph store. rdtsc cycles/op over a fixed, seeded + * graph; emits a per-op distribution as JSON on stdout for base-vs-head CI + * regression comparison (no committed baselines — see scripts/bench-compare). + * + * make bench # -O2 -march=native, NO ASan / NO double-free-check + * /tmp/mf_test_bench [N] [seed] + * + * Adaptive sampling (ported from riff/benches/lcs_bench.rs, governed by + * Heuristic_MicrobenchAreStatistical): instead of a hand-tuned fixed iteration + * count per op, each op is sampled until the relative standard error of the mean + * RE = CV/sqrt(n) (CV = stddev/mean) drops below TARGET_RE, or a sample/budget cap + * is hit. Each sample is a BATCH-MEAN (time over B iterations / B): single-op + * times have fat tails (scheduler/cache outliers) that make CV explode, but the + * CV of batch-means is well-behaved, which is what makes the RE criterion sound. + * riff persists per-op counts across runs because Criterion can't grow sample_size + * mid-run; this harness can, so it resolves the target error in-run (stateless). + * + * Reported per op: min/p50/p90/p99/mean (cycles/op) + achieved n + re. p50 (median) + * is the headline comparison metric: robust to tails and representative of typical + * ("average") cost; min/p90/p99 give the floor and tail for context. + */ +#ifndef _GNU_SOURCE +#define _GNU_SOURCE +#endif +#include +#include +#include +#include +#include +#include +#include "graph.h" + +static inline u64 tsc_begin(void) { + unsigned a, d; __asm__ __volatile__("lfence\n\trdtsc" : "=a"(a), "=d"(d)); return ((u64)d << 32) | a; +} +static inline u64 tsc_end(void) { + unsigned a, d; __asm__ __volatile__("rdtscp" : "=a"(a), "=d"(d) :: "ecx"); + __asm__ __volatile__("lfence" ::: "memory"); return ((u64)d << 32) | a; +} + +static u64 rng; +static inline u64 xs(void) { u64 x = rng; x ^= x << 13; x ^= x >> 7; x ^= x << 17; return rng = x; } + +/* Frequency reference: fixed compute+memory work. Its cycles track the run's CPU + * frequency (invariant TSC counts wall-clock), so dividing op cost by the + * reference cancels the GLOBAL frequency/turbo factor that otherwise makes the + * same code look 5-13% different run-to-run. The compare script does the math. */ +static u32 g_refbuf[4096]; +static u64 reference_work(void) { + u64 acc = 0; + for (int j = 0; j < 1024; j++) { u64 r = xs(); acc += g_refbuf[r & 4095]; g_refbuf[r & 4095] = (u32)(acc ^ r); } + return acc; +} + +/* Adaptive-sampling tunables (mirror riff's TARGET_RE_UPPER / clamps). */ +#define POOL 4096u +#define POOL_MASK (POOL - 1u) +static const double TARGET_RE = 0.02; /* stop when RE = CV/sqrt(n) <= 2% */ +static const double TARGET_BATCH = 20000.0; /* aim each batch ~20k cycles to amortize rdtsc */ +static const size_t MIN_SAMPLES = 30; +static const size_t MAX_SAMPLES = 2000; +static const u64 BUDGET_CYC = 80000000ull; /* per-op wall cap (~30ms @2.6GHz) for O(N) ops */ + +static int cmp_d(const void *a, const void *b) { double x = *(const double *)a, y = *(const double *)b; return (x > y) - (x < y); } + +static int g_first = 1; +/* Compute distribution + RE from the collected batch-mean samples and emit JSON. */ +static void emit_op(const char *name, double *s, size_t n) { + double mean = 0; for (size_t i = 0; i < n; i++) mean += s[i]; mean /= (double)n; + double var = 0; for (size_t i = 0; i < n; i++) { double d = s[i] - mean; var += d * d; } + var /= (n > 1) ? (double)(n - 1) : 1.0; + double cv = (mean > 0.0) ? sqrt(var) / mean : 0.0; + double re = cv / sqrt((double)n); + qsort(s, n, sizeof(double), cmp_d); + size_t p90 = (size_t)(n * 0.90); if (p90 >= n) p90 = n - 1; + size_t p99 = (size_t)(n * 0.99); if (p99 >= n) p99 = n - 1; + printf("%s \"%s\": {\"min\": %.1f, \"p50\": %.1f, \"p90\": %.1f, \"p99\": %.1f, \"mean\": %.1f, \"n\": %zu, \"re\": %.4f}", + g_first ? "" : ",\n", name, s[0], s[n / 2], s[p90], s[p99], mean, n, re); + g_first = 0; +} + +/* Sample __VA_ARGS__ (a statement using `_k` to index a precomputed input pool) + * in auto-sized batches until RE <= TARGET_RE, or n / cycle budget is exhausted. */ +#define ADAPT(NAME, ...) do { \ + u64 _wmin = ~0ull, _wtot = 0; int _wi = 0; \ + while (_wi < 256 && _wtot < 2000000ull) { size_t _k = (size_t)_wi & POOL_MASK; (void)_k; \ + u64 _a = tsc_begin(); __VA_ARGS__; u64 _b = tsc_end(); u64 _e = _b - _a; \ + _wtot += _e; if (_e < _wmin) _wmin = _e; _wi++; } \ + double _c = (double)_wmin; if (_c < 1.0) _c = 1.0; \ + size_t _B = (size_t)(TARGET_BATCH / _c); if (_B < 1) _B = 1; if (_B > POOL) _B = POOL; \ + double _mean = 0, _m2 = 0, _re = 1.0; size_t _n = 0; u64 _tot = 0; \ + while (_n < MAX_SAMPLES) { \ + u64 _t0 = tsc_begin(); \ + for (size_t _i = 0; _i < _B; _i++) { size_t _k = (_n * _B + _i) & POOL_MASK; (void)_k; __VA_ARGS__; } \ + u64 _t1 = tsc_end(); _tot += (_t1 - _t0); \ + double _s = (double)(_t1 - _t0) / (double)_B; samp[_n] = _s; \ + double _d = _s - _mean; _mean += _d / (double)(_n + 1); _m2 += _d * (_s - _mean); _n++; \ + if (_n >= MIN_SAMPLES) { \ + double _var = _m2 / (double)(_n - 1); \ + double _cv = (_mean > 0.0) ? sqrt(_var) / _mean : 0.0; \ + _re = _cv / sqrt((double)_n); \ + if (_re <= TARGET_RE || _tot >= BUDGET_CYC) break; \ + } \ + } \ + emit_op(NAME, samp, _n); \ +} while (0) + +int main(int argc, char **argv) { + cpu_set_t set; CPU_ZERO(&set); CPU_SET(0, &set); sched_setaffinity(0, sizeof set, &set); + size_t N = (argc > 1) ? strtoul(argv[1], NULL, 10) : 2000; + rng = (argc > 2) ? strtoull(argv[2], NULL, 10) : 0x9e3779b97f4a7c15ull; + + const char *gp = "/tmp/opbench.graph", *sp = "/tmp/opbench.strings"; + unlink(gp); unlink(sp); + stringtable_t *st = st_open(sp, 1u << 20); + graph_t *g = graph_open(gp, st, 1u << 20); + + u64 *off = malloc(N * sizeof(u64)); + char nm[32], ty[32], ob[64]; + const u64 now = 1700000000000ull; + + for (size_t i = 0; i < N; i++) { + int nl = snprintf(nm, sizeof nm, "ent-%zu", i); + int tl = snprintf(ty, sizeof ty, "type-%zu", i % 20); + off[i] = graph_create_entity(g, (const u8 *)nm, (u16)nl, (const u8 *)ty, (u16)tl, now); + int ol = snprintf(ob, sizeof ob, "obs-a-%zu", i); graph_add_observation(g, off[i], (const u8 *)ob, (u16)ol, now); + ol = snprintf(ob, sizeof ob, "obs-b-%zu", i); graph_add_observation(g, off[i], (const u8 *)ob, (u16)ol, now); + } + for (size_t i = 0; i < N; i++) { + for (int k = 0; k < 3; k++) { + size_t j = xs() % N; if (j == i) continue; + int rl = snprintf(nm, sizeof nm, "rel-%llu", (unsigned long long)(xs() % 8)); + graph_create_relation(g, off[i], off[j], (const u8 *)nm, (u16)rl, now); + } + } + + /* Precompute input pools so the timed regions contain ONLY the op (no per-iter + * snprintf/rng inside timing), which lets us batch cleanly. */ + size_t *idx = malloc(POOL * sizeof *idx); + size_t *idx2 = malloc(POOL * sizeof *idx2); + size_t *tpix = malloc(POOL * sizeof *tpix); + u64 *seed = malloc(POOL * sizeof *seed); + char **pat = malloc(POOL * sizeof *pat); + for (u32 k = 0; k < POOL; k++) { + idx[k] = xs() % N; idx2[k] = xs() % N; tpix[k] = xs() % 20; seed[k] = xs(); + char *p = malloc(32); snprintf(p, 32, "ent-%llu$", (unsigned long long)(xs() % N)); pat[k] = p; + } + char **names = malloc(N * sizeof *names); u16 *nlen = malloc(N * sizeof *nlen); + for (size_t i = 0; i < N; i++) { char *p = malloc(24); int l = snprintf(p, 24, "ent-%zu", i); names[i] = p; nlen[i] = (u16)l; } + char *tynames[20]; u16 tylen[20]; + for (int t = 0; t < 20; t++) { char *p = malloc(16); int l = snprintf(p, 16, "type-%d", t); tynames[t] = p; tylen[t] = (u16)l; } + + printf("{\n \"graph\": {\"entities\": %zu, \"relations\": %u},\n \"ops\": {\n", N, graph_relation_count(g)); + + double *samp = malloc((MAX_SAMPLES > 2048 ? MAX_SAMPLES : 2048) * sizeof *samp); + u32 cap = (u32)N + 4; u64 *out = malloc((size_t)cap * 8); + entity_t e; + volatile u64 sink = 0; volatile u32 sink32 = 0; (void)sink; (void)sink32; + + ADAPT("reference", sink = reference_work()); + ADAPT("lookup", sink = graph_lookup(g, (const u8 *)names[idx[_k]], nlen[idx[_k]])); + ADAPT("read_entity", graph_read_entity(g, off[idx[_k]], &e)); + ADAPT("neighbors_d1", sink32 = graph_neighbors(g, off[idx[_k]], 1, DIR_ANY, out, cap)); + ADAPT("neighbors_d2", sink32 = graph_neighbors(g, off[idx[_k]], 2, DIR_ANY, out, cap)); + ADAPT("find_path_d6", sink32 = graph_find_path(g, off[idx[_k]], off[idx2[_k]], 6, DIR_ANY, out, cap)); + ADAPT("search", sink32 = graph_search(g, pat[_k], out, cap)); + ADAPT("entities_by_type", sink32 = graph_entities_by_type(g, (const u8 *)tynames[tpix[_k]], tylen[tpix[_k]], out, cap)); + ADAPT("random_walk_d5", sink32 = graph_random_walk(g, off[idx[_k]], 5, DIR_ANY, 1, seed[_k], out, 8)); + ADAPT("inc_walker_visit", graph_inc_walker_visit(g, off[idx[_k]])); + ADAPT("structural_sample", graph_structural_sample(g, 1, 0.85)); + ADAPT("compute_merw_psi", graph_compute_merw_psi(g, 0.85, 100, 1e-8)); + + /* Mutating ops: non-stationary (each call grows the graph), so they can't be + * batch-sampled i.i.d. Keep a fixed single-op timed count; report distribution. */ + const size_t KM = 2000; + u64 *noff = malloc(KM * sizeof *noff); + for (size_t i = 0; i < KM; i++) { int nl = snprintf(nm, sizeof nm, "new-%zu", i); + u64 t0 = tsc_begin(); u64 r = graph_create_entity(g, (const u8 *)nm, (u16)nl, (const u8 *)"NewType", 7, now); u64 t1 = tsc_end(); + noff[i] = r; samp[i] = (double)(t1 - t0); } + emit_op("create_entity", samp, KM); + + for (size_t i = 0; i < KM; i++) { u64 a = noff[i], b = noff[xs() % KM]; + u64 t0 = tsc_begin(); graph_create_relation(g, a, b, (const u8 *)"newrel", 6, now); u64 t1 = tsc_end(); + samp[i] = (double)(t1 - t0); } + emit_op("create_relation", samp, KM); + + printf("\n }\n}\n"); + + for (u32 k = 0; k < POOL; k++) free(pat[k]); + for (size_t i = 0; i < N; i++) free(names[i]); + for (int t = 0; t < 20; t++) free(tynames[t]); + free(idx); free(idx2); free(tpix); free(seed); free(pat); free(names); free(nlen); + free(samp); free(out); free(off); free(noff); + graph_close(g); st_close(st); + return 0; +} diff --git a/scripts/bench-aggregate.mjs b/scripts/bench-aggregate.mjs new file mode 100644 index 0000000..62210ad --- /dev/null +++ b/scripts/bench-aggregate.mjs @@ -0,0 +1,41 @@ +#!/usr/bin/env node +/* + * Aggregate N op-bench run JSONs into ONE sample line for the bench-history + * NDJSON time-series. Keeps the `reference` op value alongside the per-op medians + * so downstream creep analysis can frequency-normalize across runners and time. + * + * node scripts/bench-aggregate.mjs --runs r1.json,r2.json,... --sha --date [--metric min] + * + * Emits one line: {"sha","date","reference",,"ops":{op:,...}} + */ +import { readFileSync } from 'fs'; + +function flag(name, def) { + const i = process.argv.indexOf(name); + return i >= 0 ? process.argv[i + 1] : def; +} +const files = (flag('--runs', '') || '').split(',').filter(Boolean); +const sha = flag('--sha', 'unknown'); +const date = flag('--date', 'unknown'); +const metric = flag('--metric', 'p50'); +if (!files.length) { + console.error('usage: bench-aggregate --runs r1.json[,r2,...] --sha --date [--metric min]'); + process.exit(2); +} + +function median(a) { + const s = [...a].sort((x, y) => x - y); + const n = s.length; + if (!n) return 0; + return n % 2 ? s[(n - 1) / 2] : (s[n / 2 - 1] + s[n / 2]) / 2; +} + +const runs = files.map((f) => JSON.parse(readFileSync(f, 'utf8')).ops); +const ops = {}; +for (const op of Object.keys(runs[0])) { + ops[op] = median(runs.map((r) => r[op]?.[metric]).filter((x) => x != null)); +} +const reference = ops.reference || 0; +delete ops.reference; + +process.stdout.write(`${JSON.stringify({ sha, date, reference, ops })}\n`); diff --git a/scripts/bench-compare.mjs b/scripts/bench-compare.mjs new file mode 100644 index 0000000..461c9e9 --- /dev/null +++ b/scripts/bench-compare.mjs @@ -0,0 +1,83 @@ +#!/usr/bin/env node +/* + * Compare op-bench JSON outputs (from native/op_bench), base vs head, and flag + * per-op regressions. No committed baselines: CI runs the SAME harness against + * base and head graph sources on one runner, interleaved N times, and diffs. + * + * node scripts/bench-compare.mjs --base b1.json,b2.json --head h1.json,h2.json + * [--pct 5] [--cyc 40] [--metric min] + * + * Methodology (for noisy shared CI runners): + * - Each side may have N runs; we take the MEDIAN of the per-run `min` per op. + * - We FREQUENCY-CORRECT head to base using the `reference` op (fixed work): + * invariant TSC counts wall-clock, so the reference's cycles track CPU + * frequency; scaling head by ref_base/ref_head cancels the global turbo drift + * that makes identical code look 5-13% different. + * Exits 1 if any op regressed beyond max(cyc, pct%) — wire to a SOFT-fail check. + */ +import { readFileSync } from 'fs'; + +function flag(name, def) { + const i = process.argv.indexOf(name); + return i >= 0 ? process.argv[i + 1] : def; +} +const baseFiles = (flag('--base', '') || '').split(',').filter(Boolean); +const headFiles = (flag('--head', '') || '').split(',').filter(Boolean); +if (!baseFiles.length || !headFiles.length) { + console.error('usage: bench-compare --base b1.json[,b2,...] --head h1.json[,h2,...] [--pct N] [--cyc N] [--metric min|p50]'); + process.exit(2); +} +const pct = Number(flag('--pct', '5')); +const cycFloor = Number(flag('--cyc', '40')); // ~15 ns at ~2.6 GHz +const metric = flag('--metric', 'p50'); + +function median(a) { + const s = [...a].sort((x, y) => x - y); + const n = s.length; + if (!n) return 0; + return n % 2 ? s[(n - 1) / 2] : (s[n / 2 - 1] + s[n / 2]) / 2; +} +function mergeRuns(files) { + const runs = files.map((f) => JSON.parse(readFileSync(f, 'utf8')).ops); + const out = {}; + for (const op of Object.keys(runs[0])) { + out[op] = median(runs.map((r) => r[op]?.[metric]).filter((x) => x != null)); + } + return out; +} + +const base = mergeRuns(baseFiles); +const head = mergeRuns(headFiles); + +// Frequency-correct head -> base via the reference op. +const corr = base.reference && head.reference ? base.reference / head.reference : 1; + +let regressed = false; +const rows = []; +for (const op of Object.keys(head)) { + if (op === 'reference') continue; + if (!(op in base)) { rows.push({ op, isNew: true }); continue; } + const b = base[op]; + const h = Math.round(head[op] * corr); + const d = h - b; + const dp = b ? (100 * d / b) : 0; + const thr = Math.max(cycFloor, (b * pct) / 100); + const mark = d > thr ? '\u{1F534} REGRESSION' : d < -thr ? '\u{1F7E2} faster' : ''; + if (d > thr) regressed = true; + rows.push({ op, b, h, d, dp, mark }); +} + +console.log(`### Per-op benchmark — ${metric} cycles (base vs head)\n`); +console.log(`base runs: ${baseFiles.length}, head runs: ${headFiles.length} (median of mins) · ` + + `freq-correction ×${corr.toFixed(4)} · threshold head−base > max(${cycFloor} cyc, ${pct}%)\n`); +console.log('| op | base | head* | Δ | Δ% | |'); +console.log('|---|---:|---:|---:|---:|---|'); +for (const r of rows) { + if (r.isNew) { console.log(`| \`${r.op}\` | — | — | — | — | new |`); continue; } + const sd = `${r.d >= 0 ? '+' : ''}${r.d.toFixed(1)}`; + const sp = `${r.dp >= 0 ? '+' : ''}${r.dp.toFixed(1)}%`; + console.log(`| \`${r.op}\` | ${r.b} | ${r.h} | ${sd} | ${sp} | ${r.mark} |`); +} +console.log(`\n\\* head frequency-corrected to base via the \`reference\` op.`); +console.log(regressed ? '\n**Regressions detected.**' : '\n_No regressions beyond threshold._'); +process.exit(regressed ? 1 : 0); diff --git a/scripts/bench-creep.mjs b/scripts/bench-creep.mjs new file mode 100644 index 0000000..17c90be --- /dev/null +++ b/scripts/bench-creep.mjs @@ -0,0 +1,89 @@ +#!/usr/bin/env node +/* + * Slow-creep detector for the bench-history NDJSON time-series. The per-PR gate + * (bench-compare) only sees head-vs-base, so a change that adds a sliver per PR + * compounds invisibly. This compares the newest sample's reference-NORMALIZED + * per-op cost (op/reference — frequency-independent across runners and time) + * against a rolling baseline (median over a recent window of history). + * + * node scripts/bench-creep.mjs --history history.ndjson [--sample sample.json] + * [--pct 10] [--window 20] + * + * With --sample, that sample is the "now" and the whole file is the baseline. + * Without it, the last line of history is "now" and the rest is the baseline. + * Exits 1 if any op drifted > pct% above the rolling median (soft-fail signal). + */ +import { readFileSync } from 'fs'; + +function flag(name, def) { + const i = process.argv.indexOf(name); + return i >= 0 ? process.argv[i + 1] : def; +} +const histFile = flag('--history', ''); +const sampleFile = flag('--sample', ''); +const pct = Number(flag('--pct', '10')); +const cycFloor = Number(flag('--cyc', '40')); // absolute floor: ignore sub-noise wiggle on tiny ops +const windowN = Number(flag('--window', '20')); +if (!histFile) { + console.error('usage: bench-creep --history history.ndjson [--sample sample.json] [--pct N] [--window N]'); + process.exit(2); +} + +const lines = readFileSync(histFile, 'utf8').split('\n').filter(Boolean).map((l) => JSON.parse(l)); +let sample; +let baseline; +if (sampleFile) { + sample = JSON.parse(readFileSync(sampleFile, 'utf8')); + baseline = lines; +} else { + sample = lines[lines.length - 1]; + baseline = lines.slice(0, -1); +} +if (!sample || !baseline.length) { + console.log('No prior history — creep check skipped (first sample establishes the baseline).'); + process.exit(0); +} + +function median(a) { + const s = [...a].sort((x, y) => x - y); + const n = s.length; + if (!n) return 0; + return n % 2 ? s[(n - 1) / 2] : (s[n / 2 - 1] + s[n / 2]) / 2; +} +// reference-normalize: op cost as a fraction of the fixed-work reference op. +function normalize(s) { + const o = {}; + for (const k of Object.keys(s.ops)) o[k] = s.reference ? s.ops[k] / s.reference : s.ops[k]; + return o; +} + +const win = baseline.slice(-windowN).map(normalize); +const now = normalize(sample); + +// Convert a normalized delta back to approximate cycles at this sample's +// frequency, so a tiny op's large % wiggle below the absolute floor is ignored. +const refNow = sample.reference || 1; +let creep = false; +const rows = []; +for (const op of Object.keys(now)) { + const base = median(win.map((w) => w[op]).filter((x) => x != null)); + if (!base) continue; + const c = now[op]; + const dp = (100 * (c - base)) / base; + const dcyc = (c - base) * refNow; + const isCreep = dp > pct && dcyc > cycFloor; + const isFaster = dp < -pct && -dcyc > cycFloor; + const mark = isCreep ? '\u{1F534} CREEP' : isFaster ? '\u{1F7E2} improved' : ''; + if (isCreep) creep = true; + rows.push({ op, base, c, dp, dcyc, mark }); +} + +console.log(`### Bench creep — normalized cost vs ${win.length}-sample rolling baseline\n`); +console.log(`sample: \`${String(sample.sha || '').slice(0, 9)}\` (${sample.date || '?'}) · flag drift > ${pct}% AND > ${cycFloor} cyc above rolling median\n`); +console.log('| op | baseline | now | Δ% | Δcyc | |'); +console.log('|---|---:|---:|---:|---:|---|'); +for (const r of rows) { + console.log(`| \`${r.op}\` | ${r.base.toFixed(4)} | ${r.c.toFixed(4)} | ${r.dp >= 0 ? '+' : ''}${r.dp.toFixed(1)}% | ${r.dcyc >= 0 ? '+' : ''}${Math.round(r.dcyc)} | ${r.mark} |`); +} +console.log(creep ? '\n**Creep detected.**' : '\n_No creep beyond threshold._'); +process.exit(creep ? 1 : 0); diff --git a/scripts/run-proofs.sh b/scripts/run-proofs.sh new file mode 100755 index 0000000..801c68d --- /dev/null +++ b/scripts/run-proofs.sh @@ -0,0 +1,46 @@ +#!/usr/bin/env bash +# Frama-C/WP proof gate for the v3 store. +# +# frama-c exits 0 even when WP goals are unproved, so we PARSE the per-file +# "Proved goals: P / T" summary and gate on it: +# - clean files must be FULLY proved (P == T); +# - fc_tree is safety-only — mf_fit_model's termination needs an acyclicity +# measure (the documented free-list-cycle frontier), so we require its +# safety/functional goals only (P >= 12) and tolerate the 1 terminates goal. +# +# Run from anywhere; CI calls it via `make -C native proofs`. +set -u +cd "$(dirname "$0")/../native" || exit 2 +FRAMAC="${FRAMAC:-frama-c}" +FLAGS=(-wp -wp-rte -wp-prover alt-ergo -wp-timeout 30) +rc=0 + +gate() { # file mode(strict|min) [minval] + local f=$1 mode=$2 min=${3:-0} + echo "===== $f =====" + local out line + out=$("$FRAMAC" "${FLAGS[@]}" "$f" 2>&1) + line=$(echo "$out" | grep -m1 'Proved goals' || true) + echo " ${line:-}" + if [ -z "$line" ]; then echo " FAIL: no proof summary for $f"; rc=1; return; fi + # shellcheck disable=SC2046 + set -- $(echo "$line" | grep -oE '[0-9]+ / [0-9]+' | tr '/' ' ') + local p=${1:-0} t=${2:-0} + if [ "$mode" = strict ]; then + if [ "$p" != "$t" ]; then + echo " FAIL: $f proved $p/$t (expected all)" + echo "$out" | grep -i 'Timeout\]' | sed 's/^/ /' + rc=1 + fi + else + if [ "$p" -lt "$min" ]; then echo " FAIL: $f proved $p < $min safety goals"; rc=1; fi + fi +} + +gate fc_proofs.c strict +gate fc_index.c strict +gate fc_graph.c strict +gate fc_tree.c min 12 # safety-only; termination = documented acyclicity frontier + +if [ "$rc" = 0 ]; then echo "ALL PROOF GATES PASSED"; fi +exit "$rc"