sysl.threads

Every declaration in sysl.threads, with its signature: the generated API page. This page is the argument — what the module is for, and how its pieces fit; that one is the list.

sysl.threads is where the capability lands. Everything on the sysl.sync page is reachable from a module that has given up its allocator and its operating system; nothing here is, because creating a thread needs a scheduler underneath it.

@no_os

import sysl.sync.*
import sysl.threads.spawn

var a = Atomic(0)

print(a.load())

this reaches 'sysl.threads', which requires 'os', and this module declared 'no os'

Note where that lands: at the import, not at the call. A capability a module has given up decides which modules exist for it, so a program that cannot spawn is a program whose author never sees the name — and the sysl.sync import on the line above is untouched, which is the split working exactly as it is meant to.

The module asks for an operating system and nothing more — not POSIX, not a C library:

module sysl.threads
@requires(os)

A thread is something a scheduler gives a program, and what starts one is whatever answers the hooks of sysl.threads.sys, as sysl.fs reaches files through sysl.fs.sys. On a hosted target the library answers them itself, over pthreads and the platform’s futex; on a target with no C library a kernel answers them with an @export each, over its own clone and futex — see On a target with no C library. sysl.posix.threads is the same API under the name it had when it was pthreads by symbol, kept for the programs that import it.

spawn takes an address, not a callable

import sysl.threads.*

struct Job
    input: i32
    output: i32

square(j: *Job)
    j.output = j.input * j.input

var job = Job(12, 0)
var t = spawn(&square, &job).unwrap()

t.join()

print(job.input, job.output)

12 144

&square is the address of a named function, and the parameter’s type is *extern(*T) -> unit — C’s own shape, because what is underneath is a system’s thread start: pthread_create on a hosted target, a kernel’s clone on a bare one. A closure will not do, and the refusal is worth seeing in both of the ways a reader will hit it. Written bare, the argument has nothing to infer its parameter type from, because T is what is being inferred:

import sysl.sync.*
import sysl.threads.*

var counter = Atomic(0)
var c = spawn(a -> a.add(1), &counter)

print(c.is_some())

'a' has no type here — nothing says what this closure takes, so write it

Write the type in and the real mismatch surfaces:

import sysl.sync.*
import sysl.threads.*

var counter = Atomic(0)
var c = spawn((a: *Atomic[i32]) -> a.add(1), &counter)

print(c.is_some())

'body' of 'sysl.threads.spawn' is *extern(*sysl.sync.Atomic[int]) -> unit, but a closure was given

Two reasons, and neither is a limitation waiting to be lifted. A closure would have to be boxed for the new thread to reach it, which needs an allocator this module could otherwise do without; and its captures would be values crossing a domain boundary through a box whose shape says nothing about what is in it. The address of a named function has neither problem, and what travels beside it is an ordinary parameter — which is what lets the crossing rule be asked at all.

A body with nothing to read is passed null

spawn is generic in what the body reads, so T is inferred from the body and the ptr_cast to C’s shape happens once, inside. A body with nothing of its own writes null, and the type it would otherwise have had to invent is one the body’s own signature already gave:

import sysl.threads.*

quiet(state: *int)
    print("nothing to read")

spawn(&quiet, null).unwrap().join()

nothing to read

null has no type of its own, so at a parameter still being solved it is set aside until the arguments that have one are read — here the &quiet, whose *extern(*int) -> unit says T is int. It is refused only where nothing says: a call with no other argument to read is an error asking for the type rather than a guess.

join does not carry the result back

It answers a bool — whether it waited — and nothing else. That is the crossing rule rather than an oversight: a result coming out of another domain is a value crossing a boundary, which is what a channel is for. So a body that has something to say writes it through the address it was given, or sends it, which is what the Job above does.

The Thread value is a handle rather than the thread. Copying one copies the handle, and joining either copy joins the one thread; joining twice is not checked — the second join would give the thread’s storage back a second time — for the same reason SpinLock.unlock checks nothing: the word it would take to notice is paid by every correct program. A thread never joined keeps its storage for the rest of the program. The id field is public: the pthread_t on a hosted target, which a program can hand to a POSIX call this module does not wrap, and the kernel’s thread id on a bare one.

