The Loup Freestanding Book — contents
  1. Chapter 1: What Is Freestanding Mode?
  2. Chapter 2: Building a Bare-Metal Binary
  3. Chapter 3: Integer Types and Wrapping Arithmetic
  4. Chapter 4: Functions and Control Flow
  5. Chapter 5: Structs and Layout Control
  6. Chapter 6: Enums and Pattern Matching
  7. Chapter 7: Classes and Allocators
  8. Chapter 8: Interfaces and Generics
  9. Chapter 9: Error Handling with Result
  10. Chapter 10: Ownership Verbs
  11. Chapter 11: Borrow and Lifetimes
  12. Chapter 12: Unique Ownership
  13. Chapter 13: Memory Primitives
  14. Chapter 14: Inline Assembly
  15. Chapter 15: MMIO with Volatile
  16. Chapter 16: Interrupts and Naked Functions
  17. Chapter 17: Entry Points and Panic
  18. Chapter 18: Sections and the Linker
  19. Chapter 19: Multicore and Atomics
  20. Chapter 20: The Available Standard Library Subset
  21. Chapter 21: Example — x86_64 Kernel Stub
  22. Chapter 22: Testing and Deploying Firmware
  23. Chapter 23: Memory Safety and Kernel Development Patterns
  24. Chapter 24: synchronized Classes and Lock Ordering

Chapter 10: Ownership Verbs

With no garbage collector and no reference counting under a freestanding image, something else has to say who may read a value, who may change it, and when its owner gives it away. In Loup that is the job of the ownership verbs: reads, edits, takes and shares. A verb on a parameter declares what the function does with the argument; the call site acknowledges it; the checker enforces it (Language Reference §3-2.4.9).

This chapter covers the four verbs on parameters and on method receivers, modifier, safe contexts, and @unsafe. Chapters 11 and 12 continue with borrows, lifetimes and unique.

The same buffer in C and in Loup

A NIC driver fills a transmit buffer, hands it to the device, and must not touch it again until the device is done. In C nothing records that rule:

struct tx_buf { uint8_t bytes[1514]; uint32_t len; };

void transmit(struct tx_buf *buf) {
    nic_post_descriptor(buf);    /* the device now owns the bytes      */
    buf->len = 0;                /* compiles; races with the device's DMA */
}

In Loup the hand-off is part of the signature. A takes method consumes its receiver, so the caller's binding is dead afterwards:

@mode(freestanding)

unique class TxBuffer {
    pub var frame: uint64;          # physical address of the bytes
    pub var length: uint32;

    new(frame: uint64, length: uint32) {
        this.frame = frame
        this.length = length
    }

    reads func size(): uint32 {
        return this.length
    }

    # Gives the buffer to the device; returns the descriptor value to post.
    takes func handToDevice(): uint64 {
        return this.frame | (this.length as uint64)
    }
}

func transmit(): uint64 {
    let tx = TxBuffer(0x20_0000u64, 1514u32)
    let bytes = tx.size()              # read it while we still own it
    let descriptor = tx.handToDevice() # from here on, `tx` is gone
    return descriptor + (bytes as uint64)
}

Listing 10-1: A takes method ends the caller's ownership

Touching the buffer after the hand-off — the C bug above — does not compile:

This code does not compile
@mode(freestanding)

unique class TxBuffer {
    pub var frame: uint64;
    pub var length: uint32;
    new(frame: uint64, length: uint32) { this.frame = frame; this.length = length; }

    reads func size(): uint32 { return this.length }
    takes func handToDevice(): uint64 { return this.frame }
}

func transmit(): uint32 {
    let tx = TxBuffer(0x20_0000u64, 1514u32)
    let descriptor = tx.handToDevice()
    return tx.size()
}
error[E_USE_AFTER_TAKE]: E_USE_AFTER_TAKE: binding 'tx' was consumed by a `takes` parameter and cannot be used again
  --> src/main.lpfree:15:12
   |
15 |     return tx.size()
   |            ^^
   |

The receiver of a takes func is a takes parameter like any other, which is what the message says. Read what you need before giving the value away, as Listing 10-1 does.

The four verbs

Verb Meaning Call site
reads Shared, read-only borrow. The caller keeps ownership. The default when no verb is written. f(x) or f(reads: x)
edits Exclusive, mutable borrow. The caller keeps ownership and sees the changes. f(edits: x) — required
takes Ownership transfer. The caller's binding is consumed. f(takes: x) — required
shares An ARC retain: caller and callee both keep a reference. f(shares: x) — required

The verb goes before the parameter name: func reset(edits stats: NicStats). On a method, it goes before func and applies to the receiver: reads func size(), takes func handToDevice().

shares exists for ARC values in the hosted modes. Freestanding has no ARC, so there is nothing for it to retain. The 1.25 checker does not reject it, but it has no meaning here: use reads/edits to lend, takes to give.

reads — the default

A parameter with no verb is reads: the function can look but not change. That covers value types too — a struct argument is a borrow of the caller's value, not a private copy you may scribble on:

This code does not compile
@mode(freestanding)

