Zachery Aaron Shores-Chmielewski f20876af86 feat: L1 prototype

2026-03-02 22:46:50 +07:00

35 KiB

Raw Permalink Blame History

Compiler Spec: L3 → L0

A four-layer compiler for ML training pipelines, from intent to bare metal.

Each layer is a closed DSL with finite forms. Each has its own IR suited to the decisions made at that level. Optimization happens between layers during lowering and within layers as IR→IR rewrites. Never at the DSL surface.

Lowering between layers is search: enumerate valid candidates at the target layer, score them, pick the best. If search is slow, the representation is wrong.

┌─────────────────────────────────────────────┐
│  L3 Spec          what you want             │
├───────────────── search ────────────────────┤
│  L2 Method        how, algorithmically      │
├───────────────── search ────────────────────┤
│  L1 Placement     where, on what            │
├───────────────── emit ──────────────────────┤
│  L0 Machine       explicit execution        │
├─────────────────────────────────────────────┤
│  Codegen          PTX / LLVM IR / x86 / ... │
└─────────────────────────────────────────────┘
        ↕ rewrites within each layer

Zen

Read little; write little
Correctness via DSL model, not assertions
Every stage as simple as possible; all mutations checkable
Unbounded execution = specification error
Optimize between stages, closer to machine; not at DSL level
Never sacrifice performance for correctness; change the representation
Specify via properties: liveness, safety, consistency, resource bounds

The last point is structural. Every verification table in this document classifies its checks under exactly these four property kinds. If a check doesn't fit one of them, it doesn't belong.

Property Definitions

Safety — references resolve, types match, nothing dangling. "You will not read garbage."

Consistency — declared constraints agree with each other and with structure. "Your spec doesn't contradict itself."

Liveness — every resource produced is consumed; every buffer freed; no dead allocations. "Nothing is wasted."

Resource bound — memory, compute, time, space are all finite and known. "You will not run forever or exhaust the machine."

Verification Without Solvers

The restricted DSL makes each check a specific algorithm. Conservation is a graph walk. Separation is set disjointness. Boundedness is constant arithmetic. If the DSL allowed recursion, unbounded loops, or dynamic allocation, we'd need SAT solvers. Because it doesn't, we don't.

L3: Spec

Purpose

Declare what you want. No algorithms, no hardware, no shapes beyond the data itself. This is a contract that all lower layers must satisfy.

DSL Forms

data <n> {
    <field> : <domain>
    ...
}

model <n> {
    in:         <data_ref>
    out:        <domain>
    properties: [<constraint>, ...]
}

loss <n> {
    <term_name> : <loss_kind>(<args>), weight: <float>
    ...
    combine: <combinator>
}

goal: minimize(<loss_ref>) | maximize(<ref>) | pareto([<refs>])

Domain Types

tensor(dtype, shape)        fixed shape
sequence(domain, max_len)   variable-length, bounded
table(col: domain, ...)     tabular
dist(n)                     probability distribution over n classes
scalar(dtype)               single value

Model Constraints

These are not implementations. They bound what L2 may produce.

depth(n)                    max composed stages
width(n)                    max hidden dimension
causal                      output_t depends only on input_≤t
autoregressive              output is fed back as input
equivariant(group)          symmetry constraint
param_budget(n)             max parameter count
latency_budget(ms)          max forward pass time (needs L1 info)

Loss Kinds

divergence(predicted, target)           ce, kl, etc. (choice is L2)
norm(target, p)                         Lp on params or activations
constraint(predicate)                   hard constraint → penalty
reconstruction(input, decoded)          autoencoders
contrastive(anchor, positive, negative) representation learning
custom(name, reads: [refs])             escape hatch, user-defined

IR

L3_IR = {
    data:   Map<Name, DataDecl>
    models: Map<Name, ModelDecl>
    losses: Map<Name, LossDecl>
    goal:   Goal
    hints:  Map<Path, EscapeHatch>
}

All refs resolved. All domains concrete. No optionals. A total description.

Verification