The library owns the stack

spawn makes one allocation per thread — its id word, its block of @thread_local storage, and its stack, 64 KiB unless the call asks for another size — and join gives it back. On a hosted target nothing is allocated: pthreads makes the stack and the C library the thread-local block. A program with no heap starts a thread on storage of its own with spawn_on, which lays the same three things out of a slice it is handed:

import sysl.threads.*

static var stack: [262144]u8 = [0; 262144]

shout(n: *int)
    *n *= 2

var n = 21

spawn_on(stack[..], &shout, &n).unwrap().join()

print(n)

42

The slice has to outlive the thread — the contract spawn(&body, &state) already has with whatever state points at. On a hosted target the stack is handed to pthreads, which asks for at least its PTHREAD_STACK_MIN (16 KiB on macOS, 128 KiB under glibc on aarch64) and is trimmed to whole 16 KiB pages first; a slice with no room left once the word and the thread-local block are laid answers None.

Sharing the thing at the address

The pointer is the sharing. Two threads reading and writing what is at that address is a data race unless something orders them, and the two things that order them are on the sysl.sync page.

What may be at that address

spawn is declared @crossing(arg), which is how a facility says a parameter hands a value to another concurrency domain (memory). It is why the state a thread is given is checked rather than taken on trust: a raw pointer carries no refcount of its own, and the annotation is what asks the compiler to look through it at the object that actually crossed.

import sysl.threads.*

struct Cell
    n: int

struct State
    cell: &Cell

look(s: *State)
    print(s.cell.n)

var c: &Cell = Cell(1)
var st = State(c)

print(spawn(&look, &st).is_some())

what 'arg' of 'sysl.threads.spawn' points at reaches another concurrency domain, so every count inside it has to be atomic

A plain &Cell has a non-atomic count, so two threads retaining it is exactly the race the model exists to prevent — and until the annotation existed, this program compiled and ran. Writing &sync Cell in the field and at the allocation is the whole fix: the count becomes atomic, and the same program is accepted.

Nothing here is special to this module. A package binding FreeRTOS or Zephyr writes the same line above the wrapper it already has, and gets the same refusal at its own callers’ calls.

import sysl.sync.*
import sysl.threads.*

bump(a: *Atomic[i32])
    for i in 0..<10000
        a.add(1)

var counter = Atomic(0)
var t1 = spawn(&bump, &counter).unwrap()
var t2 = spawn(&bump, &counter).unwrap()
var j1 = t1.join()
var j2 = t2.join()

print(j1, j2)
print(counter.load())

true true
20000

A SpinLock works across real threads exactly as it does in the single-threaded program on the other page, and this is where its “guards nothing by construction” becomes concrete — the lock is a field beside the data, and remembering that total is what guard guards is the programmer’s job:

import sysl.sync.*
import sysl.threads.*

struct Shared
    guard: SpinLock
    total: i32

add_up(s: *Shared)
    for i in 0..<10000
        s.guard.with(() -> s.total = s.total + 1)

var sh = Shared(SpinLock(0), 0)
var s1 = spawn(&add_up, &sh).unwrap()
var s2 = spawn(&add_up, &sh).unwrap()

s1.join()
s2.join()

print(sh.total)

20000

Take the atomic away and it is a race

import sysl.threads.*

racy(p: *i32)
    for i in 0..<100000
        *p = *p + 1

var n = 0
var r1 = spawn(&racy, &n).unwrap()
var r2 = spawn(&racy, &n).unwrap()

r1.join()
r2.join()

print(n)

That program is a data race by definition: two threads, one word, no synchronization. On the run that produced this page it printed 200000 — the right answer. It is not on the site as a checked program for exactly that reason, and the reason is the lesson: a race that gives the right answer on the machine you tested it on is why the model is built out of things you can grep for rather than things you can test for. *T is one of the two spellings that share on purpose, and it is the unchecked one.

