Execution Model

Status: reference

This document defines Concrete’s execution model: how programs start, allocate, fail, and interact with the host environment. It covers the hosted/freestanding distinction, the runtime boundary, the memory/allocation strategy, target support policy, stdlib alignment, execution profiles, performance validation, verified FFI envelopes, and the concurrency direction.

For the value and ownership model, see VALUE_MODEL. For the safety model (capabilities, trusted, Unsafe), see SAFETY. For ABI and layout details, see ABI. For stdlib module inventory, see STDLIB.

Hosted vs Freestanding

Concrete currently targets a hosted environment only. All programs assume:

• a POSIX-like OS with process model, file descriptors, and virtual memory
• libc is available and linked (malloc, free, printf, read, write, etc.)
• 64-bit address space (pointer size = 8 bytes, hardcoded in Layout)
• main is the entry point, called by the OS/libc startup code

What “hosted” means concretely

The compiler generates a main function that calls the user’s main (renamed to user_main internally). The generated main:

1. Calls user_main
2. Optionally prints the return value (for scalar types: i32/i64 → printf "%lld", bool → "true"/"false")
3. Returns 0 to the OS

There is no Concrete runtime initialization. No global constructors, no GC setup, no thread-local storage initialization, no allocator setup. The program starts in main, calls libc functions directly, and exits when main returns.

What “freestanding” would mean (future)

A future freestanding mode would remove the assumption of libc and OS facilities. This is not implemented but the direction is documented here so the hosted boundary remains explicit.

Freestanding would mean:

• no libc-backed assumptions by default
• no ambient runtime (no implicit malloc/free)
• allocation only if explicitly provided
• explicit target contract for startup, failure, and memory
• stdlib limited to a core subset (Option, Result, math, ptr, slice, mem)

The hosted/freestanding split is a later milestone (see research/stdlib-runtime/no-std-freestanding.md). The current priority is making the hosted boundary explicit so the split is straightforward when needed.

Stdlib layer classification

The stdlib naturally divides into layers by host dependency:

Today these are all compiled together. The classification exists to guide future separation and to make host dependencies auditable now.

Runtime Boundary

What constitutes the “runtime”

Concrete does not have a runtime in the traditional sense (no GC, no green threads, no event loop). The runtime boundary is the set of external symbols and conventions that a compiled Concrete program depends on at link time.

Startup

1. OS/libc calls main(argc, argv) (Concrete ignores argc/argv today)
2. main calls user_main (the user’s fn main())
3. No global initialization, no module init functions, no static constructors

Shutdown

1. user_main returns
2. main optionally prints the return value
3. main returns 0
4. OS reclaims process resources

There is no cleanup hook, no atexit registration, no destructor ordering. Linear ownership and defer handle resource cleanup within function scope. When the process exits, the OS reclaims everything.

Failure

Concrete has no panic/unwind mechanism. Failure modes:

There is no structured panic. No stack unwinding. No catch mechanism. This is intentional — it keeps the execution model simple and compatible with freestanding targets in the future. Error handling is explicit through return types.

External symbol dependencies

Every compiled Concrete program links against these categories of external symbols:

Always required (emitted by the compiler):

Conditionally required (from user stdlib imports):

Test mode

In test mode (concrete file.con --test), the compiler generates a test runner main instead of the normal main wrapper. The test runner:

1. Calls each #[test] function in order
2. Prints PASS: <name> or FAIL: <name> for each
3. Returns 0 if all pass, 1 if any fail

Memory and Allocation Strategy

Current model: libc malloc

All heap allocation goes through libc malloc/realloc/free. There is no custom allocator, no arena, no bump allocator, no GC. The compiler emits direct calls to these functions in:

• String builtins (EmitBuiltins.lean): string_concat, string_slice, string_trim, int_to_string, float_to_string, bool_to_string all call malloc for new buffers. drop_string and string_concat call free.
• Vec builtins (EmitBuiltins.lean): vec_new_{size} calls malloc with initial capacity × element size. vec_push_{size} calls realloc when full (2× growth). vec_free calls free.
• User code via std.alloc: heap_new<T>(), grow<T>(), dealloc<T>() wrap malloc/realloc/free with trusted + Alloc capability.

Allocation is capability-tracked

The Alloc capability marks functions that allocate. This is enforced by CoreCheck — a function calling heap_new, Vec::new, or String::concat must declare with(Alloc) or be called by a function that does. This makes allocation visible in:

