Threads and atomics

import "stdlib/thread" as thread;

fn worker() -> i32 { return 42; }

fn main() -> i32 {
    let h: thread::JoinHandle[i32] = thread::spawn::[i32](worker);
    return h.join();
}

For runnable proof recipes, see Threads and atomics. It documents the checked parallel_sum partition-and-join recipe and the concurrent_counter atomic shared-counter recipe from the C+ source tree.

Passing data into the worker

For non-Copy input, use spawn_with, which moves the value into the thread:

import "stdlib/text" as text;

fn proc(take s: text::Text) -> i32 { return s.len() as i32; }

let s = "hello".to_text();   // an owned Text
let h = thread::spawn_with::[text::Text, i32](s, proc);
let n = h.join();

Text is Send, so it is a valid spawn_with payload.

The safe pattern: partition and join

This is the first pattern to reach for. Race-freedom is mechanical, because there is no shared memory:

struct Range { start: i64, end: i64 }

fn sum_range(r: Range) -> i64 {
    var total: i64 = 0 as i64;
    var i: i64 = r.start;
    while i < r.end { total = total +% i; i = i +% (1 as i64); }
    return total;
}

let h1 = thread::spawn_with::[Range, i64](left,  sum_range);
let h2 = thread::spawn_with::[Range, i64](right, sum_range);
let total: i64 = h1.join() +% h2.join();

Note that Rc[T] is !Send and is rejected at spawn; share across threads with Arc[T]. See Real-time for the Send / Sync rules (E0502).

Send and Sync

Send means a value can move to another thread; Sync means it can be shared across threads. Both are enforced structurally. A nominal type that transitively hides a raw pointer is !Send and !Sync by default, so moving or sharing it across a Send / Sync bound (such as thread::spawn) is rejected with E0502. A bare *T used directly stays Send; the default applies to types that wrap one.

When you have audited a type and know it is safe to send or share, vouch for it with a hand-written marker impl. The act of writing the impl the compiler would not auto-derive is the assertion, so the body must stay empty:

struct Handle { opaque _ptr: *u8 }

impl Handle: Send {}
impl Handle: Sync {}

The conditional, generic form carries its requirement as bounds, so the marker holds only when the element type also qualifies:

impl Arc[T: Send + Sync]: Send {}

Arc, Mutex, and Channel already carry the right conditional impls, so you rarely write these by hand outside of FFI wrappers. A Send / Sync marker impl's body must stay empty (E0860 if it does not). An empty impl of Eq / Ord / Hash / Clone / ToText is no longer an error: it derives the memberwise implementation. Any other interface still needs a body unless every method it declares has a default.

Scoped threads: lend a local

spawn / spawn_with move their data into the worker. A scope lends it instead, and joins every worker before the loan ends:

import "stdlib/thread" as thread;
import "stdlib/status" as status;

struct Counts { hits: i32 }

fn tally(ref data: Counts) {
    data.hits = data.hits +% 1;
    return;
}

fn run() -> i32 {
    var counts: Counts = Counts { hits: 0 };
    {
        var s: thread::Scope = thread::scope();
        let rc: status::Status = s.lend::[Counts](counts, tally);
        assert rc == status::Status::Ok;
    }
    return counts.hits;
}

Scope::lend is #[keeps(this)] on a ref parameter, so the borrow checker knows the scope holds the loan for the rest of the scope's life. Scope::drop joins every worker it started, on every path out. There is no finish() you could forget.

Three mistakes are compile errors, not races:

• the lent value dying while the scope lives (E0514)
• a write into it while a worker holds it (E0381)
• lending the same place twice (E0381)

lend returns Status::OutOfMemory if the cell cannot be allocated or the OS refuses the thread; in either case nothing was started. Workers write back through the lent value. A thread that must return a value is still spawn / spawn_with.

Atomics

For the rare cases that cannot partition:

import "stdlib/atomic" as atomic;

let p: *u64 = ...;       // pointer to a shared u64
atomic::atomic_fetch_add_u64(p, 1 as u64, atomic::Ordering::Relaxed);

Ordering values: Relaxed, Acquire, Release, AcqRel, SeqCst. Widths: i32 / i64 / u32 / u64.

Mutex

The mutex is internally refcounted, so a clone shares it across threads (C+ has no &T to make Arc[Mutex[T]] work):

import "stdlib/mutex" as mutex;

let m = mutex::new::[i32](10);
let m2 = m.clone();              // share across threads
{
    var g = m.lock();
    g.set(g.get() +% 1);
}                                 // the guard's Drop releases

Two guards in the same scope deadlock: the borrow checker does not yet prevent this, so use block scopes to bound each guard's lifetime.