Very safe
Many bugs follow patterns. Nikaia checks for those patterns before they reach your users, and says where it cannot.
Five kinds of mistake, each with the problem, what Nikaia checks and where the check stops. Every one has a page with the whole program and the message the compiler gives.
Conflicting actions
Two tasks that change the same balance at once can overwrite each other's update. Nikaia looks at what each task touches when the program is built, and refuses two tasks that change the same value or both write to standard output, naming what they share. The way out is in the message: a value of its own for each task, a SharedMut changed through update, or the two changes in order.
Where the compiler cannot tell what a call touches, as in a Rust crate or a C library that starts its own threads, it does not refuse, so this is not a proof that every race is found. The example uses today's overlap; the specification writes it with async before an expression, which is being built (#983).
overlap {
balance = balance + 50
balance = balance - 30
}error[NK2104]: These two branches can't run at the same time.
note: Both change `balance`.Tasks that get stuck
Sometimes tasks wait for each other forever. A task that pauses while it holds a lock is rejected, since everyone who needs that value would wait too. For several locks at once, update_all takes them in one fixed order, so two transfers cannot hold one each and wait for the other.
Nikaia does not yet reject a lock taken inside another lock when you write it by hand, so using update_all for several locks is up to you. And not every possible deadlock can be ruled out in every situation; where the analysis cannot decide, it does not claim the problem is solved.
a.update fn(mut acc) {
acc.balance -= 30
time::sleep(5.millis())
}error: `time::sleep` can pause, but you're holding a lock here.A memory budget for every task
A single runaway task can use up all the memory and bring down the whole program, including the parts that were working fine. In most languages nothing stands in its way. Erlang and Elixir are known for isolating work in this way, and Nikaia is specified to do the same.
In the specification every task gets a memory budget of its own. A task that spends it ends on its own, and the rest of the program, your main application included, runs on. A shared value has a budget of its own too. This is decided and written into the specification. A calculation that runs while the program is built is already bounded in steps and in memory.
The per-task budget is not built yet, and today a task that takes too much memory can still take it from the whole program. Once built, it is a protection while the program runs, not a proof: Nikaia will not show at build time that a task stays within its budget, it makes sure that a task which does not ends with task::OverBudget, an error like any other, and only that task ends. Memory that a Rust crate or a C library allocates and keeps for itself is in no budget.
Decided and specified, not built yet: today a task can still take memory from the whole program.
Errors that go unhandled
When something fails, the program needs a way to deal with it. Functions declare when they can fail, and what they can fail with is worked out from their bodies. A function that calls something that can fail, and neither declares it nor handles it, is rejected when the program is built. Tasks are held to the same rule. A task’s error is thrown where the program waits for the task, at h.join() or at the end of an overlap, and the compiler asks for it to be handled there as for any call that can fail. A task handle that is never joined, cancelled or detached is refused (NK2109), so the error has a place to arrive.
For functions from outside Nikaia that nothing describes, Nikaia cannot know every way they fail. A description of the library closes that gap. The check shows where failures are not accounted for; it does not make the handling itself correct.
fn load() -> String {
return fs::read_to_string("config.txt", fs::Root::Anywhere)
}error: This function can fail, because `fs::read_to_string` can fail.Broken promises
Every part of a program should be able to rely on what the other parts promise.
What Nikaia checks. You write the expectation as an assert and it becomes a contract. A call that breaks it is rejected when the program is built, a promise about a result is available to the callers, and a contract carries across package boundaries.
The limit. A compiler cannot know whether data from files, arguments or the network is valid. Check it where it enters the program; once checked, the rest of the code can rely on it.
fn percent(n: int) -> int {
assert(n >= 0 && n <= 100)
return n
}
percent(140)error: This call breaks `percent`'s precondition `n >= 0 && n <= 100` every time it is reached.