Property	Check	Catches
Safety	Ref resolution	Dangling references to data fields, model outputs
Consistency	Domain compatibility	Model input domain ≠ data field domain
Safety	Loss signature	Loss term reads something that doesn't exist
Consistency	Constraint agreement	`depth(2)` + `autoregressive` on feedforward output
Resource bound	Finiteness	Everything bounded, no recursion at this level

All checks decidable. All linear in program size.

Optimization

None. L3 is a spec. You don't optimize a spec. You may simplify it — merge redundant loss terms, canonicalize domains — but no semantic changes.

Trace — MNIST at L3

data mnist {
    images : tensor(f32, [28, 28])
    labels : tensor(u8, [1])
}

model classify {
    in:  mnist.images
    out: dist(10)
    properties: [depth(3), width(512), param_budget(500K)]
}

loss objective {
    ce:     divergence(classify.out, mnist.labels), weight: 1.0
    sparse: norm(classify.params, p=1),             weight: 1e-4
    combine: weighted_sum
}

goal: minimize(objective)

This is the entire program. Everything below exists to make it run.

L3 → L2 Lowering

Given an L3 spec, enumerate valid L2 programs and pick the best.

The search space is combinatorial over (sample) × (architecture) × (backward) × (update). Architecture is the big one — it's a DAG construction problem. The search is structured, not brute force:

From depth(3) + sequential: 3-layer chain. Width search over powers-of-2 up to width(n). If causal, only causal attention. If autoregressive, add feedback edges. Backward filtered by architecture compatibility. Update mostly independent. Sample constrained by data domain.

Cost model scores without lowering to L1: param count, FLOPs per step, memory high-water mark, known convergence priors.

If search produces >10K candidates: representation too loose. Add constraints at L3 or tighten the enumeration grammar.

L2: Method

Purpose

Choose how to achieve the spec. Algorithms, architecture, training strategy. Still no hardware, no memory, no scheduling.

DSL Forms

methods for <model_ref> {
    sample:   <sample_method>
    infer:    <infer_method>
    backward: <backward_method>
    update:   <update_method>
}

Sample Methods

epoch_shuffle(batch: n, drop_last: bool)
stream_window(window: n, stride: n)
curriculum([{ filter: <pred>, duration: n_steps }, ...])
replay(buffer: n, priority: <kind>)
distributed_shard(shards: n, method: <inner>)

Infer Methods (Architecture)

sequential([<layer>, ...])
residual([<block>, ...])
diffusion_chain(steps: n, noise: <schedule>, denoiser: <infer>)
recurrent(cell: <infer>, steps: n | until(<pred>))
graph(nodes: <infer>, edges: <adjacency>)
mixture(experts: [<infer>], gate: <infer>)

Layer Primitives

linear(in, out)
conv(in_ch, out_ch, kernel, stride, padding)
attn(heads, dim, causal: bool)
norm(kind: layer | group(n) | rms)
act(fn: relu | gelu | silu | swish)
embed(vocab, dim)
pool(kind: avg | max, kernel)
dropout(p)                                training only

Backward Methods

autodiff(mode: reverse | forward, checkpoint: [<layer_ref>])
evolution(pop: n, sigma: f, selection: <kind>)
dfa(feedback_dim: n)
reinforce(baseline: <kind>)
straight_through(estimator: <kind>)
zeroth_order(samples: n, sigma: f)
hybrid(primary: <backward>, aux: <backward>, blend: <schedule>)

autodiff is an L2 declaration. L2→L1 lowering expands it into an explicit backward DAG in the tensor graph. At L1 and below, forward and backward are both explicit — no compiler magic.

Update Methods

sgd(lr)
adam(lr, beta1, beta2, eps)
muon(lr, ns_steps)
lion(lr, beta1, beta2)
schedule(warmup: n, decay: <kind>, inner: <update>)
gradient_clip(max_norm: f, inner: <update>)
ema(decay: f, inner: <update>)

IR

L2_IR = {
    sample:   SampleNode
    infer:    InferGraph              DAG of layer nodes
    backward: BackwardDecl
    update:   UpdateChain
    shapes:   Map<NodeId, Shape>     propagated during verification
    hints:    Map<Path, EscapeHatch>
}