• --report caps: shows which functions require Alloc and why
• --report alloc: shows allocation/cleanup patterns and warns about functions that allocate without cleanup

Allocation failure

Abort on OOM. All allocation paths check for null returns from malloc/realloc and abort the process immediately if allocation fails. This matches Rust’s default allocator behavior and is appropriate for hosted programs.

The abort-on-OOM guarantee covers two layers:

1. Compiler builtins (EmitBuiltins.lean): All 11 malloc/realloc call sites in string and vec builtins pipe through __concrete_check_oom, a compiler-emitted helper that null-checks and calls abort().
2. Stdlib wrappers (std/src/alloc.con): heap_new<T>() and grow<T>() null-check their malloc/realloc results and call abort() on failure.

This means any allocation reachable through the standard API is OOM-safe. Direct extern fn malloc calls from user trusted code are not checked — the user is responsible for null-checking in that case.

Future directions beyond abort-on-OOM:

1. Propagate OOM as error: builtins return Result<T, AllocError>. Correct but invasive — changes the signature of every allocating operation.
2. Allocator trait: user-provided allocator with configurable failure behavior. Most flexible but highest complexity.

Deallocation model

Concrete uses linear ownership + defer for deterministic deallocation:

• Linear types: structs and enums must be consumed exactly once. The compiler enforces this at check time.
• defer: schedules cleanup at scope exit. The standard pattern is defer vec.free(); or defer string.drop();.
• Destroy trait: types implementing Destroy get their destroy() method called when they go out of scope (not yet automatic — users must call it or use defer).

There is no automatic destructor insertion (RAII). Resource cleanup is explicit. This is intentional — it keeps the execution model transparent and avoids hidden control flow.

Stack allocation

Local variables and temporaries are stack-allocated via LLVM alloca. The compiler uses entry-block allocas for:

• aggregate variables that are modified across control flow (promoted from phi nodes to stable storage)
• temporary structs for pass-by-pointer ABI
• local variables that need an address (e.g., &mut borrows)

Stack size is not bounded or checked by the compiler. Stack overflow is caught by the OS guard page.

Memory layout

All memory layout decisions are centralized in Concrete/Layout.lean:

