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:

Stack

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

let example () =
    let buffer : Ptr<byte, Stack, ReadWrite> = stackalloc 1024
    // buffer is valid until function returns
    use buffer

Properties:

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

Arena

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

Status (January 2026): Arena is implemented as a CCS (Clef Compiler Service) intrinsic type with compiler-provided operations.

Type Definition:

// Arena<[<Measure>] 'lifetime> - CCS intrinsic type
// Layout: NTUCompound(3) = { Base: nativeint, Capacity: int, Position: int }

Current Implementation (Level 3 - Explicit):

// Create arena from stack-allocated backing memory
let arenaMem = NativePtr.stackalloc<byte> 4096
let mutable arena = Arena.fromPointer (NativePtr.toNativeInt arenaMem) 4096

// Allocate from arena (note: byref parameter for mutation)
let buffer = Arena.alloc &arena 256  // Returns nativeint
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 0

Arena Operations (CCS Intrinsics):

Lifetime Parameter: The 'lifetime measure parameter enables future lifetime tracking. Currently documentation-level; compiler enforcement planned.

Three Levels of Control (Lifetime Inference Principle):

1. Level 3 (Explicit): Full control via Arena.fromPointer, Arena.alloc &arena (implemented)
2. Level 2 (Hints): arena { } computation expression (future)
3. Level 1 (Inferred): Escape analysis via inline expansion - see Inline Functions and Escape Analysis (implemented)

Properties:

• No individual deallocation
• O(1) bump allocation
• Cache-friendly locality
• Scope-bounded lifetime
• Backing memory can come from stack or heap

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

DEFERRED: Detailed lifetime verification rules will be specified in a future revision covering ownership and borrowing semantics.

Grammar

region-type :=
    Stack
    Arena
    Peripheral
    Sram
    Flash

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

See Also

• Access Kinds - Read/Write permissions
• Platform Bindings - Platform-specific memory access