Systems · View as Markdown

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(move 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 {
    let mut total: i64 = 0 as i64;
    let mut 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 manual marker. The impl must carry unsafe, because the compiler is taking your word for it:

struct Handle { opaque ptr: *u8 }

unsafe impl Send for Handle {}
unsafe impl Sync for Handle {}

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

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

Arc, Mutex, and Channel already carry the right conditional impls, so you rarely write these by hand outside of FFI wrappers. A Send or Sync impl that omits unsafe is E0860; unsafe on any other impl is E0861.

Atomics

For the rare cases that cannot partition:

import "stdlib/atomic" as atomic;

let p: *u64 = unsafe { ... };       // pointer to a shared u64
unsafe {
    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
{
    let mut g = m.lock();
    g.set(g.get() +% 1);
}                                 // the guard's Drop releases