struct NicStats {
    var rxPackets: uint64;
    var rxBytes: uint64;
}

func countRx(stats: NicStats, length: uint64): void {
    stats.rxPackets = stats.rxPackets + 1u64
    stats.rxBytes = stats.rxBytes + length
}
error[E_READS_MUTATION]: E_READS_MUTATION: parameter 'stats' is a `reads` borrow (a parameter without a verb is read-only, §3-2.4.9) and cannot be mutated (field 'rxPackets' assigned); declare it `edits` and pass `edits: …` to change the caller's value, or copy it into a local first
 --> src/main.lpfree:9:5
  |
9 |     stats.rxPackets = stats.rxPackets + 1u64
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |

error[E_READS_MUTATION]: E_READS_MUTATION: parameter 'stats' is a `reads` borrow (a parameter without a verb is read-only, §3-2.4.9) and cannot be mutated (field 'rxBytes' assigned); declare it `edits` and pass `edits: …` to change the caller's value, or copy it into a local first
  --> src/main.lpfree:10:5
   |
10 |     stats.rxBytes = stats.rxBytes + length
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

The message lists both fixes. If the caller should see the new counts, the parameter is edits; if the function only needs a scratch copy, bind one with var local = stats.

The rule also covers calling a modifier method (below) on a class-typed reads parameter: that is a mutation of the caller's object too.

edits — exclusive, and acknowledged

An edits parameter may be changed, and the change is the caller's. Because that matters to the caller, the call site must say edits::

This code does not compile
@mode(freestanding)

struct NicStats {
    var rxPackets: uint64;
    var rxBytes: uint64;
}

func countRx(edits stats: NicStats, length: uint64): void {
    stats.rxPackets = stats.rxPackets + 1u64
    stats.rxBytes = stats.rxBytes + length
}

func onReceive(length: uint64): uint64 {
    var stats = NicStats(rxPackets = 0u64, rxBytes = 0u64)
    countRx(stats, length)
    return stats.rxPackets
}
error[E_VERB_REQUIRED]: E_VERB_REQUIRED: parameter 'stats' requires 'edits' verb acknowledgment at call site
  --> src/main.lpfree:15:13
   |
15 |     countRx(stats, length)
   |             ^^^^^
   |

Someone reading onReceive now knows stats changes in that call. The acknowledgment must also match the declaration — writing reset(takes: stats) for an edits parameter is E_VERB_MISMATCH: call-site verb 'takes' does not match parameter 'stats' declared as 'edits'. The corrected code:

struct NicStats {
    var rxPackets: uint64;
    var rxBytes: uint64;
}

func countRx(edits stats: NicStats, length: uint64): void {
    stats.rxPackets = stats.rxPackets + 1u64
    stats.rxBytes = stats.rxBytes + length
}

func reset(edits stats: NicStats): void {
    stats.rxPackets = 0u64
    stats.rxBytes = 0u64
}

func onReceive(length: uint64): uint64 {
    var stats = NicStats(rxPackets = 0u64, rxBytes = 0u64)
    countRx(edits: stats, length)
    countRx(edits: stats, length)
    let packets = stats.rxPackets          # 2
    reset(edits: stats)
    return packets
}

Listing 10-2: edits parameters and their call-site acknowledgments

edits is also exclusive: while one is active, no other borrow of the value may be. The Language Reference makes passing the same value as two edits arguments of one call E_EDITS_ALIAS; the 1.25 checker does not detect that case yet, so do not rely on it to catch merge(edits: q, edits: q).

takes — giving a value away

A takes parameter receives ownership. The caller acknowledges with takes:, and its binding is dead after the call (E_USE_AFTER_TAKE). With unique values the transfer is a move with no run-time cost (chapter 12):

unique class Frame {
    pub var number: uint64;
    new(number: uint64) { this.number = number; }
}

# The free list takes ownership of a physical frame.
var freeCount: uint64 = 0

func releaseFrame(takes f: Frame): void {
    freeCount = freeCount + 1u64
    # ... push f.number onto the free list ...
}

func unmapAndFree(): uint64 {
    let f = Frame(0x1234u64)
    let number = f.number
    releaseFrame(takes: f)
    return number                     # `f` itself can no longer be used
}

Listing 10-3: Transferring a frame to the free list with takes

Use takes wherever the callee becomes responsible for the value: a buffer posted to a device, a frame returned to an allocator, a task handed to a scheduler.

Receiver verbs

The same verbs on a method describe what the method does to this:

unique class PageRun {
    pub var start: uint64;
    pub var pages: uint64;
    new(start: uint64, pages: uint64) { this.start = start; this.pages = pages; }

    reads func end(): uint64 {               # looks only
        return this.start + this.pages * 4096u64
    }

    edits func grow(extra: uint64): void {   # changes this run in place
        this.pages = this.pages + extra
    }

    takes func split(): uint64 {             # consumes the run
        return this.start
    }
}

func demo(): uint64 {
    var run = PageRun(0x10_0000u64, 4u64)
    run.grow(2u64)
    let end = run.end()
    let start = run.split()
    return end - start
}

