Mica 7.7.5 lets a program written in C train a model through a Mica library: an exported routine opens a tape window of its own, walks the tape back and reads its gradients, so a C product calls a routine that learns on the device it runs on. A value always belongs to its type, on every tier, wherever it comes from. Tasks, generators and processes keep one set of rules: workers share the program’s streams, a select waits on them, and a lost worker costs only the value it held. The ownership checks hold one cell to one owner on every path, a cell read out of a slot stays that slot’s, and an array element is followed by its index. A library routine’s allocations are narrated at their own line and column, in the library’s own file.

Beside them, a library writes its own C header, a C host’s threads call a Mica library at the same time, elemental routines apply one body to every element of a vector, a matrix or a tensor, a routine’s heading gives its parameters defaults, everyday words such as value and file are names, and --sanitize thread runs a multicore program under the thread sanitizer.

A C program trains through a Mica library

A tape window stands in the body of any routine now, an exported one included, with Backward and Gradient after it in the same body. A library exports a routine that learns, and a C program calls it like any other function:

{
    Learn - a library whose exported routine learns: it records a curve on a tape window of its own and reads the slope.

    'Slope' records x² + 3x on a window in its own body, walks the tape back and answers the gradient, so a C program
    that calls it reads the derivative 2x + 3 at the point it names and never sees the tape.
}
library Learn;

imp
    Backward, Gradient : std;

