Every concurrency bug you have ever debugged started the same way: something was still running when you thought it had stopped.

A thread outlives the function that created it and touches a local that is gone. A future is never awaited and its failure is never seen. A worker keeps a pointer to a buffer the caller has already reused. In each case the language handed you a handle and, with it, an obligation — join this, await that, cancel the other — and the bug is what happens when a single exit path forgets.

Mica does not hand you a handle. It gives you a block, and the block is the lifetime.

The example is examples/Tasks. Build and run it:

make -C mica-container/examples/Tasks run

Keep that one file open. Everything below happens in it, and the “try it” moments are changes you make to it.

A block that cannot leak a task

Here is the whole of Mica’s task syntax. A task declaration looks like a procedure, schedule makes one ready, and concurrent is the block they live in:

concurrent
    schedule Worker(1, 1);
    schedule Worker(2, 1);
    WriteLn("  parent: both workers are ready, neither has run");
end;

WriteLn("  parent: past the end, so both have finished");

Which prints:

  parent: both workers are ready, neither has run
  worker 1: step 0
  worker 2: step 0
  parent: past the end, so both have finished

Two things in that output are the whole design.

schedule does not run anything. The parent keeps going and prints its own line first. Scheduling makes a task ready; it does not transfer control. That is why the parent’s line comes out before either worker’s, even though both schedule statements ran before it.

The end joins. The last line is proof: reaching it means both workers have finished. Not “probably finished” — the end of a concurrent block is a join over every task started inside it, and the compiler plants that join on every path out of the block. A leave, a return, a failure travelling up the failure channel: each one drains the scope on its way past.

There is no handle to forget, because there is no handle. schedule yields nothing you could store, and a task has no name outside the block. Try to schedule one anywhere else and the compiler stops you:

analyzer error 5327: 'schedule Worker' must stand inside a 'concurrent' block:
the block's 'end' is where the tasks it schedules are joined, so a schedule
outside one would start work no 'end' waits for — wrap it in 'concurrent … end'

That refusal is what makes the join total. If a task could be started outside a block, some block would have to be responsible for a task it never saw.

Arguments are snapshots

The second rule removes the second classic bug: the worker that reads a variable the parent has since changed.

cell := 10;

concurrent
    schedule Snapshot(cell);
    cell := 20;
    schedule Snapshot(cell);
    cell := 99;
end;

WriteLn("  the cell itself now holds: %lld", cell);
  captured: 10
  captured: 20
  the cell itself now holds: 99

Both tasks ran after the parent had already written 99. They printed 10 and 20 anyway, because schedule copied its arguments at the moment it ran. An argument is a value the task owns. It is not a window onto the parent’s variable, and no amount of scheduling delay can make it become one.

This falls out of Mica’s value model: parameters are values, values are copied, and there are no hidden references anywhere in the language. Concurrency does not need a special rule here — it inherits the ordinary one.

The copy is the whole value, whatever it holds. A record with a name and a list of scores crosses the same way a number does:

type
    Scores = array of int64;
    Player = record
        name   : string;
        scores : Scores;
    end;
task Report(who : Player);
var
    total, at : int64;
begin
    total := 0;

    for at := 0 to Length(who.scores) - 1 do
        total := total + who.scores[at];

    WriteLn("  %ls scored %lld in %lld rounds", who.name, total, Length(who.scores));
end;

In a program that imports WriteLn, Length and Append from std and declares player : Player, the body hands the record to a task and changes its own copy while the task runs:

player.name := "Ada";
player.scores := new Scores reserve 0;
Append(address player.scores, 12);
Append(address player.scores, 30);

concurrent
    schedule Report(player);

    player.name := "Grace";
    player.scores[0] := 0;
    Append(address player.scores, 99);
end;

WriteLn("  the variable now holds %ls with %lld rounds", player.name, Length(player.scores));
  Ada scored 42 in 2 rounds
  the variable now holds Grace with 3 rounds

The task receives its own copy of the text and of the array, made at schedule in memory the task owns and released when the task ends, so the parent is free to rename, grow and overwrite its variable the moment the schedule returns. A task placed on a process receives the same copy: the request that starts it carries the text and the arrays with the value. What cannot cross is a pointer, because it names memory the task could not own; the compiler refuses it and names the field that holds it.

Try it. Change Snapshot to take no parameter and read cell directly. The compiler will refuse it, and the message names the exact discipline that replaces the snapshot — that refusal is the subject of data-race freedom.

One carrier, and the turns it takes

Mica’s tasks are stackful and cooperative. Each one gets a real stack, so a task body is an ordinary body — no async colour, no rewriting a function because it might suspend. And by default the whole program runs on one carrier: one operating-system thread, running one task at a time.