Mutex[T]

Mutex[T] owns what it protects, which is the whole difference against SpinLock. Underneath it is a sysl.sync.Guarded[SleepLock, T] — the record-beside-its-lock every lock in the library shares (library/sync.md) — held in one private field, and Guarded keeps its own value private in turn, so there is no way to reach the value that does not go through the lock:

import sysl.threads.*

var m = Mutex.new(7)

print(m.inner)

field 'inner' of 'sysl.threads.Mutex' is private to 'library/sysl/threads/mutex.sysl', the file that declares it

Private is the entirety of what “owns” means here. With the value public, reading it would be an unsynchronized read of the very thing the type exists to synchronize, and the type would be a spinlock with a suggestion attached.

The private field does a second job: it puts the positional constructor out of reach, so Mutex.new is the only way in and there is no way to build one that starts out held.

import sysl.sync.Guarded
import sysl.threads.*

var built: Mutex[int] = Mutex(Guarded.new(SleepLock.new(), 5))

built.with((p) -> print(*p))

the constructor names every field of 'sysl.threads.Mutex' in order, and 'inner' is private to 'library/sysl/threads/mutex.sysl', the file that declares it — build it through an associated function of its own

with lends the value for one call

m.with(body) takes the lock, calls body with the address of the value, releases the lock when body returns, and answers whatever body answered:

import sysl.threads.*

inc(m: *Mutex[i32])
    for i in 0..<10000
        m.with((n) -> *n += 1)

var mx = Mutex.new(0)
var a1 = spawn(&inc, &mx).unwrap()
var a2 = spawn(&inc, &mx).unwrap()

a1.join()
a2.join()

print(mx.with((n) -> *n))

20000

The address is lent, and the compiler holds the closure to giving it back. with is declared @lends(body), so a closure passed there may read and write through the address, and hand it to a function that only uses it, but may not let it outlive the call — the mistake an address returned from lock could never be protected from:

import sysl.threads.*

var m = Mutex.new(1)
val p = m.with((n) -> n)

print(*p)

lends this body a pointer that is valid only until the call returns, and this one is returned

Rust answers the same question with a guard whose destruction releases the lock. A sysl destructor runs for a value behind a &T, so a guard would be a heap allocation per hold — on the one path where the point is to hold a lock for as few instructions as possible. The closure costs nothing: body is a type parameter, so each call is a direct call of that closure’s own body, and with is usable under @no_alloc.

try_with never waits, and answers an Option of what body answered — None where the lock was held:

import sysl.threads.*

var q = Mutex.new(5)
val qp = &q

print(q.try_with((v) -> *v).unwrap())
print(q.with((v) -> qp.try_with((w) -> *w).is_none()))

5
true

lock_raw is the hold a block cannot express

Some holds are not a block: a lock taken in one function and released in another, or handed from one thread to the next with the processor. lock_raw answers the address and unlock_raw releases it, and nothing ties the address to the hold — which is what the name says, and why with is the one to reach for wherever the hold does fit a block. defer is the idiom for a raw hold, as it is for sysl.fs‘s close:

import sysl.threads.*

var m = Mutex.new(3)
var p = m.lock_raw()

*p = *p * 2
m.unlock_raw()

var g = m.try_lock_raw()

print(g.is_some(), m.try_lock_raw().is_none())

m.unlock_raw()
print(m.with((v) -> *v))

true true
6

None of these takes an Ordering, because a lock’s orderings are fixed by what a lock means. The exchange that takes it is an acquire and the store that frees it is a release, and that pairing is what publishes everything the holder wrote to whichever thread takes the lock next. It is the whole of what makes the data safe to touch.

It is a futex lock written in sysl, not a pthread_mutex_t

