Memory Regions

Memory region types define where memory lives and how it behaves. They are intrinsic to Clef and guide code generation throughout the compilation pipeline.

Overview

Clef extends the type system with memory region information. Every pointer type carries region semantics that determine:

• Allocation strategy
• Access patterns (volatile, cached)
• Lifetime constraints
• Code generation decisions

Region Types

The following memory regions are defined:

Sram and Flash are also the static storage of the lifetime lattice: a value whose lifetime is the whole program (constructed once, held to program end, never freed) is placed in Sram when mutable or Flash when immutable, as a program-lifetime global rather than a heap allocation. A fixed-address Peripheral register is already a program-lifetime global of this kind; a program-lifetime closure, list, or record is the same, and lives in the same static storage. This is what lets a target without a heap still hold a value that outlives its constructing scope.

The lattice extends one rung past the process on targets that claim the Freestanding Substrate profile: Modular Blob Storage persists values that outlive a program run, and Namespace Storage layers names and history above it. Both are placed through the regions of this chapter — sealed records in non-volatile storage, working sets in bounded RAM — and both carry their durability as a coeffect committed at target binding.

Stack

Stack-allocated values have automatic lifetime bounded by their lexical scope.

let example () =
    // Fixed-size stack array; storage is allocated in the Stack region
    let buffer : array<byte, 1024, Stack> = [| 0uy; ... |]
    // A region-typed handle to the buffer's storage, valid until the function returns
    let handle : Ptr<byte, Stack, ReadWrite> = Ptr.ofArray buffer
    use handle

Properties:

• Thread-local storage
• Automatic cleanup at scope exit
• Size limits enforced by platform

Arena

Arena-allocated values are bulk-allocated and freed together.

Arena is a CCS (Clef Compiler Service) intrinsic type with compiler-provided operations.

Schematic Type and Layout:

// Arena<'lifetime> - CCS intrinsic with an inferred lifetime identity
// Layout: NTUCompound(3) = { Base: index, Capacity: index, Position: index }
//   Base and Capacity are the arena's buffer as a memref<?xi8> view (base index into the declared
//   space, extent); Position is the bump cursor. No field is an address.
 

In this section, 'lifetime denotes the arena’s inferred lifetime identity in the coeffect domain. The operation signatures use this schematic notation without declaring source lifetime-parameter syntax. Lifetime orderings SHALL be established by the lifetime constraints, independently of physical units of measure. Every allocation and use SHALL retain its relationship to the actual backing region and its admitted lifetime.

Explicit Allocation:

// Create arena from a bounded stack array as backing memory
let arenaMem : array<byte, 4096, Stack> = [| 0uy; ... |]
let mutable arena = Arena.fromArray arenaMem  // capacity taken from the array bound

// Allocate from arena (note: byref parameter for mutation)
let buffer = Arena.alloc &arena 256  // Returns a Ptr<byte, Arena, ReadWrite> handle
let aligned = Arena.allocAligned &arena 64 16  // 64 bytes, 16-byte aligned

// Query and reset
let remaining = Arena.remaining arena
Arena.reset &arena  // Position back to the arena's floor (0, or the sentinel slot; see Floor below)
 

Arena Operations (CCS Intrinsics):

Allocation can be explicit through Arena.fromArray and Arena.alloc &arena, or inferred through escape analysis; see Inline Functions and Escape Analysis.

Properties:

• No individual deallocation
• O(1) bump allocation
• Cache-friendly locality
• Lifetime bounded by the admitted backing region and allocation/use obligations
• Backing memory comes from the stack, from static storage (Sram/Flash), or, where the target has one, from the heap. A target without a heap backs arenas with stack or static storage only.

The { Base, Capacity, Position } layout states the allocation discipline as checkable facts: every allocation advances Position by the requested (aligned) size, and Position never exceeds Capacity. An implementation’s allocation emission is subject to the preservation and diagnostic obligations over exactly these facts.

Floor. An arena that hosts nodes of a collection type (List Operations §5.2, Map Representation §2.2, Set Representation §2.2) carries the sentinel of that type at offset 0, copied from the type’s program-lifetime sentinel image when the arena is created. The arena’s floor is the size of that slot, taken as the largest sentinel slot among the node types the arena hosts; every sentinel image is all-zero (tag Empty is case 0, height is 0, links are 0, payload slots are zero), so one slot at offset 0 serves every hosted type. Position begins at the floor, alloc never returns an index below it, and reset returns Position to the floor, never to 0. These are literal facts of the arena’s saturated layout, and they are what the collection chapters’ VC-RO obligations rest on: every store into a node lies at or above the floor by construction, and no runtime index value need be reasoned about. An arena that hosts no such type has floor 0.

Peripheral

Peripheral regions represent memory-mapped I/O with volatile semantics.

let gpioReg : Ptr<uint32, Peripheral, ReadWrite> = Ptr.ofAddress 0x48000000UL

Properties:

• Volatile loads and stores
• No reordering by compiler or CPU
• Memory barriers as required
• Not cacheable

Sram

General-purpose RAM with standard memory semantics.

Properties:

• Cacheable
• Standard load/store semantics
• May be reordered by optimizer

Flash

Read-only program memory, typically for embedded systems.

let lookupTable : Ptr<int, Flash, ReadOnly> = ...

Properties:

• Read-only access enforced
• Link-time placement
• Cacheable

Region-Typed Pointers

Pointers carry region and access information in their type:

type Ptr<'T, 'Region, 'Access>

Examples:

Ptr<uint32, Peripheral, ReadWrite>  // GPIO register
Ptr<byte, Flash, ReadOnly>          // Constant data
Ptr<int, Stack, ReadWrite>          // Stack buffer
Ptr<float, Arena, ReadWrite>        // Arena-allocated array
 

Compile-Time Enforcement

Region mismatches are type errors:

// ERROR: Cannot assign Peripheral pointer to Stack pointer
let wrong : Ptr<int, Stack, ReadWrite> = peripheralPtr

Code Generation Effects

Lifetime Constraints

Lifetime verification in Clef is coeffect discipline carried on the Program Semantic Graph, with no ownership or borrowing annotations in the source language. Every value is classified against the four-point lifetime lattice by escape analysis (Closure Representation §3.3), placement follows the classification, a classification with no home on the selected target is diagnosed at compile time, and the classification is subject to the preservation and introduction obligations of Conformance §6.

A region SHALL outlive every value placed in it, and every use of a value SHALL fall within its region’s extent. These lifetime orderings are discharged as proof obligations carried on the PSG with the escape coeffect (Program Semantic Graph §14.3).

Target Reachability

The region types of this chapter name storage a target provides, and the platform descriptor lists the regions each target has (Platform Bindings). A construct whose region the selected target does not provide SHALL be diagnosed at compile time when compiled for that target; reachability is carried as a lattice-family coeffect alongside escape classification (Grade Discipline §4.1).

On the JSIR pathway, no region of this chapter exists: the host garbage collector owns placement, every lifetime class of the lifetime lattice has a home, and Ptr, Arena, Mmio, and every region-typed construct SHALL be diagnosed as unavailable for the target (the CCS8030 pattern of Platform Bindings). The lifetime lattice itself still classifies every value at design time on that pathway; only the storage classes of this chapter are absent.

Grammar

region-type :=
    Stack
    Arena
    Peripheral
    Sram
    Flash

region-typed-ptr := Ptr < type , region-type , access-kind >