const
    { the coefficient of the curve's linear term }
    Linear = 3.0;

{ The slope of x² + 3x at 'x' is recorded and walked by the routine's own window. }
exp function Slope(x : float64) : float64;
var
    p, y : tracked float64;
begin
    p := x;
    tape
        y := p * p + Linear * p;
    end;
    Backward(y);
    Slope := Gradient(p);
end;

begin
end.

--emit-header writes Learn.h beside the archive, and the C program includes it instead of declaring the library by hand:

#include <stdio.h>

#include "Learn.h"

int main(void)
{
    Learn__init();
    printf("slope at 1.5: %.2f\n", Learn__Slope(1.5));
    printf("slope at -2.0: %.2f\n", Learn__Slope(-2.0));
    return 0;
}

The library is built from a mica.project that states its version, and the build names the runtime floor the C program links beside it:

mica --compile --link --output-modifier archive --optimize O2 \
  --platform linux,arm64,utf-32 --project mica.project \
  --source Learn.mica --build build --emit-header
cc -o learn main.c -Ibuild build/Learn.a /usr/lib/mica-stdlib-arm64.a /usr/lib/mica-dragon-rt-arm64.a -lm -lpthread
./learn

It prints, on AArch64 and on x86-64 alike:

slope at 1.5: 6.00
slope at -2.0: -1.00

The header declares every export under its exact linkage name, every type those exports use, every exported constant as a typed macro and each parameter’s default in a comment. Each prototype states its thread safety in the GNU C Library’s words, so the header of Learn says what training touches:

/** MT-Unsafe race:tape */
double Learn__Slope(double x);

Every library now defines Learn__init, its body’s entry, which a C program calls once before its first call into the library. The library’s routines read and write its tracked variables when C calls them, and its body counts with for. A routine that opens a window is refused by name wherever a second window could open while it records: inside another window, in a task, a generator, a callback or a concurrent block.

On the multicore runtime, every C thread that calls into a library becomes a task of its own on its first call, with its own failure record and returned texts, and a library’s synchronized statements always take their locks. A library is exactly as thread-safe as its own marks, like any C library. A multicore build serves the callbacks a C library keeps and fires later from threads of its own, and a C host whose library places work on processes calls <Library>__init_processes once, early in main. A C program that links a Mica library into a shared object of its own can unload it with dlclose and exit cleanly.

A value always belongs to its type

{
    Months - converts three numbers into a month, the last of them past the month's range.

    A month is a subrange of 1 to 12, so the conversion of 13 into it stops the program with the reason and the place,
    at every tier: the optimizing tiers keep the check, since they read every value of the type as a month.
}
program Months;

imp
    WriteLn : std;

const
    MonthLine = "month %lld";
    First = 11;
    Last = 13;

type
    { A month is numbered from 1 to 12. }
    Month = 1..12;

var
    number : int64;
    month : Month;

begin
    for number := First to Last do
    begin
        month := number as Month;
        WriteLn(MonthLine, month as int64);
    end;
end.

It prints, at the debug tier and at O2, on both processors:

month 11
month 12
Mica runtime failure: reason=ordinal_out_of_domain (20), token_stream_index=49
Mica runtime context: file=Months.mica, line=28, column=25
Mica runtime source:         month := number as Month;

An as into a subrange, Chr, and Succ, Pred, Inc and Dec at a range’s edge stop at the conversion on every tier, where only a checked build stopped. So does a value of a subrange, an enumeration, bool or unicode that a C routine answers, writes through an address or hands to an exported routine or a callback, and one that a read through a pointer to C memory or a bit record field meets. A C contract states which pointer parameters its C may fill, and the contract --emit-contract writes for a Mica library states it for every export.

Because the value is always a member of its type, optimized builds read the declared range as a proof: table[month] over an array[Month] reads its element with no bounds check, and a case that names every value of its selector keeps no stop behind its arms.

One cell, one owner, on every path

{
    HandedOnce - hands a cell to an owning parameter on one path and releases it after the paths meet.

    A call through an owning parameter hands the cell's release to the callee, so on the path that calls 'Take' the
    dispose after the 'if' would release the cell a second time, and the compiler refuses that dispose where it stands.
}
program HandedOnce;

type
    { A node is the cell the routine owns. }
    Node = record
        weight : int64;
    end;

{ The routine takes the node through an owning parameter and releases it. }
procedure Take(taken : owning pointer Node);
begin
    dispose taken;
end;

{ The one arm of the 'if' hands the node over, and the dispose after the arms meet releases it again on that path. }
procedure OneArm(flag : bool);
var
    node : pointer Node;
begin
    node := new Node;
    if flag then
        Take(node);
    dispose node;
end;

begin
    OneArm(True);
end.

7.7.5 refuses it at the release:

obligation error 13113 [29,5]: heap cell is disposed again after it was already released on some path reaching here — the call to 'Take' at line 28 took the cell allocated at line 26 through an owning parameter on a path reaching here, which hands its release to the callee on that path; release the cell on the other paths before they meet, or give the variable a new cell after that call

7.7.4 compiled it, and the program stopped as it ran, with free(): double free detected in tcache 2.

A cell handed to an owning parameter, disposed, stored into an owning field or appended to an array on only some of the paths that reach a later release is refused there, and so is a loop body that does so on its next turn. A cell read out of an owning slot stays that slot’s until a store through the same name and path clears it, and a cell read out of an array element stays that element’s until a store through the same index clears it, so releasing the cell read, or storing it into a second owner, is refused wherever two names may be one place or an index may name the element.

A record whose fields own cells moves whole into an owning place, item : owning Entry, and a generic routine’s owning V and borrowed V work over any type parameter, so a map’s Get answers a borrowed view of the cell it holds. dispose releases a record or an array a routine holds as a whole, and a dynamic array of owning pointers, or of records holding them, owns the cells stored into it. The memory narration names the allocations of a library’s generic routine at their own line and column of the library’s file.

What this proves is the owning side, at compile time: a cell has one owner, a hand-over happens once, and a release happens on every path. A borrowed pointer is a view of a cell another name owns. A checked build stops a read through a borrowed pointer whose cell was released, and the known limitations say how far the compile-time checks follow one; following every borrowed pointer to its owner is the next release’s work.

Tasks, generators and processes share one set of rules

{
    SharedRing - three worker processes and a carrier task share one ring, each value reaching exactly one of them.

    Each reader placed on a process asks the program for every value its loop pulls, and the ring hands each value to
    one reader only, the carrier reader among them. One producer emits in order, so every reader takes an increasing
    run of the ring, the end of the stream reaches every worker, and nothing is left behind them.
}
program SharedRing;

imp
    WriteLn : std;

const
    Values = 1000;
    RingSlots = 8;
    DisorderLine = "a reader took %lld values out of order";
    LostLine = "a reader was lost";
    LeftLine = "values left behind the readers: %lld";

var
    ring : stream of int64;
    v : int64;
    remaining : int64;

{ The generator emits the numbers from 1 to 'n' in order. }
generator Counted(n : int64) : stream of int64;
var
    k : int64;
begin
    for k := 1 to n do
        emit k;
end;

{ A reader counts the values that arrive out of the producer's order, which one producer makes none. }
task Reader(s : stream of int64);
var
    v : int64;
    previous : int64;
    disorder : int64;
begin
    for v in s do
    begin
        if v <= previous then
            disorder := disorder + 1;
        previous := v;
    end;
    WriteLn(DisorderLine, disorder);
end;

begin
    ring := schedule Counted(Values) buffer RingSlots;

    { three workers and a carrier task pop the same ring }
    concurrent
        schedule Reader(ring) on process;
        schedule Reader(ring) on process;
        schedule Reader(ring) on process;
        schedule Reader(ring);
    on lost do
        WriteLn(LostLine);
    end;

    for v in ring do
        remaining := remaining + 1;
    WriteLn(LeftLine, remaining);
end.

It prints, at every tier on both processors:

a reader took 0 values out of order
a reader took 0 values out of order
a reader took 0 values out of order
a reader took 0 values out of order
values left behind the readers: 0

A task placed on a process reads a stream of the program one value per ask, so workers and carrier tasks share one ring. Its elements may hold text, dynamic arrays and descriptors, and a stream that fails ends the worker’s loop with the failure. A select waits on a stream a worker feeds, with an on lost arm for it, and a lost reader costs only the value it held, which on lost held do names, in the order the losses happened. Several stages may pull one ring opened with schedule ... buffer. Tasks on processes that wait on each other with too few workers stop with a report that names the remedy.

A concurrent block’s child starts right away on the carrier that schedules it, so the stacks standing at once grow with a fork-join tree’s depth, not its breadth: a tree of 131,071 tasks runs to its end. A synchronized mark holds around every statement it can stand before, a name lookup parks only its own task, every descriptor the runtime opens is close-on-exec, and a program holds one timer for all of its sleeping tasks and deadlines.

Elemental routines, defaults and everyday names

{
    Steps - applies one routine written for a single value to every element of a vector and of a matrix.

    'Clip' is declared elemental, so a call hands it a whole vector or matrix and answers one of the same shape, and a
    single bound beside it serves every element. Its bounds have defaults in its heading, so the call over the vector
    leaves them out and the call over the matrix names the narrower ones it wants. The vector is called 'value', an
    everyday word that is a name like any other.
}
program Steps;

imp
    WriteLn : std;
    Min, Max : math;

const
    VectorLine = "vector %.2lf %.2lf %.2lf";
    MatrixLine = "matrix %.2lf %.2lf %.2lf %.2lf";
    Lowest = 0.0;
    Highest = 1.0;
    Half = 0.5;

var
    value, clipped : vector[3] of float64;
    grid, kept : matrix[2, 2] of float64;

{ The clip of one value keeps it between two bounds, the unit interval unless the call names others. }
elemental function Clip(x : float64, low : float64 := Lowest, high : float64 := Highest) : float64;
begin
    Clip := Min(Max(x, low), high);
end;

begin
    value := (-0.5, 0.25, 1.75);
    clipped := Clip(value);
    WriteLn(VectorLine, clipped[0], clipped[1], clipped[2]);

    grid := ((-1.0, 0.25), (0.75, 2.0));
    kept := Clip(grid, Lowest, Half);
    WriteLn(MatrixLine, kept[0, 0], kept[0, 1], kept[1, 0], kept[1, 1]);
end.

It prints, at every tier on both processors:

vector 0.00 0.25 1.00
matrix 0.00 0.25 0.50 0.50

A function declared elemental is written for a single value and applies to every element of a vector, a matrix or a tensor, and a single value beside them conforms to every shape. A program’s own elemental routine takes extents known only at run time, records on the tape as whole-tensor verbs so Backward and Gradient give its derivative at every element, and runs over tensors held on a GPU. The math unit’s elementwise verbs are elemental routines under one name for every shape: Tanh(m) is written where a program wrote TanhMap(m).

A parameter may state a constant default of every type a constant can have, and a call may leave out the trailing parameters that have one, an elemental call over a vector or a matrix too, as Clip(value) does. A library’s contract carries the defaults to its importers, and the editor’s signature help shows them. A variable, field, parameter, constant or type may be called value, address, file, set, object, library, new or with, since these words read by their position: value p still reads through a pointer. A chained comparison, a < b < c, draws one refusal that writes the two comparisons it means.

A template’s value parameter has the type its gen block declares in every specialization, binds every number that type holds, and binds a named constant exactly as the number it holds. A refusal a generic routine raises only because of a call’s type arguments stands at that call, and a generic routine may do to a type parameter only what its constraint promises.

Smaller programs, sanitizers and debugging

{
    Deep - descends without a floor until its stack runs out.

    'Descend' calls itself with no case that stops it, so the program's stack runs out, and the report names the routine
    whose frame overflowed and the line of its heading.
}
program Deep;

imp
    WriteLn : std;

const
    DepthLine = "depth %lld";
    Start = 1;

{ The descent goes one level deeper on every call and never comes back. }
function Descend(depth : int64) : int64;
begin
    Descend := Descend(depth + 1) + 1;
end;

begin
    WriteLn(DepthLine, Descend(Start));
end.

It stops, at the debug tier and at O2, on both processors:

Mica runtime failure: reason=stack_overflow (21), token_stream_index=18
Mica runtime context: file=Deep.mica, line=17, column=10
Mica runtime source: function Descend(depth : int64) : int64;

A stack overflow names the routine whose frame overflowed and the line of its heading, on every tier, and a large frame touches every page it spans as it is taken, so an overflow always reaches the guard. A breakpoint on a routine’s own name stops in it, break Descend in gdb and a function breakpoint in the editor, and backtraces name each frame that way.

Every program and every task hold 24 KiB less zeroed memory for their result marks, every program 8 KiB less for its cell registry, and a program built without debug information 184 KiB less zeroed data; every thread holds 48 KiB less resident memory. A multicore program shares one C allocator arena, and each carrier after the first reserves 7.75 MiB less stack. mica --inspect names the address space a program image maps and its initialized and zeroed data, Mica’s own apart from the C library’s.

At the optimizing tiers an integer constant is the immediate of the instruction that reads it, an if whose arms fold away leaves no test behind, an array whose lower bound lies far from zero is rebased by one instruction on AArch64, and a small zeroed heap cell is cleared by its own few stores.

On x86-64 the same tiers’ float code no longer waits for instructions it does not depend on: a conversion from an integer, a conversion between float widths and a square root start at once, and a float copy between registers writes the whole register. SpectralNorm, which had slowed since 7.7.0, runs faster than in 7.6.5 again.

--sanitize thread links a multicore program against the GNU C compiler’s thread sanitizer and the runtime floor built under it, and the first race it finds names both accesses with their C files and lines. mica --run takes --sanitize and --platform, so a script runs checked, or for the other architecture under its user-mode emulator. The program generator now judges every program under the thread, address and undefined-behavior sanitizers beside the four tiers on both processors.

Upgrading

Things a 7.7.4 build meets differently in 7.7.5:

  • A conversion into a subrange, an enumeration, bool or a unicode scalar that falls outside its type stops with ordinal_out_of_domain on every tier, where only a checked build stopped, and so does such a value entering from C.
  • A call into a library whose contract an earlier compiler wrote checks every pointer it hands over and warns once (5700): regenerate the contract with --emit-contract.
  • A cell handed over, disposed or stored on only some of the paths reaching a later release is refused there (13113), and a cell read out of a slot or an array element and then released or stored into a second owner is refused (13106, 13109).
  • A C host calls <Library>__init once before its first call into a library. A library and the program or C host that links it agree on --tasking, or the link stops, naming the library or the floor’s marker. On the single-carrier runtime a callback a C library fires on another thread is refused at its entry.
  • Backward or Gradient in a body that opens no window before it is refused at compile time, where it stopped the program as it ran.
  • A generic routine may do only what its constraint promises: x + 1 under T is ordered is refused, and a for bound of a type parameter’s type needs ordinal. A template’s value parameter N : int64 mixes with a float64 only through a written conversion, mu / (C as float64).
  • [1] for a set of Day, and 1 in work, are refused (5060, 5115), where the number was read as the member it counts.
  • The children of a concurrent block start right away and have no order, so output that several children print may come in a different order than before.
  • One frame may hold up to 8,347,648 bytes on the default stack, where a frame just under the stack’s size compiled and then died.
  • Dragon SDK: the runtime floor contract moves to version 7, and dragon_floor_check takes a new argument, parking, after multicore. Rebuild a floor of your own against this release before you link it.

The packages and the commands that install them are on the install page.