The InferGraph is a DAG, not a sequence. sequential and residual are sugar that lower into the DAG form. This makes fusion and rewrite uniform.

Key principle: recurrent(... steps: n) is finite. recurrent(... until(pred)) is a specification error unless pred is proven terminating with a maximum bound. We do not allow unbounded execution.

Verification

Property	Check	Catches
Consistency	Shape propagation	Mismatched shapes on infer DAG edges
Consistency	Spec constraint check	depth, width, param_budget violated
Consistency	Backward compatibility	Backward method can't handle infer graph structure
Consistency	Update shape match	Update produces params of wrong shape
Consistency	Sample/data match	Batch shape inconsistent with data domains
Resource bound	Finiteness	DAG is acyclic (recurrent unrolled to fixed depth)
Resource bound	Resource estimation	Rough FLOPs, memory — feeds L1 search cost model

Optimization (IR→IR rewrites)

Semantics-preserving transformations on L2 IR: layer fusion (linear → act becomes fused_linear_act), redundant norm elimination, checkpoint selection for memory/compute tradeoff, architecture search pruning of dominated candidates.

Trace — MNIST at L2

methods for classify {
    sample:   epoch_shuffle(batch: 128)

    infer: sequential [
        linear(784, 256), norm(layer), gelu,
        linear(256, 256), norm(layer), gelu,
        linear(256, 10),  softmax
    ]

    backward: autodiff(mode: reverse)
    update:   schedule(warmup: 1000, decay: cosine,
                       inner: adam(lr: 3e-4))
}

Search chose this from L3 constraints: 3-layer sequential (from depth(3)), widths 256 (under width(512)), ~200K params (under param_budget(500K)). softmax output satisfies dist(10).

L2 → L1 Lowering

Given an L2 method and a hardware description, produce a valid L1 placement. Search decides: which compute goes on which node, how to partition across accelerators, pipeline depth, where to stage data, whether to fuse or split stages.

Cost model uses hardware specs: transfer time = data_size / bandwidth, compute time = FLOPs / throughput, memory pressure = peak live tensors, pipeline bubble ratio = (depth − 1) / (depth × stages).

If placement search explodes, either the hardware description is too ambiguous or the L2 method has too many equivalent decompositions.

Three things happen during this lowering that don't happen at other boundaries:

Backward expansion. If L2 declares autodiff(mode: reverse), the lowering derives the backward pass and writes it as explicit tensor ops in the L1 tensor graph. At L1, no operation is implicit.
Update materialization. L2's adam(lr, beta1, beta2, eps) becomes an explicit actor handler with tensor arithmetic at L1.
Data binding. L3's abstract data declarations gain physical storage locations (@ ssd_0, path: "...").

L1: Placement

Purpose

Map the L2 method onto specific hardware. This is the layer where the systems-level DSL lives. It answers two questions: where does each computation live (topology + placement), and when does it execute (schedule + dataflow).

Six declaration forms: system, data, actor, stage, tensor_graph, pipeline. Plus a schedule block.

DSL Forms — Topology

system <n> {
    node <id> { kind: <storage|memory|compute>, <properties> }
    ...
    edges {
        <id> -> <id>  : bandwidth <rate>      // unidirectional
        <id> <-> <id> : bandwidth <rate>      // bidirectional
    }
}

Node kinds:

storage — persistent (SSD, disk). Source of data.
memory — volatile (RAM, HBM). Has capacity.
compute — processing (CPU, GPU). Has isa, and optionally vram, cores, sm, etc.

DSL Forms — Data Sources

data <n> {
    <field> : <domain> @ <storage_node>, path: <string>
    ...
}

Binds L3's abstract data declarations to physical storage. The @ annotation names the topology node where the data lives at rest.

DSL Forms — Actors

Actors own mutable state. They process messages one at a time — serialized, no concurrent access to their state.

actor <n> on <node> {
    state {
        <field> : <type>, <init>
        ...
    }

    window <n> : (<fields>)
        readers(<stage_or_graph_refs>)

    on <MessageType>(<args>) {
        <update logic>
    }
}

