Memory Model & Concurrency

1. Abstract

This RFC defines Aura’s memory and concurrency model: tracing GC, reference vs value semantics, lightweight tasks, bounded channels, async/await, shared-memory synchronization, happens-before rules, and the policy that data races are bugs—detected in development, not licensed as silent undefined behavior. The current runtime adds an opt-in POSIX M:N worker pool and reactor around the cooperative task model.

Runtime implementation details (scheduler, collector algorithm) are expanded in RFC-006; this document is the language-level contract.

Toolchain today (2026-08-02): class instances are GC heap references and struct values remain by-value. The runtime has registered-root stop-the-world mark/sweep coordinated with concurrent worker activity, an opt-in POSIX M:N worker pool, a POSIX poll reactor, bounded channels/select, task scopes, blocking jobs, and task-safe lazy cells. C20c–e add MVP shared pointer boxes for mutable class, Array, and nested Fun captures; C20g adds read-only collection snapshots. C21b–e add sema-checked scoped refs and borrow-safe Array field returns. C22a–i land async/task syntax and barriers; C22j–k task frames/executor; C22n–o bounded channels and typed payloads. General CFG now also supports awaited return expressions with typed frame slots; scheduler-owned task payload transfer and nested spawn pollers are covered, while richer open-generic captures, non-POSIX backends, and a concurrent tracing collector remain open.

2. Motivation

The current scheduler boundary also supports explicit reference wrappers for Task/TaskHandle frame payloads and Channel payloads. These references are released independently from lexical handles; only richer open-generic captures, non-POSIX backends, and a concurrent tracing collector remain open in this area.

2.1 Problem statement

Service authors need cheap concurrency and safe memory without Rust-style ownership. Classic JVM models provide GC and threads but historically weak tools for structured concurrency; Go provides tasks and channels with a simple model. Aura combines GC + tasks with a modern async surface and explicit race policy.

2.2 Why now

Compiler lowering, stdlib sync primitives, and diagnostics all depend on a single concurrency story.

2.3 Success metrics

3. Goals

• Clear concurrency story for backends and CLIs.
• Safe-by-default memory via GC (no UAF in safe code).
• Async I/O first-class with structured patterns.
• Shared state possible with explicit locks/atomics/channels.
• Portable memory ordering story for atomics.

4. Non-goals

• Full CUDA/GPU model in v1.
• Distributed actor cluster protocol (library later).
• Rust-style ownership as the primary model; C21 may add only a scoped, non-owning ref capability.
• Hard real-time GC guarantees in v1.

5. Prior art & alternatives

6. Design

6.1 Overview

┌─────────────────────────────────────────────┐
│  Process                                    │
│  ┌─────────────┐    ┌─────────────────────┐ │
│  │ GC Heap     │    │ Task scheduler (M:N)│ │
│  │  objects    │◄──►│  tasks / async      │ │
│  │  structs*   │    │  I/O reactor        │ │
│  └─────────────┘    └─────────────────────┘ │
│         ▲                    ▲              │
│         │    channels/locks  │              │
└─────────┴────────────────────┴──────────────┘
* structs may live in heap boxes or stack/registers when escaped analysis allows

• Memory: tracing GC for class instances and boxed values.
• C22 concurrency: many cooperative tasks multiplexed by one deterministic ready queue on one OS thread. A task yields only at an await/runtime suspension point; no OS thread is created by spawn.
• Communication: prefer channels & isolation; locks for shared mutability.

The C22 MVP excludes OS-thread scheduling, work stealing, a blocking-I/O reactor, and concurrent GC. Those facilities may be added by a later RFC or milestone without changing the source vocabulary below. Release packaging, signing, notarization, and publication are also outside C22.

The landed implementation lowers general async branch/loop/repeated-await CFGs and reuses that typed frame contract for inferred immutable and mutable captures spawn bodies. The runtime also exposes a versioned AuraTypeErasedOps/AuraTypeErasedValue clone/drop/mark contract for values that must cross an open generic or plugin boundary; concrete compiler monomorphs continue to use typed layouts. Typed channel operations, failure propagation, cancellation, and frame GC hooks are part of the shipped contract rather than fallback behavior. Capture discovery is lexical: bindings introduced inside a spawn body, loop, or match/catch shadow an outer name and never become accidental frame fields; lambda bodies retain their separate closure-environment lowering.

6.2 Memory management strategy

Decision: Tracing GC. The current phase is precise stop-the-world mark-sweep with executor safepoints; a concurrent tracing collector remains a later phase.