Listing 10-4: reads, edits and takes receivers

modifier

On a class, modifier marks a method that writes the object's var fields (§3-2.4.11). It may not be used on a struct method — structs are values, so there is no aliasing for it to guard (E_MODIFIER_ON_STRUCT):

class DeviceState {
    pub var resets: uint32 = 0;
    pub var online: bool = false;

    pub modifier func reset(): void {
        this.resets = this.resets + 1u32
        this.online = false
    }

    pub func isOnline(): bool {
        return this.online
    }
}

func recover(edits dev: DeviceState): bool {
    dev.reset()
    return dev.isOnline()
}

Listing 10-5: A modifier method called through an edits parameter

In freestanding, the checker requires modifier only on synchronized classes, where it is what takes the lock (chapter 24); on a plain class a method that writes a field without modifier is accepted. Write modifier anyway: it documents which methods change the object, it is required in the hosted modes, and it is what reads parameters are checked against — calling a modifier method on a reads parameter is E_READS_MUTATION.

safe contexts

A safe { … } block, or a function declared safe func, asks the compiler to enforce shared-XOR-mutable rules for everything in scope, including plain class references (§3-2.4.12). In the hosted modes, calling a modifier method on an ARC object requires one. In freestanding there is no ARC; safe blocks are accepted and checked, and a function with an edits parameter is implicitly safe func:

class Counter {
    pub var hits: uint32 = 0;
    pub modifier func bump(): void { this.hits = this.hits + 1u32 }
}

safe func bumpTwice(edits c: Counter): void {
    c.bump()
    c.bump()
}

func demo(): uint32 {
    let c = Counter()
    safe {
        c.bump()
    }
    bumpTwice(edits: c)
    return c.hits                        # 3
}

Listing 10-6: A safe block and a safe func

requires clauses state contracts across several parameters, for example that two buffers do not overlap: func copyInto(dst: Queue, src: Queue) requires edits(dst), distinct(dst, src): void. Both compilers parse the clause and apply its verbs to the parameters, but the call-site acknowledgment and the distinct checks (E_DISTINCT_ALIAS, E_REQUIRES_UNACKNOWLEDGED) are not implemented in 1.25 (§3-2.4.10). Treat distinct as documentation for now.

@unsafe("reason") — the audited escape

When code does something the compiler cannot check — trusting a hard-coded address, viewing memory through an overlay, a naked function — Loup asks for an explicit, greppable acknowledgment with a reason. It is written two ways:

  • @unsafe("reason") on a declaration (a function, a module variable, an overlay binding);
  • unsafe("reason") { … } around a block of statements.
@unsafe("mmio: the firmware maps the HPET registers at this physical address")
func hpetBase(): uint {
    return 0xFED0_0000
}

func readScratch(base: uint): uint64 {
    var value: uint64 = 0
    unsafe("raw read: `base` is the scratch page the boot loader reserved") {
        value = bufGetU64(base, 0)
    }
    return value
}

Listing 10-7: @unsafe on a declaration and an unsafe region

The reason is a plain string argument: @unsafe("…"), not @unsafe(reason: "…"). grep -E '@?unsafe\(' then lists every such site in a code base. Which operations require the acknowledgment is decided per feature: @naked functions always do (chapter 16), buffer overlays do (a warning in 1.25, an error with [freestanding] overlays = "error", chapter 13), and raw-poke intrinsics such as bufGetU64 do when the package sets [freestanding] rawpoke = "unsafe-only". Inline asm { } does not need @unsafe in freestanding (chapter 14).

Parameter forms at a glance

Parameter Meaning May change the caller's value? Caller writes
x: T / reads x: T shared borrow no f(x)
edits x: T exclusive borrow yes f(edits: x)
takes x: T ownership transfer — the callee owns it f(takes: x)
borrow x: T shared borrow (older spelling of reads) no f(x) or f(borrow x)
excl borrow x: T exclusive borrow of a struct (older spelling of edits) yes f(x)
borrow[~a] x: T borrow tied to lifetime ~a no f(x)
volatile borrow x: T device registers: every access is volatile yes (MMIO stores) f(dev), passing on another volatile borrow

Chapter 11 covers the borrow forms and lifetimes; chapter 15 covers volatile borrow.

Summary

  • Verbs go before the parameter name; receiver verbs go before func. reads is the default.
  • Writing through a reads parameter is E_READS_MUTATION; declare it edits or copy it.
  • edits, takes and shares must be acknowledged at the call site (E_VERB_REQUIRED), with the matching verb (E_VERB_MISMATCH).
  • After takes, the caller's binding is dead (E_USE_AFTER_TAKE), including after calling a takes func method.
  • shares is an ARC concept with no meaning in freestanding.
  • modifier marks class methods that write fields; freestanding enforces it on synchronized classes. It is not allowed on struct methods.
  • safe blocks and safe func work in freestanding; requires distinct(...) is parsed but not yet checked.
  • @unsafe("reason") and unsafe("reason") { } are the audited escapes.

Next: borrows and lifetimes.