Tasks change hands at suspension points. Yield is the explicit one:

while i < steps do
begin
    WriteLn("  worker %lld: step %lld", tag, i);
    i := i + 1;
    Yield();
end;

Schedule three steps against two and the ready queue rotates in scheduling order:

  worker 1: step 0
  worker 2: step 0
  worker 1: step 1
  worker 2: step 1
  worker 1: step 2

Strict alternation until the shorter worker runs out, then the longer one finishes alone. That ordering is not a lucky run — it is what a first-in, first-out ready queue on one carrier must produce, and it is identical at every optimization level and on both x86-64 and ARM64.

Yield is not the only suspension point, and in real programs it is rarely the interesting one. A task that reads from a descriptor that has nothing to give leaves the ready queue too, and the carrier picks up someone else; readiness puts it back. That is the subject of its own page — tasks and blocking I/O — and the reason a cooperative scheduler is not the trap it sounds like. What you must not do is compute for a long time with no suspension point at all, which is the busy-loop problem.

The tree is the call tree

A concurrent block belongs to the activation it stands in. That single sentence is Mica’s whole structure of concurrency, and it is worth taking slowly.

procedure Prepare();

    task Step(tag : int64);
    begin
        WriteLn("  prepare: step %lld begins", tag);
        Yield();
        WriteLn("  prepare: step %lld ends", tag);
    end;

begin
    concurrent
        schedule Step(1);
        schedule Step(2);
    end;
end;

Calling Prepare() from the program’s main body prints:

  prepare: step 1 begins
  prepare: step 2 begins
  prepare: step 1 ends
  prepare: step 2 ends
  back in the program, after Prepare joined its own scope

Prepare owns a scope of its own and joins it before it returns. The caller does not know that scope exists, and does not need to: a procedure that starts tasks is, from the outside, just a procedure that takes a while.

So concurrency nests because activations nest. A second scope comes from a second activation, never from a second block in the same one. The task tree and the call tree are the same tree, which is why a Mica program’s concurrency has a shape you can read off the source rather than reconstruct from a debugger.

This is the idea the Erlang and Kotlin communities call structured concurrency. What is different here is that it is not a library convention you can opt out of. There is no unstructured form to fall back to.

Leaving early cancels — and the cleanup still runs

The join is total on every path, including the paths that leave early. What changes on an early exit is not whether children are waited for, but whether they are asked to stop first:

concurrent
    schedule Chatter();
    schedule Winder();

    leave when cancel;
end;

Run that with cancel false and both tasks run to their natural ends. Run it with cancel true and the scope cancels on the way out. Here are both, from the same two tasks:

Reaching the end: nothing is cancelled
  chatter: before the suspension point
  winder: completed 3 of 3 rounds
  winder: cleanup
  chatter: after the suspension point
  chatter: cleanup

Leaving early: the scope cancels, the cleanup still runs
  chatter: before the suspension point
  winder: completed 0 of 3 rounds
  winder: cleanup
  chatter: cleanup

Read the two blocks against each other and three separate facts come out.

Cancellation is delivered at a suspension point. Chatter prints its first line in both runs — a cancelled task is not killed where it stands. It keeps running until it reaches a point where it would suspend, and there the cancellation arrives as a leave it cannot decline:

task Chatter();
begin
    defer WriteLn("  chatter: cleanup");

    WriteLn("  chatter: before the suspension point");
    Yield();
    WriteLn("  chatter: after the suspension point");     { the uncancelled run only }
end;

Yield is only the plainest of these points. Every call that waits is one: a read or an accept on something that is not ready yet, and Sleep. A task cancelled while it sleeps leaves at the sleep, exactly as a task cancelled in a read leaves at the read.

Cleanup is not optional. chatter: cleanup appears in both runs. A cancelled task unwinds like any other early exit, so defer runs, heap obligations are discharged, and a task that opened something closes it. There is no “cancelled” path that skips your cleanup, because cancellation is an exit path and Mica has only one kind.

A task that computes decides for itself. Winder never suspends. It polls instead:

while (n < 3) and not TaskCancelled() do
    n := n + 1;

WriteLn("  winder: completed %lld of 3 rounds", n);

TaskCancelled is a plain read of the running task’s cancel state. Because Winder reaches no suspension point, nothing unwinds it, and it publishes its partial result — 0 of 3 in the cancelled run, 3 of 3 in the other — and returns normally. That is the difference the two mechanisms are for: suspension points give you cancellation for free, and the poll gives you cancellation you can shape when free is not what you want.

