Concurrency
Toka provides lightweight concurrency through tasks and message passing, enabling efficient parallel execution.
Tasks
Spawn concurrent tasks with the task module:
import std/io::println
import std/thread::thread_spawn
fn worker(id: i32) -> i32 {
println("Worker {} started", id)
// Do work...
println("Worker {} done", id)
return 0
}
fn main() -> i32 {
auto t1# = thread_spawn<i32>({ => return cede worker(1) })
auto t2# = thread_spawn<i32>({ => return cede worker(2) })
t1#.join()
t2#.join()
return 0
}
MPSC Channels
Communicate between tasks using MPSC (Multi-Producer, Single-Consumer) channels:
import std/channel::channel
import std/thread::thread_spawn
import std/io::println
fn main() -> i32 {
auto pair# = channel<i32>()
auto tx# = cede pair.tx
auto rx# = cede pair.rx
thread_spawn<i32>({ [cede tx] =>
tx#.send(cede 42)
return cede 0
})
thread_spawn<i32>({ [cede rx] =>
auto res_opt = rx#.recv()
println("Got a message!")
return cede 0
})
return 0
}
Async Functions and Cancellation
An asynchronous function declares its result with -> async T. Its .await points are allowed only inside an async function and preserve PAL ownership and borrow facts across suspension. Use .await? when cancellation must be handled as an explicit Option<T> result; ordinary .await propagates cancellation rather than manufacturing a value.
Task and thread handoff is stricter than an ordinary call: it cannot carry a hidden borrow, str, bytes, raw pointer, or captured outer resource. Move an owned shape across the boundary only through a cede parameter and an explicit cede argument.
Atomic Operations
Use atomic types for lock-free concurrent access:
import std/atomic::*
fn main() -> i32 {
auto counter = AtomicI32::new(0)
counter.fetch_add(1, Ordering::SeqCst)
return 0
}
Mutex / Sync
For shared mutable state:
import std/sync::Mutex
fn main() -> i32 {
auto lock# = Mutex<i32>::new(0:i32)
auto g = lock#.lock().unwrap()
// Access shared data safely
// g released automatically when it goes out of scope
return 0
}
Safety Guarantees
Toka's concurrency model prevents:
- Data races: Two tasks cannot simultaneously write to the same memory
- Bounded ownership handoff: A task or thread cannot silently retain a borrowed or moved resource
- Send/Sync violations: Types that are not thread-safe cannot be shared across tasks
Toka does not claim to prove the absence of every application-level deadlock; cancellation policy, lock scope, and protocol ordering remain part of the program's design.