Windows grant read-only access to actor state from stages or tensor graphs. The actor's message handler is the only writer. Safety requires that readers and writers never execute concurrently — enforced by data dependency chains within a step and actor serialization across steps.

DSL Forms — Stages

Stages are stateless dataflow processors. They receive buffers, do work, and forward results. Every buffer received must be consumed exactly once — forwarded or freed. No exceptions.

stage <n> on <node> {
    reads: <refs>                          // optional window reads

    fn process(<args>) -> forward(<target>, <outputs>)
                        | Drop(<buf>) {
        <body>
    }
}

Buffer types carry region provenance: buf<ram_0>, buf<gpu_0>. Every forwarding site is checked: target exists, arity matches, types match, region provenance matches the target's placement.

DSL Forms — Tensor Graphs

Lazy DAGs of primitive tensor ops. Run on accelerators. No control flow, no mutation, no side effects — pure compute.

tensor_graph <n> on <node> {
    reads: <window_refs>

    fn compute(<inputs>) -> (<outputs>) {
        let t0 = tensor_matmul(x, w)
        let t1 = tensor_add(t0, tensor_broadcast(b, shape))
        ...
        return (loss, gw, gb)
    }
}

The reads clause grants access to actor state via a window — same mechanism as stages. The body is a sequence of let bindings over primitive tensor ops. No autodiff — both forward and backward are explicit. Movement ops (reshape, permute, broadcast) are free — metadata only.

Primitive tensor ops:

tensor_matmul(a, b)              matrix multiply
tensor_add(a, b)                 elementwise add
tensor_sub(a, b)                 elementwise subtract
tensor_mul(a, b)                 elementwise multiply
tensor_scale(a, scalar)          scalar multiply
tensor_broadcast(a, shape)       expand dimensions
tensor_transpose(a)              transpose
tensor_reduce_mean(a)            reduce mean (all axes)
tensor_reduce_sum(a, axis: n)    reduce sum on axis
tensor_const(v)                  scalar constant

DSL Forms — Pipelines

Ordered chains of stages and tensor graphs.

pipeline <n> {
    <stage_or_graph> -> <stage_or_graph> -> ...
}

DSL Forms — Schedule

schedule {
    pipelines: [<refs>]
    actors:    [<refs>]
    pipeline_depth: <n>
}

No explicit phases. Execution order is inferred from forward() edges — the dependency DAG. pipeline_depth controls overlap: at depth 2, step N+1's early stages can overlap with step N's late stages. The actor is the serialization fence between steps.

IR

L1_IR = {
    topology:      Graph<NodeId, Edge>           hardware graph
    data_sources:  Map<Name, DataDecl>
    placement:     Map<L2_NodeId, HW_NodeId>     where each computation lives
    actors:        Map<Name, ActorDecl>
    stages:        Map<Name, StageDecl>
    tensor_graphs: Map<Name, TensorDAG>          lazy compute DAGs
    pipelines:     [Pipeline]                    ordered stage/graph chains
    schedule:      ScheduleDecl
    hints:         Map<Path, EscapeHatch>
}

Every cross-reference is resolved during parsing. demux reading connection_manager.routes becomes a pointer within the tree. If a name is unresolved, the parser rejects. If a syntax rule is violated, the parser rejects. Semantic validity is the verifier's job.

Verification — Structural (Phase 1)

Reads the IR. Does not transform it. If it also rewrote things, we'd need to verify the verifier's transformations. Keeping it read-only keeps it auditable.

Property	Check	Catches
Safety	Topology consistency	Edges reference nonexistent nodes; no path for transfers
Safety	Ref resolution	Dangling window reads, missing forward targets
Safety	Forwarding signatures	Arity mismatch, type mismatch, region provenance mismatch
Safety	Window separation	Reader and writer may execute concurrently
Consistency	Tensor shape propagation	Mismatched shapes in tensor graph DAG
Consistency	Region provenance	`buf<ram_0>` forwarded to a `gpu_0` tensor graph
Liveness	Buffer conservation	Buffer allocated but never freed or forwarded
Liveness	Tensor reachability	DAG node neither consumed nor named as output
Resource bound	Persistent memory bounded	Actor state exceeds node capacity
Resource bound	DAG finiteness	Tensor graph or pipeline contains a cycle