Try it. Put a Yield() inside Winder’s loop and run it again. It stops being a task that decides and becomes a task that is unwound: completed … rounds disappears from the cancelled run, and only the cleanup line remains.

A task from another unit

A library or an object may export a task, and a program that imports it schedules it exactly as it schedules its own. The body runs as the library compiled it, and it reaches the library’s variables the way every routine of the library does, under the library’s own marks:

library Workers;

var
    total : int64;

exp task Add(tag : int64);
begin
    synchronized total := total + tag;
end;

exp function Total() : int64;
begin
    Total := total;
end;

begin
end.
program Sums;

imp
    WriteLn : std;
    Add, Total : Workers;

var
    k : int64;

begin
    concurrent
        for k := 1 to 10 do
            schedule Add(k);
    end;

    WriteLn("total %lld", Total());
end.

Saved as Workers.mica and Sums.mica beside a project file that states the library’s version, mica.project:

{ "version": "1.0.0", "sources": ["Workers.mica"] }

the library builds once into an archive with its contract, and the program builds against that contract:

mica --compile --link --output-modifier archive --emit-contract --project mica.project --source Workers.mica --build build/workers
mica --compile --link --external-contract build/workers/mica.external --source Sums.mica --build build
./build/Sums
total 55

The program’s block joins the ten tasks, and a failure the task declares comes back to that block’s on fail section in the library’s exported domain. A task is still never called: Add(3) outside a schedule is refused, because a task yields no value and runs under its block’s join.

What this does not do

An honest list, because a concurrency model’s limits matter more than its features.

There is no detached task. No spawn that outlives its creator, no daemon, no task you hand to a scheduler and forget. If you want work to continue, some activation on the stack has to still be inside the block that owns it. This is a real constraint, and it is the price of the join being total.

A task returns nothing. task declarations take parameters and yield no value. Results come back through what a task writes — under the discipline of data-race freedom — or through a stream, which is the next article. A failure is different: a task that fails propagates on the failure channel and cancels its siblings, which the section below and the error-handling material cover.

One section per failure domain

A concurrent block may schedule failing tasks of several domains, and it consumes each in a section of its own. The declared error type of a section’s binding selects the section, so nothing new is spelled:

var
    parseFailure : ParseError;
    fetchFailure : NetError;

begin
    concurrent
        schedule Parse(document);
        schedule Fetch(host);
    on fail parseFailure do
        WriteLn("parse failed %lld", Ord(parseFailure));
    on fail fetchFailure do
        WriteLn("fetch failed %lld", Ord(fetchFailure))
    end;
end;

The first failure wins. It cancels the other tasks of the block, and its section runs after the join. A failure a cancelled task would have reported afterwards is a consequence of that cancel and is dropped, so exactly one section of a block ever runs. Swift’s task groups and Kotlin’s coroutineScope rule the same way; Python’s ExceptionGroup keeps every failure instead, a road Mica did not take, because the failure that caused the cancel is the one that explains the block.

Three rules follow, and the compiler holds you to each of them:

  • every domain the block’s tasks fail is consumed — by its own section, by on fail continue (which discards every domain no section names, and stands last), or by forwarding, when the enclosing activation itself fails that domain;
  • no two sections name one domain, and no section names a domain no task of the block fails;
  • a section whose statement is a call ends it with a semicolon, because a clause behind a call binds that call — the same innermost-first reading a clause behind a loop body has. Without the semicolon the next section’s on fail lands on that call, and the refusal says so.

Ordering is guaranteed by the carrier count, not by the language. Everything you saw above is deterministic because this program runs on one carrier. Build the same source with --tasking multicore,2 and the results stay correct while the interleaving stops being predictable. Which output determinism you are entitled to, and which you are not, is the carriers article.

Cancellation is cooperative, not preemptive. A task with neither a suspension point nor a TaskCancelled poll runs until it finishes. There is one exception — the back-edge safepoint that lets a deadline stop a genuine busy loop — and that, too, is the carriers article.

What the compiler proved

You did not write a join, and no exit path could skip one. You did not write a handle, so no handle could leak. You did not write cleanup twice — once for the normal path and once for the cancelled one — because there is only one kind of exit. And the ordering you saw is the ordering the machine must produce, on both architectures, at every tier.

What Mica takes from you here is the freedom to start work nobody is waiting for. What it gives back is that “is anything still running?” stops being a question you can get wrong.

Next

Generators and streams — the other thing a stackful suspension buys you: a body that produces values one at a time and suspends between them, consumed by an ordinary for-in loop.

Tasks on processes — the same schedule, one word apart: a task in a worker process of its own, which shares nothing with the program and ends alone when it traps.