Safe Aura guarantees:

• No use-after-free / double-free for GC-managed objects.
• Finalizers: discouraged; prefer explicit Close/using patterns (stdlib).

6.2.1 C21 ref MVP boundary

The selected C21 direction is a checked, non-owning borrow for short-lived access to an existing owner. It does not change GC ownership: the owner keeps the object or Array buffer alive, while sema rejects a ref T that would outlive the owner's lexical scope. The first consumers are safe Array field returns and read-only collection views.

The MVP has no mutable borrow, heap-stored reference, nullable/nested ref, closure/task escape, pinning, or concurrent sharing. Codegen may represent a valid borrow as a temporary pointer/view; no new runtime retain/release ABI is required. Mutable Array lambda captures are a separate owned shared-cell contract: the outer binding and each closure retain the cell, and the Array payload is released after the last cell owner. Async/tasks were outside the C21 implementation track; C22 now adds explicit single-threaded lifetime barriers without changing this ownership ABI.

6.2.2 C22 async borrow barriers

C22 removes that deferral at the contract level while preserving the same non-owning lifetime model: ref T is synchronous-only. The sema must reject a borrow at await, a spawned-task capture, channel send, channel receive, or task-owned storage. A task frame, Task<T>/TaskHandle<T> result, closure environment, and queued channel payload are all task-owned storage for this rule. receive may produce an owned T; only a borrow retained across that operation is invalid.

All such errors use E-BORROW-ASYNC-ESCAPE with the operation-specific message borrowed value cannot cross {operation} boundary, a primary span on the borrowed expression, a secondary span on the boundary token, and the note use an owned value (for example, clone()) before this boundary. This wording is shared with RFC-002 so pretty and structured diagnostics identify the same operation and source locations.

6.3 Value semantics & references

• Interior mutability: fields of classes mutable per var/val; no separate Cell required for GC objects.
• Pinning: needed at FFI boundaries for buffers (RFC-006).

6.4 Threading model

• Logical concurrency unit: task, represented by a stackless frame and scheduled cooperatively.
• MVP execution: one runtime executor, one ready queue, FIFO enqueue order, and no user-visible parallelism.
• OS threads: unavailable to C22 spawn; worker pools, spawnBlocking, work stealing, and scheduler placement are deferred to RFC-006 follow-up work.

6.5 Async model

The source forms are defined by RFC-001 §6.3.1. In this RFC, an async fun returns a task-producing computation, spawn { ... } schedules a new task and returns its handle, join(handle) observes completion, and cancel(handle) requests cooperative cancellation. These names are reserved and are not interchangeable with OS-thread APIs.

async fun loadUser(id: Id): User { ... }

fun main() {
  spawn { backgroundSync() }

  val user = await loadUser(42)
  // structured: prefer scopes
  taskScope {
    val a = async { fetchA() }
    val b = async { fetchB() }
    use(await a, await b)
  }
}

6.5.1 Task and handle contract

For C22, calling an async fun creates a lazy Task<T> computation. spawn registers that computation with the single-threaded executor and returns a GC-managed TaskHandle<T>. A handle may be retained, passed, and joined more than once; every join after completion observes the cached outcome.

General async CFG lowering treats return await expression as a suspension edge rather than re-evaluating the expression after resume. The awaited value is stored in a typed frame slot, and the normal cancellation, failure propagation, and aggregate drop hooks apply before the terminal Task<T> result is published. If the operand contains another async operation, the compiler lifts the innermost await into the same continuation graph (for example return await await makeTask()), preserving each child handle's ownership and avoiding duplicate evaluation after resume.

Expression-form if values use the same rule: when either branch awaits, the compiler emits a branch state and assigns the selected value into the typed continuation slot. The branch is selected exactly once, and the unselected child task is never created, so suspension cannot re-evaluate the expression.

Task<T> and TaskHandle<T> are distinct: the former is a computation, the latter is the scheduled identity used by join and cancel. C22 has no preemptive cancellation, OS-thread affinity, or implicit auto-restart.

The alpha std surface reserves std.task.taskScope(() -> Unit), std.task.Select<T>, std.task.select<T>(), and std.task.spawnBlocking<T>(() -> T) as placeholders for structured concurrency, channel selection, and worker-pool execution. They fail explicitly until async closure lowering, child supervision, readiness fairness, and worker runtime support are available; the conceptual block form remains the RFC language target.

6.6 Shared-state concurrency

Primitives (stdlib):

Default style: share-memory-by-communicating when practical; locks when needed.