Conservation check per stage: build the control flow graph, walk every path tracking live Buffer resources. Every path must end with an empty live set. If any path ends with a live buffer, the verifier rejects with the specific path and buffer name.

Separation check: within a step, the data dependency chain ensures the window reader (tensor graph) completes before the writer (actor handler) fires. At pipeline_depth > 1, cross-step safety requires that step N's actor update completes before step N+1's reader begins — the actor serializes this.

Optimization (IR→IR rewrites)

Stage fusion (merge adjacent stages on same node), pipeline rebalancing, tensor graph rewriting (fuse ops, eliminate copies), communication optimization (overlap compute and transfer), parallelism mapping (data/tensor/pipeline parallel as topology + placement rewrites).

Trace — MNIST at L1 (abbreviated)

system single_gpu {
    node ssd_0  { kind: storage }
    node ram_0  { kind: memory, capacity: 32GB }
    node cpu_0  { kind: compute, isa: x86_64, cores: 8 }
    node gpu_0  { kind: compute, isa: cuda, vram: 24GB, sm: 84 }

    edges {
        ssd_0 -> ram_0  : bandwidth 2GB/s
        ram_0 <-> cpu_0 : bandwidth 50GB/s
        cpu_0 <-> gpu_0 : bandwidth 32GB/s
    }
}

actor model_state on gpu_0 {
    state {
        w : tensor(f32, [784, 256]), init: kaiming
        b : tensor(f32, [256]),      init: zeros
    }

    window weights : (w, b)
        readers(forward_backward)

    on GradUpdate(gw, gb) {
        let lr = 3e-4
        w = tensor_sub(w, tensor_scale(gw, lr))
        b = tensor_sub(b, tensor_scale(gb, lr))
    }
}

stage load_data on cpu_0 { ... }
stage transfer_to_gpu on cpu_0 { ... }
tensor_graph forward_backward on gpu_0 {
    reads: model_state.weights
    fn compute(x, y) -> (loss, gw, gb) { ... }
}
stage transfer_grads on cpu_0 { ... }

pipeline train { load_data -> transfer_to_gpu -> forward_backward }
pipeline grad_return { transfer_grads }

schedule {
    pipelines: [train, grad_return]
    actors: [model_state]
    pipeline_depth: 2
}

L1 → L0 Lowering

Not search — emission. The verified L1 IR is lowered into L0 through three compiler passes, then split into two code paths.

Pass 1: Memory Planning

Compiler-derived, not user-declared. Three strategies selected by lifetime analysis:

Strategy	Use	Lifetime
Persistent	Actor state (w, b)	Init → program end
Arena	Tensor intermediates	Graph start → graph end, bulk reset
Pool	Transfer staging buffers	alloc → free, freelist

Pass 2: Stream Inference

Each step's GPU work gets a stream. At pipeline_depth: N, N streams. Cross-stream dependencies become sync events.

stream_0: step N   → K0, K1, ..., sgd_kernel
stream_1: step N+1 → K0, K1, ..., sgd_kernel

sync: event recorded after sgd_kernel on stream_0
      waited before K0 on stream_1

Pass 3: Kernel Scheduling & Fusion

Tensor graph DAG nodes are grouped into kernels. Fusion rules: elementwise ops fuse freely; reduction forces a kernel boundary; different iteration spaces cannot fuse.

Dual Emission

The verified L1 IR splits into two code paths:

Path A — Control. Stages and actor handlers emit to Control IR (Machine IR). This is the CPU-side orchestration: data loading, transfers, message dispatch, pipeline coordination.

Path B — Compute. Tensor graphs emit to Compute IR (UOps). This is the accelerator-side math: matmuls, reductions, elementwise, fused kernels.

Both paths feed into the Phase 2 (concrete) verifier before codegen.

L0: Machine

Purpose

Fully explicit execution plan. Every buffer, every kernel, every stream, every byte. No decisions left. This is what actually runs.

Control IR

