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 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:

'schedule Worker' must stand inside a 'concurrent' block

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.

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 same idea the Erlang and Kotlin communities call structured concurrency, and that C++ is still arguing about. 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;

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.

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 error-handling material covers.

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.