There is no borrow-based Send/Sync enforcement. Documentation and optional attributes may mark thread-hostile types. Race detector covers misuse.

The alpha Mutex and RwLock are non-generic state gates; protected data is owned by the caller and is not stored in the lock. A future generic guard API must first define guard lifetime, async cancellation, and ownership behavior.

6.6.1 Bounded channel contract (C22)

Channel<T>(capacity) is a single-producer/multi-producer-safe-by-contract message queue for the MVP executor, with capacity strictly greater than zero. The queue is FIFO for successfully sent values. send(value) suspends the current task while the queue is full; receive() suspends while it is empty. Waiting senders and receivers are resumed in FIFO wait-queue order.

close() is idempotent. After close, no new value can be sent. Receivers drain already queued values in FIFO order and then receive Closed; a sender that observes a closed channel receives Closed and its payload is destroyed or released according to normal GC/value rules. Cancellation removes a waiting operation without reordering other waiters. A channel owns or retains queued payloads until delivery, drain, or close cleanup; a C21 ref T is never a legal payload across this boundary.

6.6.2 Alpha placeholder contracts

std.task.select<T>() constructs a selector and Select<T>.add(Channel<T>) -> Select<T> registers a channel. The eventual await selector.next() -> T? operation returns one ready value or the closed sentinel after all registered channels close. The alpha source declarations throw placeholders; readiness fairness, registration mutation, and a richer closed-channel outcome remain runtime work.

std.sync.lazy<T>(() -> T) -> Lazy<T> reserves exactly-once initialization; Lazy<T>.get() -> T and isInitialized() -> Bool must be safe across the future worker scheduler. The alpha calls throw placeholders until task-safe retention and initialization races are defined.

std.task.spawnBlocking<T>(() -> T) -> TaskHandle<T> reserves execution of a blocking closure on a worker pool. It must not run blocking work on the cooperative executor, and cancellation must define whether queued/running work is abandoned or joined. The alpha call throws a placeholder.

6.7 Memory consistency model

• Sequentially consistent atomics as default API for simplicity.
• Acquire/release variants available for experts.
• Happens-before edges: unlock→lock same mutex; channel send→receive; task spawn→start; async resume edges; volatile/atomic ops per their orderings.
• Data race definition: concurrent conflicting accesses to the same non-atomic location where at least one is a write, without happens-before.

Data race policy:

Aura does not promise that racy programs have sequential semantics; it promises races are not a free optimization license to delete safety checks elsewhere, and tools help find them.

6.8 FFI & foreign memory

• Foreign memory is not GC-managed unless copied/bridged.
• Buffers passed to C must remain valid for the call (pin / explicit lifetime scope).
• Allocator hooks for custom native buffers → RFC-006.
• unsafe required for raw pointer dereference.

6.9 Examples

fun worker(c: Channel<Int>) {
  for (n in c) {
    println(n)
  }
}

fun main() {
  val c = Channel<Int>()
  spawn { worker(c) }
  c.send(1)
  c.send(2)
  c.close()
}

async fun handle(conn: Conn) {
  val req = await conn.readRequest()
  val res = await route(req)
  await conn.writeResponse(res)
}

6.10 Error model / edge cases

6.11 Compatibility & migration

• Scheduler tuning flags may change performance but not language semantics without edition.
• Strengthening race detection must not break race-free programs.

7. Open questions

8. Rationale & trade-offs

Go-like tasks + GC maximize concurrency productivity for servers. Stackless async integrates cleanly with LLVM and avoids huge per-task stacks. Rejecting ownership keeps the type system focused on nullability and classes. Rejecting silent UB for races aligns with “safety as a product value” while remaining implementable without a borrow checker. Cost: GC pauses and the need for discipline (and a detector) around shared mutation.

9. Unresolved / future work

• Formal memory model appendix (axiomatic)
• Profiler/tracing integration
• Optional ownership annotations for buffers
• Actor library design

10. Security & safety considerations

• UAF/double-free in safe code: mitigated by GC.
• Races as security bugs (TOCTOU, torn reads of pointers—mitigated if references are atomic-sized and GC-safe; still logical bugs).
• FFI is the primary memory-safety escape hatch.
• Side channels (Spectre) out of scope unless noted.

11. Implementation plan (optional)

12. References

• Go memory model; Go race detector
• Java Memory Model (happens-before concepts)
• Kotlin coroutines / structured concurrency (Trio, Swift TaskGroup inspiration)
• RFC-000, RFC-001, RFC-006

Changelog