Ten operations over named memory regions. SSA registers. No flat address space — every load and store names its region, so the backend knows all aliasing without analysis.

load.{sz}  rgn[off]           read from named region
store.{sz} rgn[off], val      write to region (rw only)
hash val → reg                deterministic hash for map indexing
arith {op} a, b → reg         add, sub, mul, and, or, shift
cmp {op} a, b → reg           eq, neq, lt, gt → 1-bit result
branch reg → blk, blk         conditional jump
jump → blk                    unconditional jump
queue_push rgn, val            push descriptor to queue
queue_pop rgn → reg            pop descriptor from queue
terminate                      end of execution unit

Regions are named, sized, access-controlled memory. Not a flat address space — specific bounded things. This preserves aliasing knowledge all the way to codegen. A flat address space throws this away and forces the backend to re-derive it.

Why not target C? C implies abstractions we don't use: a call stack (we don't recurse), a general pointer model (we have named regions), function boundaries (we inline everything). The C compiler then has to re-discover structure we already know. It may fail and generate worse code. More importantly, C is a black box: we lose visibility into what actually executes.

Compute IR (UOps)

Atomic operations inside a kernel. Each is a typed node (op, dtype, src[], arg) forming a DAG rooted at STORE nodes.

Category	Ops
Memory	`LOAD` `STORE` `INDEX`
Arithmetic	`ADD` `MUL` `MULACC` `NEG` `RECIPROCAL` `MAX` `MOD`
Compare	`CMPLT` `CMPNE` `WHERE`
Transcendent	`EXP2` `LOG2` `SIN` `SQRT`
Control	`RANGE` `END` `IF` `ENDIF` `BARRIER`
Type	`CONST` `CAST` `BITCAST` `VECTORIZE` `GEP`
Special	`WMMA` `REDUCE` `CUSTOM`

~25 ops. Complete for any dense numeric kernel. CUSTOM covers sparse, scatter, and target-specific intrinsics.

IR

L0_IR = {
    memory_plan:   Map<BufferId, MemorySlot>
    kernel_plan:   [KernelDecl]
    stream_plan:   Map<StreamId, [KernelId]>
    sync_plan:     [SyncPoint]
    transfer_plan: [Transfer]
    init_plan:     [InitOp]
    control_blocks: [Block]              Machine IR blocks
}

KernelDecl = {
    id:         KernelId
    inputs:     [BufferId]
    outputs:    [BufferId]
    ops:        [UOp]                    the kernel body
    grid:       (x, y, z)
    block:      (x, y, z)
    shared_mem: bytes
}

MemorySlot = {
    pool:       PoolId                   which physical memory
    offset:     bytes
    size:       bytes
    lifetime:   (first_use, last_use)
}

Verification — Concrete (Phase 2)

After memory planning, stream inference, and kernel scheduling. Pure read-only checks on the concrete plan.

Property	Check	Catches
Safety	Kernel correctness	UOp sequences don't type-check, out-of-bounds access
Safety	Buffer lifetime safety	Overlapping writes to same memory slot
Safety	Stream hazard check	Shared mutable region + different streams, no sync
Liveness	Sync completeness	Cross-stream dependency missing a barrier
Resource bound	Memory capacity	Sum of live slots > pool capacity at any time t
Resource bound	Pool exhaustion	No headroom for transient allocations at pipeline depth

Optimization (IR→IR rewrites)

Closest to the metal. Most aggressive. Kernel fusion (merge adjacent kernels sharing buffers), memory packing (minimize peak by reordering lifetimes), launch config tuning (grid/block for occupancy), instruction selection (UOp → target ISA), register pressure management, prefetch insertion.

Codegen

L0 IR → target code. This is the only target-dependent phase in the entire compiler.

Control Path

Machine IR → target backend. The 10 ops translate mechanically.

Backend	Characteristics
x86-64	Each op → 1–3 instructions. ~5 live values, no spills. Regions → register pointers.
LLVM	Regions become pointer arguments with `!noalias` metadata. LLVM gets perfect aliasing.
eBPF	Machine IR's restrictions (no loops, bounded access, linear resources) already satisfy the eBPF verifier. Nearly 1:1.
FPGA	Each block → combinational pipeline stage. Regions → BRAM ports. `queue_push` → FIFO write-enable. `terminate` → valid signal.