The lock under Mutex[T] is a SleepLock: one Atomic[u32] and the two futex hooks, the classic three-state lock. The word is zero when free, one when held, and two when held with somebody asleep on it; an uncontended take and release are one atomic operation each and never reach the system, a contended take marks the word two and sleeps in sysl_futex_wait, and only a release that finds a two calls sysl_futex_wake. A waiter sleeps — it neither spins nor yields — so a contended lock costs nothing while it waits.

A pthread_mutex_t was never the answer, and the reason is a build property: its size lives in a header and differs between two libcs on the same platform — 64 bytes on Darwin, 40 under glibc on x86-64, 48 on aarch64, 40 again under musl — and the standard library reads no header. The futex is what every system that has threads keeps underneath its own mutex, so it is one word the library lays out itself, and the same SleepLock runs on a kernel answering the hooks as on a hosted target.

SleepLock is public for the hold Mutex[T] does not express — a lock beside data the program names itself, as SpinLock is, for code that may sleep:

import sysl.threads.*

var l = SleepLock.new()

print(l.try_lock(), l.try_lock())
l.unlock()
print(l.try_lock())

true false
true

A table locked record by record is Guarded[L, T]

Mutex[T] is one lock over one value. A table whose every record has a lock of its own — a buffer cache, an inode table — is an array of sysl.sync.Guarded[L, T]: the record and its lock side by side, inline, with no box. L is any type implementing sysl.sync.Lock (acquire, try_acquire, release), and SleepLock and SpinLock both do. with takes the record’s own lock, hands the closure the record in place, and releases on every way out; two threads holding two records run at once:

import sysl.sync.Guarded
import sysl.threads.*

struct Slot
    hits: int

var slots: [2]Guarded[SleepLock, Slot] = [Guarded.new(SleepLock.new(), Slot(0)),
                                          Guarded.new(SleepLock.new(), Slot(0))]

bump(t: *[2]Guarded[SleepLock, Slot])
    for _ in 0..<1000
        (*t)[0].with((s) -> s.hits += 1)
        (*t)[1].with((s) -> s.hits += 2)

val a = spawn(&bump, &slots).unwrap()
val b = spawn(&bump, &slots).unwrap()

a.join()
b.join()
print(slots[0].with((s) -> s.hits), slots[1].with((s) -> s.hits))

2000 4000

The table crosses because each record is @guards(value) and an array is shared element by element — the rule is reference/memory.md § A table whose every record has its own lock.

Condvar

A place to sleep until another thread says something changed. It is a sequence number every notify_one and notify_all bumps: a waiter reads it while it still holds the lock, lets the lock go and sleeps only while the number is still the one it read — so a notification sent between the release and the sleep is never slept through. A wait may end with nothing changed, so the condition is re-checked in a loop, as with every condition variable:

import sysl.threads.*

struct Rally
    m: Mutex[int]
    turn: Condvar

answer(r: *Rally)
    for i in 0..<3
        val n = r.m.lock_raw()

        while *n % 2 == 0
            r.turn.wait(&r.m)

        *n += 1
        r.m.unlock_raw()
        r.turn.notify_all()

var r = Rally(Mutex.new(0), Condvar.new())
var t = spawn(&answer, &r).unwrap()

for i in 0..<3
    val n = r.m.lock_raw()

    while *n % 2 == 1
        r.turn.wait(&r.m)

    *n += 1
    r.m.unlock_raw()
    r.turn.notify_all()

t.join()
print(r.m.with((n) -> *n))

6

wait_for(&m, ns) is the same with a limit, answering false where the time ran out first, and wait_raw(&lock) waits over a bare SleepLock.

Channel[T]

A bounded queue two threads hand values across, and the one place the rule about leaving a concurrency domain is asked of a value rather than of an address. Everything else on this page shares by address — spawn hands a *T, Mutex[T] hands a *T — and what crosses is a pointer whose far end both threads are looking at. A channel is the other shape: a value goes in on one thread and comes out on another, and the two are never looking at one object.

import sysl.threads.*

var slots: [4]int = [0; 4]
var ch = channel(slots[..])