• Type sizes and alignments follow platform conventions (i8=1, i16=2, i32=4, i64=8, f64=8, ptr=8, bool=1)
• Structs use C-like field layout with natural alignment padding (unless #[repr(packed)])
• Enums use tag + padded payload (i32 tag, payload aligned to max variant alignment)
• #[repr(C)] provides C-compatible layout for FFI structs
• #[repr(align(N))] sets minimum alignment

See ABI for full details.

Future directions

FFI and Runtime Ownership Boundary

This section documents how ownership, capabilities, and resource tracking interact with the FFI boundary. For FFI type rules and safety checks, see FFI. For ABI and calling convention details, see ABI.

Capability model at the FFI boundary

Extern functions participate in the capability system:

The standard pattern is a three-layer stack:

1. libc declaration (std.libc): raw extern fn malloc(size: u64) -> *mut u8
2. trusted wrapper (std.alloc): trusted fn heap_new<T>() with(Alloc, Unsafe) -> *mut T — calls malloc, null-checks, casts the pointer. The trusted marker means raw pointer operations inside are audited, but Unsafe is still visible to callers.
3. user code: calls heap_new<T>() with both Alloc and Unsafe capabilities

Today trusted allows raw pointer operations without additional checks inside the function body, but it does not hide capabilities from callers. The declared with(...) set is the caller-visible contract. A future capability-hiding mechanism (where a trusted wrapper could absorb Unsafe and expose only Alloc) is not yet implemented.

Ownership across FFI calls

The linearity checker tracks ownership at the Concrete level:

• By-value arguments to extern fn consume the variable. If you pass a linear type by value, it is marked consumed. The compiler assumes the foreign function took ownership.
• By-reference arguments (&T, &mut T) borrow without consuming. The original variable remains usable after the call.
• Raw pointers (*mut T, *const T) are Copy. No ownership tracking. The compiler cannot see what C code does with a pointer.

What the compiler cannot track

Once data crosses the FFI boundary, the compiler has no visibility:

These gaps are intentional — they match the cost model of C FFI in Rust, Zig, and other systems languages. The mitigation is:

1. trusted fn wrappers that present a safe interface
2. Capability tracking that makes FFI usage visible in reports
3. --report unsafe that shows which trusted functions wrap which extern calls

What is NOT allowed at the FFI boundary

The compiler enforces that only FFI-safe types appear in extern fn signatures:

• Allowed: integers, floats, bool, char, (), raw pointers (*mut T, *const T), #[repr(C)] structs
• Rejected at compile time: String, Vec<T>, HashMap<K,V>, non-repr(C) structs, enums, arrays, references

This prevents accidentally passing a managed Concrete type to C code that doesn’t understand its layout.

Calling convention

#[repr(C)] structs in extern fn signatures are passed by value following the platform C ABI. LLVM handles the register/stack lowering for the target architecture. Internal Concrete function calls use pointer-based passing for all aggregates.

For full calling convention details, see ABI.

Known gaps and future directions

Target and Platform Support Policy

Concrete currently supports a single target profile:

Support tiers

A target is not “supported” just because LLVM can emit code for it. Supported means:

• layout assumptions are documented and tested
• ABI behavior matches documented conventions
• the runtime boundary (startup, allocation, failure) works as specified
• core stdlib modules compile and pass tests
• reports remain truthful

What is target-dependent

What is not yet validated empirically

• Cross-compilation (building for a different target triple than the host)
• 32-bit targets (pointer size is hardcoded to 8)
• Non-POSIX hosted environments (Windows, WASI)
• Struct layout agreement between Concrete and C compilers on Tier 2/Experimental targets

Future directions

Stdlib and the Execution Model

The stdlib is classified into three layers by host dependency (see Hosted vs Freestanding above). This section documents how stdlib modules align with the execution model and where the boundaries are.

Module-to-layer mapping

What the execution model constrains in stdlib

1. No hidden allocation. Every stdlib function that allocates must declare with(Alloc). The --report alloc output makes this auditable.
2. No hidden host access. Hosted modules require their respective capability (Network, Process, Random, Console, etc.) or Unsafe for direct libc calls. A function that only does computation cannot accidentally pull in network or filesystem dependencies.
3. Deterministic cleanup. All stdlib types that own resources provide explicit free()/drop()/close() methods. There is no implicit destructor insertion.
4. Abort-on-OOM. All allocation through std.alloc and compiler builtins aborts on null. Stdlib types built on Vec/String inherit this guarantee.

What is not yet enforced

• The layer classification is documentary, not compiler-enforced. A core module could import a hosted module without a compiler error (the capability system would catch the effect mismatch, but there’s no “this module is core-only” annotation).
• test module output goes through compiler-inserted printf calls, technically making it hosted, but tests are not production code.

Execution Profiles

Concrete does not yet implement execution profiles, but the direction is documented here so the constraints inform Phase F and G work.

What execution profiles would provide

An execution profile is a set of compiler-enforced restrictions on what a program (or module/package) may do at runtime. The goal is to support high-integrity use cases without making all Concrete code live under maximum restriction.

Planned profiles

How profiles would work

1. Declaration: a module or package declares its profile (e.g., #[profile(no_alloc)])
2. Enforcement: the compiler rejects code that violates the profile’s restrictions during capability checking
3. Reporting: --report profile shows which functions/modules satisfy which profiles and where violations occur
4. Composability: a high_integrity module can call no_alloc and no_unsafe code. A default module can call any profile.

What makes this feasible

Concrete’s existing capability system already tracks Alloc, Unsafe, Network, Process, Random, Console, etc. Profiles are essentially named capability budgets — a no_alloc profile is “reject any function that requires Alloc.” The enforcement mechanism already exists; profiles would add named sets and module-level declarations.

Relationship to proofs

The high_integrity profile would closely align with ProofCore eligibility. Code that satisfies the high-integrity profile is more likely to be provable because it avoids Unsafe, bounds allocation, and has no FFI dependencies. The profile and proof eligibility checks could share the same underlying filter.

Performance Validation Direction

Concrete does not yet have performance benchmarks or regression tracking. This section documents the intended approach so it can be implemented incrementally.

Principles

1. Representative workloads, not microbenchmarks. Performance should be measured on programs that resemble real use, not isolated operations. The integration test corpus (12 programs) is a starting point.
2. Compilation time matters. The compiler itself is a performance-sensitive artifact. lake build time and per-file compilation time should be tracked.
3. Runtime performance is secondary to correctness. Concrete delegates optimization to LLVM (-O2). The compiler’s job is to emit clean, correct LLVM IR — not to implement its own optimization passes.
4. Observability over cleverness. Debug info quality, stack trace usefulness, and report truthfulness should not be sacrificed for performance. Optimization policy should explicitly account for these.

What should be measured

What counts as a regression

• Test suite time increasing >20% without new tests added
• Compiler build time increasing >30% without new passes added
• Any integration program becoming >2x slower at -O2 without code changes

What is explicitly out of scope

• Custom optimization passes in the Concrete compiler (rely on LLVM)
• Target-specific peephole optimizations
• Benchmark suites that don’t correspond to real usage patterns
• Performance comparisons with other languages (premature at this stage)

Future directions

Verified FFI Envelopes and Structural Boundedness

This section documents the direction for making FFI boundaries and resource usage mechanically verifiable, beyond the current trust-based model.

Verified FFI envelopes

Today, extern fn contracts are trust-based: the programmer declares the signature, and the compiler trusts it. A verified FFI envelope would add mechanical checking:

How envelopes would work

1. Declaration: an extern fn can optionally have an envelope annotation describing pre/postconditions
2. Verification source: envelopes could be checked against C header files, manual annotations, or generated bindings
3. Compiler integration: the compiler would reject calls that violate envelope constraints (e.g., passing a potentially-null pointer to an envelope that requires non-null)
4. Report integration: --report ffi would show which extern functions have verified envelopes and which are trust-only

Structural boundedness reporting

Structural boundedness means the compiler can statically determine resource usage bounds for a function or module:

What exists today

• Allocation tracking: --report alloc shows which functions allocate and where
• Capability tracking: --report caps shows full capability requirements
• Unsafe tracking: --report unsafe shows trusted/extern boundaries
• Proof eligibility: ProofCore extraction identifies the pure, provable fragment

What is needed

• FFI envelope syntax and checker (Phase F/G)
• Static allocation size analysis for bounded-allocation profiles (Phase F)
• Stack depth analysis for stack-bounded guarantees (Phase G)
• --report boundedness that summarizes which functions satisfy which structural bounds (Phase F)

Concurrency and Execution Model

Concrete does not yet implement concurrency. This section documents the intended direction so that runtime, capability, and ownership decisions made now remain compatible with the concurrency model.

Design principles

1. Explicit over ambient. Thread creation, blocking, and synchronization should require explicit capabilities, not be available by default.
2. Structured over detached. Concurrent work should belong to explicit scopes with defined lifetimes. Fire-and-forget spawning should be rare and marked.
3. Threads first, async later. OS threads are the base primitive. Evented I/O and executor-driven async are specialized later additions, not the default.
4. Ownership across threads. Values moved into spawned threads are consumed (linear move). Shared mutable state requires explicit synchronization types.
5. Capability-gated. Spawning threads requires a Spawn (or Concurrency) capability. Blocking requires Block. These are separate from Network/Process/Random.

First concurrency model (designed in Phase E, implemented in Phase J)

The initial model targets hosted environments only:

What the capability system provides

fn process_batch(data: Vec<Work>) with(Spawn, Block, Alloc) -> Vec<Result> {
    let (tx, rx) = channel::new::<Result>(data.len());
    for item in data {
        thread::spawn(fn(item: Work, tx: Sender<Result>) with(Alloc) {
            tx.send(do_work(item));
        }, item, tx.clone());
    }
    return rx.collect();
}

The signature makes visible: this function spawns threads, may block, and allocates. --report caps would show exactly which functions in a module require Spawn or Block.

Staging

What concurrency does NOT change

• The runtime boundary remains minimal (no GC, no green threads, no event loop in the default runtime)
• Linear ownership semantics are unchanged — spawn consumes the closure’s captured values
• Allocation model is unchanged — threads use the same libc malloc with abort-on-OOM
• Failure model is unchanged — no panic/unwind, threads that fail return errors via channels or join

What to avoid

• Rust-style async/await as a first-class language feature before the thread model is stable
• Runtime fragmentation (multiple incompatible executor ecosystems)
• Hidden executors or schedulers in stdlib
• Function coloring that forces non-concurrent code into async signatures
• Ambient concurrency — spawning should be as visible as allocation

See research/stdlib-runtime/concurrency.md for the full near-term design and research/stdlib-runtime/long-term-concurrency.md for the long-term layered model.

Summary