Compute Path

UOps → target ISA. Three passes:

Instruction selection — maps UOps to target ISA. MULACC → fma.rn.f32 on PTX, vfmadd on x86.
Register allocation — handles spill/fill and manages pressure per-target. GPU has thousands of registers (occupancy-sensitive), CPU has 16 GPRs (spill-heavy).
ISA emission — produces final text or binary. Warp divergence on GPU means IF/ENDIF UOps have different cost profiles than on CPU. Vectorization width is target-dependent.

Bounded Complexity

Codegen is deferred complexity, not buried complexity. The contract is clear: L0 IR is target-independent. Codegen is the only target-dependent phase. The UOp set is small enough that adding a new backend means writing ~25 emission rules plus register allocation for that target. This is a bounded, mechanical task — not an open research problem. The Machine IR is similarly small: 10 ops, each mapping to a handful of target instructions.

Linking & Runtime

Binary Structure

One binary. CPU object + accelerator blobs + metadata.

.text     schedule_loop, stage_pipeline, actor_dispatch, platform_primitives
.rodata   kernel cubins, memory_layout_table, stream_descriptors, schedule_descriptor
.data     pool_metadata, arena_metadata
.bss      gpu_context, stream_handles, event_handles

Platform Primitives

Hand-written per platform. The generated code calls into these. The emitter produces control flow + kernels. The runtime provides the operations.

Primitive	Linux + CUDA
`region_alloc`	Pool: atomic pop. Arena: bump.
`region_free`	Pool: atomic push. Arena: no-op.
`dma_ssd_to_ram`	`io_uring` / mmap+prefault
`pcie_dma_h2d`	`cuMemcpyHtoDAsync`
`pcie_dma_d2h`	`cuMemcpyDtoHAsync`
`gpu_dispatch`	`cuLaunchKernel`
`gpu_sync`	`cuStreamSynchronize`
`gpu_event_*`	`cuEventRecord / cuStreamWaitEvent`
`queue_push/pop`	Ring buffer in shared memory

Machine IR and kernel descriptors are target-independent. Only backends and primitive implementations change per platform.

Runtime Error Policy

All correctness errors caught at compile time by the two-phase verifier. The binary assumes all static proofs hold. Hardware faults crash the process — outside scope of generated code.

Escape Hatches

At any layer, annotate with #[<target_layer>::<directive>]:

// At L3: force a method choice
model classify {
    ...
    #[l2::backward(evolution(pop: 50))]
}

// At L2: force a placement
infer: sequential [
    linear(784, 256),
    #[l1::on(gpu_1)]
    linear(256, 10)
]

// At L2: force a kernel
infer: sequential [
    linear(784, 256),
    #[l0::kernel("fused_gelu.ptx")]
    ...
]

The escape hatch must pass verification at its target layer. You can inline PTX, but it must have the right buffer types. The compiler checks the boundary. If it fails, the error points at the annotation — the user broke the contract.

An escape hatch is opaque to optimization at layers above its target. #[l0::kernel(...)] cannot be fused with adjacent ops at L1. It's a black box with a typed boundary. This is the price of escaping.

Search Architecture

Every lowering boundary uses the same pattern:

lower(source_ir, target_constraints) -> Result<target_ir, SearchFailure>

    1. enumerate(source_ir, target_grammar) -> [candidate]
    2. filter(candidates, verify_target)    -> [valid]
    3. score(valid, cost_model_target)      -> [(candidate, cost)]
    4. select(scored)                       -> target_ir | SearchFailure

SearchFailure =
    NoCandidates(reason)        constraints too tight
  | TooManyCandidates(count)    representation too loose
  | Timeout(budget_exhausted)   problem is genuinely hard

SearchFailure is a diagnostic, not an error. It tells you what to fix: tighten constraints, loosen them, or redesign the layer boundary.

Data Ingestion

Data flows from storage to device memory before any kernel touches it:

Storage → decode (CPU) → Host Memory → batch → Staging → DMA → Device

