nocturn9x/peon-rewrite
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

docs: define memory and threading model

Browse Source
This commit is contained in:
Mattia Giambirtone
2026-07-31 19:07:03 +02:00
parent d29afd5884
commit 9c176be48e
2 changed files with 379 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
docs/manual/memory-model.md
View File

@@ -2,6 +2,9 @@
[Back to Manual](index.md)
For the proposed long-term ownership and OS-thread semantics, including freely aliasable
`mut lent` borrows, see [Memory Model and Threading Design](../memory-model-and-threading-design.md).
Peon manages heap-allocated values using **generational references** -- a scheme that
provides memory safety without a garbage collector and without the full complexity of
Rust's borrow checker.

376
docs/memory-model-and-threading-design.md Normal file
View File

@@ -0,0 +1,376 @@
# Memory Model and Threading Design
Status: proposed design direction.
This document defines the intended relationship between ownership, freely aliasable
borrows, deterministic destruction, and OS-thread concurrency in Peon. It complements
the user-facing [memory model](manual/memory-model.md) and the existing
[structured concurrency plan](structured-concurrency-plan.md).
## Goals
Peon's memory model should provide:
- no tracing garbage collector by default
- deterministic destruction of owned values
- exactly one owning `ref T` handle for each managed allocation
- lightweight non-owning borrows without Rust-style alias exclusivity
- any number of `mut lent T` aliases in sequential code
- scoped `mut lent T` borrows that may cross thread boundaries
- memory safety even when programmers choose nondeterministic concurrent mutation
- no atomic or locking overhead in ordinary single-threaded code
- explicit costs for shared ownership and synchronization
An optional cycle collector may eventually be provided for explicit shared-ownership
graphs. It must not run in the background by default.
## Core ownership model
### Plain values
Plain `T` values use inline storage. Values implementing `ImplicitCopy` are copied by
ordinary assignment and argument passing. Other values move by default and are destroyed
at their compiler-determined ownership boundary.
### Unique managed references
`ref T` is a unique, affine owning handle. At most one owning handle for an allocation
may exist at a time.
- Assignment, argument passing, capture, and return transfer the handle unless an
operation explicitly constructs an independent value.
- Moving a `ref T` invalidates the source handle.
- `clone(refValue)` creates a fresh allocation and clones the referent; it does not create
a second owner of the original allocation.
- Destruction of the sole owner destroys the referent and releases its allocation.
Owner uniqueness is a frontend invariant. Random generation IDs and runtime checks can
detect stale access, but cannot establish unique ownership.
If Peon later provides shared ownership, it should use distinct explicit types:
- `Rc[T]` for non-atomic, thread-local shared ownership
- `Arc[T]` for atomic, cross-thread shared ownership
- `Weak[T]` for non-owning references into an `Rc` or `Arc` allocation
The ordinary `ref T` type must not silently become reference-counted or shared.
## Freely aliasable borrows
`lent T` and `mut lent T` are non-owning views. They never destroy their referent.
Unlike Rust, Peon does not impose the rule "many immutable borrows or one mutable
borrow." Any number of mutable and immutable borrows may refer to overlapping storage:
```peon
var owner = new(int64);
let a = mut borrow(owner);
let b = mut borrow(owner);
a[] = 1;
b[] = 2;
```
In sequential code, operations through these aliases occur in ordinary program order.
This is memory-safe as long as the owner remains alive and the referenced storage remains
stable.
The performance consequence is that the compiler generally cannot assume `mut lent`
parameters are exclusive. It must not attach C `restrict`-like or LLVM `noalias`
semantics unless a separate API explicitly promises exclusivity.
An optional exclusive-borrow type or parameter annotation may be added later for
specialized high-performance APIs, but it is not the default meaning of `mut lent`.
## Borrow lifetime and provenance
Freely aliasable borrows still require lifetime checking. The compiler must prevent a
borrow from outliving or invalidating its storage.
Provenance analysis must cover all escape sinks, including:
- function returns
- assignment into globals or longer-lived object fields
- escaping closures
- generator and async frames
- task and thread arguments
- storage in containers whose lifetime exceeds the owner
When a borrow is live, operations that can invalidate its storage must be rejected or
delayed. Depending on the storage kind, these include:
- destroying or moving the owner
- reallocating a collection's backing storage
- replacing an owner cell
- unmapping or recycling the allocation
Runtime generation checks remain useful as hardening, for dynamically checked weak
references, and where static provenance is deliberately incomplete. A random 64-bit
generation is probabilistic stale-reference detection, not a proof of ownership or a
substitute for a valid metadata-lifetime policy.
## Crossing thread boundaries
### Structured thread scopes
Borrows may cross threads only through a structured thread scope whose children are
joined before the scope exits:
```peon
thread scope workers {
spawn worker(mut borrow(value));
spawn worker(mut borrow(value));
}
```
For the lifetime of `workers`:
- `value` and its backing storage outlive every child
- the owner cannot be moved or destroyed
- relocatable backing storage cannot be reallocated
- child borrows cannot escape the scope
The compiler should prove these constraints from provenance and the lexical scope. When
the owner is dynamic and static proof is unavailable, the runtime may pin it once when
the borrow enters the thread scope and unpin it after join. It should not pin and unpin
the owner on every dereference.
Structured lifetime safety does not by itself synchronize access to the payload.
### Transfer versus sharing
Moving a uniquely owned value into a child transfers it to that thread. Once transferred,
ordinary accesses remain non-atomic because no other safe handle can access it.
Borrowing the same value into multiple children shares it. Shared immutable reads are
safe when the referent cannot be mutated for the duration of the scope. Shared mutation
uses one of the access models below.
## Concurrent access models
Peon must not lower unsynchronized conflicting accesses to ordinary C loads and stores
while claiming memory safety. A C data race is undefined behavior and can cause memory
corruption, not merely a nondeterministic result.
Peon therefore distinguishes ordinary shared storage, atomic storage, and representations
that are explicitly safe to race on.
### Ordinary `T`
Multiple cross-thread `mut lent T` handles may exist, but conflicting accesses to an
ordinary `T` require synchronization such as:
- `Mutex[T]` or `RwLock[T]`
- channels or ownership transfer
- actor isolation
- a user-defined internally synchronized abstraction
Unsynchronized conflicting access to ordinary storage is not safe Peon. It must either
be rejected by the relevant API or require an explicit `unsafe` block. It must not be
silently emitted as a racy C access.
### `Atomic[T]`
`Atomic[T]` provides explicit operations and memory orderings for supported scalar or
pointer-sized values:
```peon
let counter: mut lent Atomic[int64] = ...;
counter.fetchAdd(1, relaxed);
```
Atomic operations may still participate in logical races, but they do not create a
language-level data race. Relaxed atomics should be available when the programmer only
needs indivisible access rather than inter-thread ordering.
### `shared mut lent T`
Peon may provide an explicit shared view for ordinary-looking, implicitly atomic access:
```peon
let shared = share(mut borrow(counter));
```
Loads and stores through `shared mut lent T` use atomic operations. The view itself is
cheaply copyable and may be sent to multiple threads.
This facility is only sound for types with a race-safe representation. A compiler-known
`RaceSafe` marker should be derived conservatively.
Likely `RaceSafe` types include:
- integers and booleans with supported atomic widths
- suitable floating-point representations when supported by the target
- pointer-sized tokens with explicitly atomic access
- structures whose independently accessible fields are all `RaceSafe`
Types that are not automatically `RaceSafe` include:
- strings, sequences, and slices represented by multiple related words
- generational references represented by `(ptr, owner, generation)`
- tagged unions whose tag and payload can be observed inconsistently
- types with validity invariants spanning multiple independently mutated fields
- values wider than the target can atomically load or store as a unit
Even a structure of `RaceSafe` fields offers only per-field atomicity. It does not provide
a coherent snapshot or preserve application-level invariants across fields. Such
invariants still require a lock, a sequence lock, immutable copy-and-swap, or another
purpose-built abstraction.
## Thread eligibility
Peon needs compiler-known equivalents of the following properties:
- `Send`: ownership of a value may be transferred to another thread
- `Sync`: an immutable borrow may be shared between threads
- `RaceSafe`: supported accesses through a shared mutable view have defined atomic
semantics
These should be marker properties with no runtime representation. They are derived from
the full transitive contents of a type and may only be implemented manually through an
`unsafe` mechanism.
Suggested defaults:
- plain scalar values are `Send` and `Sync`
- a value object is `Send` or `Sync` when all of its fields are
- unique `ref T` is `Send` when `T` is `Send`
- a moved unique owner does not require atomic access in its destination thread
- `lent T` may cross a scoped thread boundary when `T` is `Sync` and provenance is valid
- freely aliasable `mut lent T` may cross a scoped thread boundary, but payload access
must follow the concurrent access models above
- local `Rc[T]`, raw pointers, unsynchronized FFI handles, and unsafe closure captures do
not derive thread eligibility automatically
## `#pragma[thread]` and call propagation
`#pragma[thread]` means that a named function is eligible to execute in an OS-threaded
context. It is a semantic effect, not merely a request to select atomic allocator helpers.
Thread context propagates transitively through calls, but users should not have to place
the pragma on every helper.
When a threaded function calls an otherwise ordinary function, the compiler should:
1. Check the callee and its arguments under the threaded effect.
2. Reuse the ordinary implementation if its behavior and lowering are context-independent.
3. Emit a threaded specialization if reference, shared-access, or runtime lowering differs.
4. Reject the call if the callee uses thread-local-only state, unsynchronized mutable
globals, thread-unsafe FFI, or another operation forbidden in a threaded context.
The threaded effect must be present in function and closure types so indirect calls cannot
bypass these checks. Closures used as thread entry points must have thread-eligible
captures.
The compiler should avoid duplicating functions that contain only pure value computation
or otherwise generate identical code in both contexts. Specialization is needed only
where behavior or runtime operations differ.
### Globals
Annotating an ordinary mutable global with `#pragma[thread]` does not make its payload
safe to access concurrently. The language should distinguish:
- thread-local globals, with one instance per OS thread
- shared immutable globals
- shared `Atomic`, locked, or internally synchronized globals
An annotation may grant visibility from threaded code, but it cannot substitute for a
synchronization or representation rule.
## Runtime implications
The common paths should have the following costs:
| Operation | Intended cost |
|-----------|---------------|
| Owned local dereference | Raw pointer access; no atomic operation |
| Proven local `lent` dereference | Raw pointer access or one hoisted validity check |
| Local allocation | Thread-local allocator cache; no global lock in the common path |
| Move into another thread | Ownership transfer; normally no runtime synchronization |
| Borrow into structured threads | Static proof, or one pin per boundary crossing |
| Immutable scoped sharing | No per-dereference synchronization |
| `Arc` clone/drop | Atomic strong-count operation |
| `Weak` upgrade | Atomic lifetime validation |
| `Atomic` or shared-view access | Explicit atomic operation |
| Locked mutation | Explicit synchronization operation |
The existing threaded open protocol, which atomically pins an owner for each dereference
and records that pin in thread-local storage, should not be the long-term common path.
Lifetime protection belongs at ownership and structured-concurrency boundaries wherever
possible.
Owner metadata also needs a deterministic lifetime rule. Acceptable strategies include:
- reclaiming it with the owner when static analysis proves no dynamic stale handles exist
- weak-counting the metadata when `Weak` or other dynamic checked handles exist
- retaining a bounded allocator arena with an explicit reuse and exhaustion policy
Keeping all metadata resident forever is acceptable as an early prototype strategy, not
as the final memory model for long-running programs.
## Cycles and optional collection
Unique `ref` ownership should make ordinary ownership graphs acyclic by construction.
Explicit `Rc` and `Arc` graphs may form cycles and should use `Weak` edges to break them.
If Peon later provides cycle collection:
- it applies only to explicit shared-ownership graphs
- it is disabled by default
- it runs synchronously when requested or at an explicitly configured safe point
- it does not run as an implicit background service
- destructor ordering and interaction with concurrent graph mutation must be specified
A concurrent general-purpose cycle collector is not required for the initial threading
model.
## Safety guarantee
Safe Peon should guarantee:
- use-after-free and double-free prevention
- deterministic destruction of uniquely owned values
- valid lifetimes for borrows crossing structured thread scopes
- freely aliasable `mut lent` handles
- defined concurrent mutation through `Atomic`, `RaceSafe` shared views, or synchronized
abstractions
- no hidden tracing collector or background memory-management work
Peon does not guarantee deterministic application results when multiple threads perform
logically racing atomic operations. It does guarantee that such supported races do not
become C undefined behavior or corrupt the language runtime.
Unsynchronized conflicting access to an ordinary non-atomic representation is outside
safe Peon and requires an explicit `unsafe` boundary.
## Prior art
- Rust separates thread transfer and sharing with
[`Send` and `Sync`](https://doc.rust-lang.org/nomicon/send-and-sync.html), and separates
local `Rc` from atomic [`Arc`](https://doc.rust-lang.org/std/sync/struct.Arc.html).
- Rust's [scoped threads](https://doc.rust-lang.org/std/thread/fn.scope.html) demonstrate
how lexical joining permits threads to borrow non-static storage safely.
- Swift's [`Sendable`](https://github.com/swiftlang/swift-evolution/blob/main/proposals/0302-concurrent-value-and-concurrent-closures.md)
provides a compiler-known concurrency-domain boundary.
- Pony's [reference capabilities](https://tutorial.ponylang.io/reference-capabilities/reference-capabilities.html)
distinguish isolated transfer, immutable sharing, and mutable access rights.
- Nim's [ARC/ORC memory managers](https://nim-lang.org/docs/mm.html) demonstrate
deterministic reference counting with cycle collection either omitted or provided as
a separate strategy.
- Koka's [Perceus](https://koka-lang.github.io/koka/doc/book.html#why-perceus) demonstrates
compiler optimization of deterministic reference counting and allocation reuse under
strong cycle and sharing constraints.
## Open questions
- Final syntax for structured OS-thread scopes and shared mutable views.
- Whether `RaceSafe` is user-visible or only appears in diagnostics and generic bounds.
- Which scalar widths and floating-point types are atomically supported on each target.
- Whether shared-view field accesses are automatically atomic or require fields to be
declared `Atomic` explicitly.
- The exact unsafe boundary for unsynchronized ordinary cross-thread access.
- How threaded effects participate in overload resolution and generic specialization.
- Whether dynamic owner pinning blocks destruction, reports an error, or is impossible
outside runtime-internal weak-reference operations.
- The final metadata reclamation strategy for dynamically checked stale handles.