Паралелізм без data race
Parallelism дозволений тоді, коли compiler може довести сумісність effect sets і memory regions.
Axiom не намагається знайти race у runtime. Він забороняє ordinary conflicting concurrent access ще до генерації коду.
Паралельна обробка незалежних частин
1normalize(view<f32> samples):2 parallel for usize i = 0; i < samples.size(); i = i + 1:3 samples[i] = clamp(samples[i], -1.0, 1.0)Mutable view на audio/data buffer.
parallel for вимагає proof independence між ітераціями.
Кожна ітерація читає/пише лише samples[i]. Якщо analyzer доводить, що різні i — disjoint elements, loop законний.
Scoped task borrow
1process(view<u8> left, view<u8> right):2 require disjoint(left, right)3 const task a = spawn filter(left)4 const task b = spawn filter(right)5 await a6 await bПередумова доводить, що mutable regions не перекриваються.
Task отримує scoped mutable borrow left.
Другий task — right.
Після await mutable permission повертається parent scope.
Structured concurrency не дозволяє child пережити borrowed memory.
Shared mutable state
Звичайний mutable object не можна просто дати двом tasks. Для спільного стану існують semantic synchronization types: atomic<T>, mutex<T>, channel<T>. Lock тимчасово видає exclusive mutable permission.
Memory order
Atomic operations за замовчуванням мають sequential semantics. Слабші порядки — relaxed, acquire, release, acquire_release — задаються явно. Семантично безглузде load(release) є compile-time error.