The contract boundaries are clean: L2 says what to sample (epoch shuffle, curriculum, etc.), L1 says where to stage it (which memory pool, which node), L0 says how bytes move (DMA ops, transfer plan). Format-specific decoders (JPEG, video, custom binary) are pluggable at the L1/L0 boundary — they're CUSTOM UOps or host-side init ops.

Open Questions

1. Recurrence and variable-length. Current stance: everything finite, until(pred) is spec error without a proven bound. But transformers process variable-length sequences. Is sequence(domain, max_len) at L3 enough? Or do we need a richer notion?

2. Multi-model composition. GAN = generator + discriminator. Distillation = teacher + student. RL = policy + value + environment. L3 currently has one model per spec. Do we want multiple models with relationships, or a separate composition layer?

3. Training loop structure. L3 says goal: minimize(loss). Real training has phases — pretrain, finetune, RLHF. Epochs, checkpointing, evaluation. Probably L2 as a schedule, but it needs design.

4. Cost model grounding. L2 cost model is heuristic. L1 uses hardware specs. Neither is calibrated. Do we want empirical calibration — run a few kernels, measure, update?

5. Incremental compilation. If you change one loss term at L3, do you re-search all of L2? Probably: hash each IR node, re-lower only the subgraph whose inputs changed.

6. The host language. Rust for the compiler (algebraic types = IR correctness for free). But the DSL parser, the REPL, the interactive experience — Python bindings? LSP?

What Is Resolved

Layer count and purpose (4 layers, clear separation of concerns)
L1 is the systems-level DSL: actors, stages, pipelines, windows, tensor graphs, topology
Dual emission from L1: stages/actors → Control IR, tensor graphs → Compute IR (UOps)
Two-phase verification: structural (pre-scheduling, at L1) and concrete (post-scheduling, at L0)
Verification at every layer, classified by four property kinds
Named memory regions in Control IR — aliasing known to codegen without analysis
Memory planning as a compiler pass (persistent, arena, pool), not user-declared
Stream inference from pipeline_depth + placement
Escape hatch semantics (typed, opaque, verified at target)
Codegen contract (target-independent L0 IR, target-dependent emission only)
Data ingestion contract (L2 what, L1 where, L0 how)
Search architecture (uniform enumerate → filter → score → select at every boundary)
Platform primitives as the narrow runtime interface
No autodiff at L1 — backward is explicit; autodiff is an L2 method expanded during lowering
Dependency-inferred scheduling — no user-specified phases

35 KiB Raw Permalink Blame History Unescape Escape

Compiler Spec: L3 → L0

Zen

Property Definitions

Verification Without Solvers

L3: Spec

Purpose

DSL Forms

Domain Types

Model Constraints

Loss Kinds

IR

Verification

Optimization

Trace — MNIST at L3

L3 → L2 Lowering

L2: Method

Purpose

DSL Forms

Sample Methods

Infer Methods (Architecture)

Layer Primitives

Backward Methods

Update Methods

IR

Verification

Optimization (IR→IR rewrites)

Trace — MNIST at L2

L2 → L1 Lowering

L1: Placement

Purpose

DSL Forms — Topology

DSL Forms — Data Sources

DSL Forms — Actors

DSL Forms — Stages

DSL Forms — Tensor Graphs

DSL Forms — Pipelines

DSL Forms — Schedule

IR

Verification — Structural (Phase 1)

Optimization (IR→IR rewrites)

Trace — MNIST at L1 (abbreviated)

L1 → L0 Lowering

Pass 1: Memory Planning

Pass 2: Stream Inference

Pass 3: Kernel Scheduling & Fusion

Dual Emission

L0: Machine

Purpose

Control IR

Compute IR (UOps)

IR

Verification — Concrete (Phase 2)

Optimization (IR→IR rewrites)

Codegen

Control Path

Compute Path

Bounded Complexity

Linking & Runtime

Binary Structure

Platform Primitives

Runtime Error Policy

Escape Hatches

Search Architecture

Data Ingestion

Open Questions

What Is Resolved

35 KiB

Raw Permalink Blame History