print(ch.capacity(), ch.len(), ch.is_closed())
print(ch.try_send(1), ch.try_send(2))
print(ch.try_receive(), ch.try_receive(), ch.try_receive())

4 0 false
true true
Some(1) Some(2) None

The storage is the caller’s, which is this module’s house style rather than a limitation — Mutex[T] wraps a value the caller built and spawn takes an address the caller has. What it buys is that a channel needs no allocator at all, so it is available to a program that gave the heap up, and its capacity is a number the program chose. The storage has to outlive every thread holding the channel, which is the contract spawn(&body, &state) already has with whatever state points at.

import sysl.threads.*

struct Feed
    ch: Channel[int]

feeder(f: *Feed) -> unit
    for i in 1..5
        f.ch.send(i)

    f.ch.close()

var slots: [2]int = [0; 2]
var f = Feed(channel(slots[..]))
var running = spawn(&feeder, &f) match
    Some(t) -> t
    None -> panic("the thread did not start")

var total = 0

loop
    f.ch.receive() match
        Some(v) -> total += v
        None -> break

print(running.join(), total)

true 15

Five values go through a ring of two, so the producer really does fill it and really is woken.

@crossing(value) is written on send, and marking the way in is the whole check

send and try_send are the two operations that put a value in, so they carry @crossing(value) — which is what holds a caller to the rule about what may reach another domain. receive carries nothing and needs nothing: nothing can be taken out that was not put in, so a channel whose sends are held to the rule can hold nothing that breaks it.

They were free functions taking the channel by address until sysl let a member carry an annotation about a parameter, because the word had to go on a wrapper a caller already went through. That left a channel’s queries as methods and its transfers as functions, which is an asymmetry a reader had to learn and no longer has to.

import sysl.threads.*

struct Node
    n: int

var slots: [2]&Node = [Node(0); 2]
var ch = channel(slots[..])

print(ch.send(Node(1)))

reaches another concurrency domain, so every count inside it has to be atomic

A waiter sleeps

A full send sleeps on one Condvar and an empty receive on the other, each woken by the transfer that makes room or brings a value, and close wakes both — so a waiter costs nothing while it waits, and is not woken for a transfer that cannot help it.

The ring is a pointer, and that is the crossing rule

The slots are held as a *T and a count rather than as a []T, and it is not a preference: a struct holding a view may not reach another domain at all, because a view owns its elements through a count that is not atomic. A channel that kept the slice would have been refused at the spawn that shares it — one line before the first send, and for the only thing the type is for. A raw pointer carries no count, so it crosses; the caller writes a slice at channel(…) and never sees the pointer.

The ring is Ring[T] rather than four fields of this struct’s own, which it was until that module existed. A bounded queue over caller-supplied storage is what a channel is made of and is also a thing on its own, so what is left in this file is the lock and the closed flag; the wrapping arithmetic is over there and tested there. The pointer-and-count shape travelled with it for exactly the reason this section gives, which is why a channel can embed one.

The copying half of the crossing rule is still not written. The memory model allows a channel to take a heap-backed view because it copies the bytes, and this one assigns a slot — the same share the sender held. So a view is refused here exactly as it is at spawn.

yield_now and current

import sysl.threads.*

print(yield_now())

var me = current()
var mine = current()

print(me.id == mine.id)

true
true

yield_now is a hint, not a wait. A thread that yields is still runnable and may be handed the processor straight back. It answers whether the system took the offer.

current() is what a body compares against to learn that it is not the thread that spawned it. Its id is the one spawn answered for the thread; it cannot be joined, a thread waiting for itself waiting for ever.

On a target with no C library

Everything above is written over six hooks, the externs of sysl.threads.sys — the shape sysl.fs.sys and sysl.env.sys already have. On a hosted target sysl.threads.hosted answers them over pthreads and the platform’s futex (futex(2) on Linux and Android, os_sync_wait_on_address on macOS 14.4 and later); a program for a target with no C library answers each one it reaches with an @export, and one it leaves unanswered is refused when it is compiled, naming it:

The stack and the thread-local block are the library’s to lay out. spawn hands the hook a 16-aligned stack and, in tls, the value the thread pointer holds while the thread runs, the block behind it already laid out of the program’s template: every bare image’s link names the template’s bounds (__sysl_tls_data, __sysl_tls_data_end, __sysl_tls_end, __sysl_tls_align), and the library copies the initialized part and zeroes the rest at the offsets the linker wrote into every access. So a kernel’s spawn hook only writes the register — CLONE_SETTLS. The first thread is the one the library did not start; a program with @thread_local storage lays its block itself with tls_room() and tls_place(room) (@thread_local). On a hosted target tls is always null: the C library lays every thread’s storage down itself.

A build-c archive leaves the four template symbols undefined: the link that makes the image is the C project’s, and it defines them — with the same --defsyms, or in its linker script.

Threads and tasks

Threads are one of two ways sysl does two things at once. The other is the task: an async function’s call hands back a Task[T] without running it, await runs one to its result inside another, and something outside the tasks — block_on, or an executor written against step and park — decides which one runs next. Nothing on this page changes because tasks exist: a thread is still a thread, and every rule above still holds.

The two compose rather than compete. A task is a value, so it can be handed to a thread like any other — spawn‘s @crossing(arg) asks of the task’s frame what it asks of everything else at that address, and the thread runs it with an executor of its own:

import sysl.threads.spawn

struct Job
    t: Task[int]
    out: int

run(j: *Job)
    j.out = block_on(j.t)

async checksum(n: int) -> int
    var total = 0

    for i in 0..<n
        await yield_now()
        total += i

    total
end checksum

var job = Job(checksum(1000), 0)
val worker = spawn(&run, &job).unwrap()
val mine = block_on(checksum(2000))

worker.join()
print(job.out, mine)

499500 1999000

A task whose frame holds a string, an ordinary &T across an await, a value a statement computed before its await, or a park is refused at that spawn, exactly where the same things would be refused inside a plain struct — the rule is on the reference page.

Note the import. This module’s yield_now is the thread’s — a hint to the system that answers a bool — and the task’s yield_now is a form the compiler supplies, so the module’s declaration is the nearer name wherever the module is imported whole; awaiting it is refused, the refusal naming sysl.threads.yield_now as what shadowed the task form. A file that runs tasks imports what it uses from here by name, as the program above imports spawn.

What a task changes is where interleaving can happen. Two tasks driven by one executor run on one thread and never at the same instant, so they cannot race on a plain var — but each await is a point where the task stops and others run, so state read before an await may have changed after it. A thread has the opposite pair of properties: no stopping point is written down, and anything it shares is shared at every instruction. Blocking stays honest on both sides — a thread that waits is a thread that waits, and a task that waits says so with await at the place it does.

There is no task runtime in this module or anywhere in the standard library. The compiler supplies block_on and the executor contract; an event loop that drives many tasks is a package — kairos for a microcontroller, with its async face planned, and one over libuv planned for a host.

How strong this is

Honestly weaker than Rust or Swift 6, and worth saying plainly rather than implying a guarantee the language cannot keep.

This module is where the first row stops being theoretical. spawn is declared @crossing(arg), so the pointer it takes is looked through and a state whose counts are not all atomic is refused where the call is written. That is also why this API takes an address rather than a value: a spawn taking a T would be claiming the copying half of the crossing rule, which belongs to a channel and is still not written — Channel[T] above assigns a slot rather than copying, so it refuses a view exactly as spawn does.

The unchecked half of that row is where the annotation is absent. A facility with no @crossing on it is a boundary the compiler was never told about, and there is no way to guess one: a scheduler in a package looks like any other function until somebody writes the line.

So a data race requires you to have shared something on purpose. Sharing takes &sync or *T, both of which are greppable and neither of which is what an ordinary value is. What remains permanent is the race you can write by putting a mutable field in a &sync T, because it is the cost of not having a borrow checker.

Next: sysl.args — how argc and argv become a []string, and the two layers that read options out of them.