Brummel
4ec8f90b19
Third tranche, completing the honesty-rule sweep across the remaining
contracts. Same conservative bar: cut unbacked-verification claims,
change/deletion history, and forward-intent; keep present-state design
rationale.
- 0003: drop "sanitiser-verified" — no TSan/sanitiser test exists in
the tree, so the claim asserts a verification that does not happen.
The data-race-freedom property (argued from the non-atomic-but-never-
shared hot path + atomic-relaxed shared counter) stays.
- 0008: the `Type::Con.name` hash paragraph ("the tightening shifted
the hashes ... The new pins ... re-asserts the pre-tightening hashes")
-> present-state: which fixtures carry which hash shape and which test
pins each.
- 0013: drop "the former codegen-side fallback (at ..., and the
now-deleted `synth_with_extras`) is retracted" (deletion history; the
present fact is that codegen does not re-resolve, per the boundary);
"A future refactor that loosens any one of the four breaks ..." ->
present-tense statement that the four are load-bearing and each pinned.
- 0017: drop "a real cost surfaced by the `bench_closure_chain`
regression at the operator-routing-eq-ord milestone" (history) and
"the symmetric extensions are mechanical when the first such workload
appears" (forward-intent); keep the present-state allocation cost, the
pin, and the Int-only-asymmetry rationale.
All 18 contracts now reviewed against the code. Ledger pins green;
honesty sweep clean.
3.4 KiB
Embedding ABI
Embedding ABI
ail build --emit=staticlib compiles a module to a relocatable
lib<entry>.a (program objects only) plus a separate
libailang_rt.a (the RC runtime: rc.c + str.c), with no
@main trampoline and no MissingEntryMain requirement — a
kernel module is a library.
Each fn carrying (export "<sym>") (schema: FnDef.export) is
emitted as an externally-visible C entrypoint @<sym> forwarding to
the internal @ail_<module>_<fn>. The symbol is author-chosen and
decoupled from the ail_<module>_<def> mangling so a module/fn
rename does not move the C symbol.
The set that can cross the boundary is exactly: Int (lowered
i64), Float (lowered double), or a single-constructor record
whose every field is one of those (crossing as a bare ptr to the
box layout below); the fn's effect set must be empty. There is no
general value-marshalling layer — the host hand-constructs and
hand-reads that box layout directly, so the enumerated set is the
whole contract, narrow by construction, not a subset of a wider
embedding ABI. Because the box layout is the host's contract
surface with no accessor indirection, it is a one-way commitment
frozen as of M3: a compiler change MUST NOT move the box offsets
below for an exported type, nor invert the host-free rule.
These are enforced at ail check (export-non-scalar-signature,
export-has-effects) — an effectful or non-scalar export fails to
typecheck. Every exported entrypoint takes a mandatory leading ailang_ctx_t*
(M2): a per-thread embedding context created by ailang_ctx_new()
and released by ailang_ctx_free(), owned by the calling thread for
its lifetime. The host links one ailang_ctx_t per OS worker thread
and the runtime accounts RC alloc/free into it: the per-allocation
hot path (the per-ctx counters and the per-object refcount header)
is non-atomic by design and never shared — a box never crosses a
thread (Ctx: !Send) and each ailang_ctx_t is
single-thread-per-ctx. The one datum a multi-threaded host shares
is the global RC-stats fallback counter (used when no ctx is
bound); it is atomic-relaxed so the swarm's leak accounting is
exact. The swarm artefact is data-race-free by this split.
The staticlib swarm artefact is RC-only:
ail build --emit=staticlib rejects --alloc=bump (the bench
stub is leak-only and not swarm-safe; --alloc=gc no longer
exists as a CLI value — see the Boehm-retirement iter). The
value/record
layout is frozen as of M3 (see Frozen value layout); the
ctx-threaded C signature is the M2 shape.
Export parameters are written bare: a scalar type carries no
own/borrow mode (a single-constructor record export parameter,
by contrast, carries own/borrow — see memory model
for the full ownership contract; the
frozen value layout below specifies how that contract lands at the C ABI). The
canonical M1 export shape:
(fn step
(export "backtest_step")
(type
(fn-type
(params (con Int) (con Int))
(ret (con Int))))
(params state sample)
(body
(app + state (app * sample sample))))
ail emit-ir <module> --emit=staticlib prints this kernel's LLVM
IR (the external @<sym> forwarders, no @main) instead of the
executable-path main-required rejection — the Decision-5
IR-readability affordance for a main-free kernel.
Ratified by: crates/ailang-codegen/tests/embed_record_layout_pin.rs.