Overture

A synchronous data-flow language with dependently typed clocks, implemented as a standalone compiler written in, and heavily inspired by, ATS2/Postiats. Overture grows out of Dependent Types for Multi-Rate Flows in Synchronous Programming (Blair & Xi, ML/OCaml 2015), which encoded Prelude's clock calculus in ATS. Prelude observed that implementing multi-rate data-flows in traditional synchronous languages was often a tedius and error prone process without any formal checks provided by the underlying typesystem. In Prelude, individual data-flows are assigned their own clock, and the typechecker confirms that clocks meet the specification required by nodes that consume the clocks. In the ML/OCaml 2015 paper, we showed that multi-rate clocks could be expressed using dependent types in ATS. We defined an interface for representing operators within the dependent type system, and compiled Prelude programs to ATS programs that used this interface. This discharged typechecking to ATS, but it still didn't reveal a dependently typed interface to the real-time system programmer; the more expressive type system was concealed within an internal phase of the Prelude compiler.

In this work, we extend the representation of multi-rate data-flows in ATS' type system into a standalone programming language. In contrast to Prelude, data-flows have proper dependent types, and operators and combinators can be implemented using quantifier over clocks. To cite this work, please use the following paper:

@inproceedings{Blair:17,
  author    = {William Blair and
               Hongwei Xi},
  title     = {Dependent Types for Multi-Rate Flows in Synchronous Programming},
  booktitle = {Proceedings {ML} Family / OCaml Users and Developers Workshops, {ML}
               Family/OCaml 2015},
  series    = {{EPTCS}},
  volume    = {241},
  pages     = {36--44},
  year      = {2017},
  url       = {https://doi.org/10.4204/EPTCS.241.3},
  location  = {Vancouver, Canada}
}

As a disclaimer, this implementation was primarily authored by Claude's Fable 5 model using our ML/OCaml 2015 paper and the ATS2 sources as input, along with prompts that outlined the proposed language and major design decisions. While Claude has demonstrated proficiency in writing ATS source code, the code can be cleaned up over time. In addition, the implementation has not been heavily tested beyond the small programs that were presented in the paper and generated during development. As a result, using programs generated by Overture should be done with caution. However, it is interesting that the AI managed to take the pragmatic approach to programming in ATS that many beginner programmers do not. That is, the AI quickly abandoned starting with dependently typed code and instead used the ML style data-structures for the initial implementation. In practice, we have found this "gradual typing" approach to be helpful in using ATS productively.

In Overture, every program term is a data-flow: an infinite stream of values, with each produced at an integer date. The language offers no direct computation — it only composes nodes between sensors and actuators. When compiled to a real system, sensor nodes correspond to functions that read values from hardware, for example from an analog to digital converter (ADC) and actuators apply outputs to physical devices, for example a digital to analog converter (DAC). Each strictly periodic flow carries a clock (n, p) where n : int is the period and p : rat the phase offset, valid when the activation date n * p is a natural number.

Example Overture Program

The following example program reads temperature from a sensor, obtains a command from a controller and submits the command to a database to yield a possible alert. Individual temperature values are produced ten times more often than alerts are expected, and the Overture program below effectively allows a controller to act on every tenth reading of a temperature sensor. While other approaches exist (e.g., applying some filter to all the temperature's values), Overture's type system guarantees that one temperature value will be read for every possible alert output, which is produced every 100 ticks. Note that the use of dependent types in sampling generally applies to sampling from a source that is ten times faster than the rate of the actuator. That is, other sensor/actuator pairs with different rates could be passed to the sampling node, provided the actuator was 10 times slower than the sensor.

sensor temp : rate(int, (10, 0));
actuator alert : rate(int, (100, 0));

extern node controller {c: clock}
  (i : rate(int, c), j : rate(int, c))
  returns (o : rate(int, c), p : rate(int, c));

extern node database {c: clock}
  (i : rate(int, c)) returns (o : rate(int, c));

node sampling {c: clock}
  (i : rate(int, c)) returns (o : rate(int, c * 10))
  var command : rate(int, c * 10);
  var response : rate(int, c);
let
  (o, command) = controller(i /^ 10, (0 fby response) /^ 10);
  response = database(command *^ 10);
tel

alert = sampling(temp);

Node bodies are unordered systems of equations: response is read (under a fby) before its defining equation. The universal quantifier {c: clock} makes sampling polymorphic over every clock; the typechecker proves each obligation with a built-in linear integer solver. Here they all discharge arithmetically — note that command *^ 10 oversamples a flow whose period is already 10 * period(c), so its divisibility obligation holds for any c. A node that oversamples its input, by contrast, genuinely constrains the clocks it accepts, and must say so in its quantifier:

node upsample {c: clock | 4 | period(c)}
  (i : rate(int, c)) returns (o : rate(int, c / 4))
let
  o = i *^ 4;
tel

Omit the guard and the unsatisfied obligation is reported in surface syntax:

error: unsolved constraint: guard of [*^]
  needed: (4 | period(c))
  hypotheses: true

Quantifiers may equivalently be written with literal UTF-8, as in Lean — an editor can insert them:

node upsample ∀ c: clock ∣ 4 | period(c).
  (i : rate(int, c)) returns (o : rate(int, c / 4))

Existential quantifiers describe node outputs. For an extern node the guard must determine the witness (the solver checks that any two clocks satisfying the guard are equal): the implementation's chosen output clock has to be computable at compile time, since it becomes a task-table entry during code generation. Implemented nodes may declare looser existentials — their witness is in the body.

node delay3 {c: clock}
  (i : rate(int, c))
  returns (o : [q: clock | period(q) == period(c)
                        && date(q) == date(c) + 3 * period(c)]
                 rate(int, q))
let
  o = shift(i, 3);
tel

The Clock Calculus

Clock transformations are static functions of sort clock, applied with infix operators (fixity comes from declarations, defaults built in). Sampling a flow and transforming a clock are different operations and spell differently: term-level *^//^ resample a flow, while on clocks the result is written as plain arithmetic on the period -- oversampling divides the clock, undersampling multiplies it:

operator	result type	clock	guard
f *^ k (oversample)	rate(a, c / k)	(n/k, p*k)	k > 0 && k | period(c)
f /^ k (undersample)	rate(a, c * k)	(n*k, p/k)	k > 0
shift(f, k), k : rat	rate(a, shift(c, k))	(n, p+k)	isint(k * period(c))
v fby f	unchanged
cons(v, f) / tail(f)		phase −1 / +1	date(c) >= period(c) for cons
merge(b, f, g)		common clock
f when b	rate(gated, a, c) at the common clock
current(v, bf)	rate(gated, a, c) back to rate(a, c)

Guards may also use the projections period(c) and date(c) and the relations == != < <= > >= | (divides) && ||.

The fundamental flow type is rate(k, a, c), where the kind index k classifies the flow: strict for strictly periodic flows and gated for boolean-gated ones (the paper's BFlow). The two- argument form rate(a, c) is sugar for rate(strict, a, c), so the common case never mentions kinds. f when b gates a flow by a boolean flow at the same clock, yielding rate(gated, a, c): values appear only on the subset of c's dates where the gate was true.

Because presence is data-dependent while clocks are static, gated flows are terminal in the clock calculus: every clock operator's signature demands the strict kind, so resampling a gated flow is rejected with a kind mismatch. Kind indices are compared structurally during matching (they have no arithmetic, so syntactic comparison is complete) and never reach the solver. Nodes may quantify over kinds — {k: kind} — to pass either flavor through. Quantifier groups may sit on either side of the node name; the position is stylistic (template-flavored axes like kinds and payload types read naturally on the left, DML statics on the right), the semantics identical — variables are classified by sort, and guards from any group are conjoined:

node {k: kind} {a: type} pass {c: clock}
  (i : rate(k, a, c)) returns (o : rate(k, a, c))

Gated flows are eliminated by actuators declared rate(gated, ...) (actuation skips absent ticks) or by current(v, bf), which holds the last present value (v initializes). In generated code a gated flow is a pair of cells (value, presence bit); the static clock still bounds the dates, so the task table is unchanged — presence only decides whether the slot does anything. Extern nodes may not yet carry gated flows in their interfaces (the presence bit awaits an ABI convention).

Extern nodes may declare a worst-case execution time as a static integer expression over their quantifiers, in the spirit of Prelude's wcet:

extern node reader {c: clock; k: int | k > 0 && 2 * k <= period(c)}
  (i : rate(int, c)) returns (o : rate(int, c))
  wcet 2 * k;

The typing rule is the per-flow necessary condition of the synchronous hypothesis, discharged at the declaration site: under the node's guard, wcet <= period(c) must hold for every clock in its interface — so the guard is forced to bound the admissible periods, and every instantiation inherits the proof. The value lands in the --emit-graph task table alongside period and offset; whole-system schedulability (interference, utilization) remains the downstream RTOS analysis's job, but the compiler emits that problem completely.

Internally the solver lowers every clock to the integer pair (period, activation date d = n*p): validity is structural rather than a constraint, clock * and / leave dates invariant, and every operator stays linear — which is what keeps Fourier–Motzkin elimination applicable. Obligations are checked by refuting hypotheses ∧ ¬goal (Gaussian elimination, integer-tightened FM); divisibility and integrality goals substitute unit-coefficient equalities and check residual coefficients.

Units of Time

Overture deliberately fixes no physical time unit. Following the ML/OCaml 2015 paper — which requires only that every date be an integer — all temporal quantities live on one shared abstract integer timeline whose unit we call a tick:

• in ticks: periods, activation dates (n * p), shift distances (n * k), wcet declarations, the date t passed to sensors and actuators, and the tick-count argument of generated programs;
• dimensionless: phase offsets (a fraction of the period) and the sampling factors of *^ and /^ (ratios between rates).

The typechecker never interprets the unit, and every judgement is invariant under a global rescaling of it: multiplying all literal periods and wcets by a constant changes no constraint's truth. What one tick means — a millisecond, a microsecond, a bus minor frame — is a deployment decision, made where generated code meets a real timer: the emitted harness advances t in logical time only, and pacing step(t) against hardware is the runtime's job (see below). The one obligation this convention creates is consistency: a program's sensors, actuators, and wcet declarations must all be written against the same intended unit, since wcet <= period(c) compares them directly.

Schedulability

Schedulability for generated Overture programs is obtained in two stages, by two type systems, split along a precise line: Overture's typechecker proves every per-task property, and the generated program's own compilation proves the whole-system one.

Stage one — Overture's typechecker proves the task set is well-posed:

• every flow's clock relations hold (logical synchrony: values from different-rate flows meet at the dates the clocks say);
• every instance has a definite ground period, offset, and wcet after monomorphization;
• the per-task necessary condition wcet <= period(c), per declaration, under its guard.

What it deliberately does not prove is the whole-system sufficient condition. Two nodes of wcet 6 at period 10 each pass their own check and are jointly infeasible on one processor (utilization 1.2): interference between tasks sharing a processor is a property of the sum, and the general arithmetic (utilization bounds, response-time fixed points) is nonlinear — outside the linear constraint domain Overture's solver decides.

Stage two — the schedule certificate. For the ATS backend, that global condition is discharged when the generated program is compiled. Codegen emits overture_sched.sats/.dats and constructs the_schedule in the harness through a budget-indexed builder whose types demand, slot by slot, that the work released in each base-tick slot fits within it — exactly the timing model of the sequential step(t) executive. Every period, offset, and wcet is a ground literal after monomorphization, so patsopt decides each obligation while compiling the harness. The result: a generated program that builds is schedulable (under its wcet claims, on the cyclic executive it ships with), and an infeasible task set is a program that does not build — the two-wcet 6 example above is refused by patsopt at the offending slot_add, where 6 <= 10 - 6 has no solution.

The remaining honesty, so the guarantee is read correctly:

• the slot-capacity test is sufficient but conservative — a set feasible under preemptive scheduling may be refused;
• the C backend ships the same task table as plain data (overture_tasks[]) with no certificate; feasibility for C deployments must come from the ATS artifact (compile it as the certificate for the same numbers) or an external analysis;
• acceptance is conditional on the wcet declarations being true: they are claims about hand-written C, and only runtime budget enforcement can police them;
• the unpaced logical-time harness meets the synchronous hypothesis by construction (time is suspended during step(t)); the certificate is about what happens once a deployment paces ticks against a real timer.

Building and Running

The compiler is written in ATS2 and built with the vendored toolchain (expected at ATS2-Postiats-int-0.4.2/, configured by src/Makefile via PATSHOME):

make            # builds src/overture
make test       # runs tests/run_tests.sh (pos/ must pass, neg/ must fail as specified)

overture [--typecheck] file.ovt      # default mode
overture --dump-tokens file.ovt      # lexer output
overture --dump-ast file.ovt         # parse tree after fixity resolution
overture --dump-ast2 file.ovt        # resolved, sort-checked program
overture --emit-graph file.ovt       # clock-erased dataflow graph (JSON)

Code Generation

overture --codegen file.ovt monomorphizes the program from its top-level equations inward (every reachable node instance gets ground statics, exactly as the typechecker inferred them) and writes two ATS2 files, compiled to native code by patscc:

overture --codegen=ats tests/pos/sampling.ovt
patscc -DATS_MEMALLOC_LIBC -o sampling \
  sampling_gen.dats sampling_stubs.dats overture_sched.dats
./sampling 320
[t=0] alert = 0
[t=100] alert = 101
...

*_gen.dats is the harness: one value cell per flow, a step function firing each action when its ground clock (n, d) says so (t >= d && (t - d) mod n == 0), and a main loop over logical base ticks (gcd of the periods). Clock operators compile to their value-level residue: *^//^ are latest-value copies (dates are invariant), shift/tail are ring-buffered delay lines of depth s/n + 1 (the calculus requires value-preserving delays: fby(x, f) = cons(x, shift(f, 1)) fails with re-sampling registers), fby is one-slot delayed state, cons a same-instant copy with an initial value, merge a conditional copy.

*_stubs.dats holds deterministic default implementations (sensors return the date; actuators print; extern nodes sum their inputs) — replace it for real IO. That file boundary is where the thin OS for real hardware will plug in, and it is also where ticks acquire a physical unit: a real runtime paces each step(t) against a timer at whatever duration per tick the deployment chose, leaving every compile-time judgement unchanged. Pacing makes deadlines real; for the ATS backend, the schedule certificate guarantees they are met — a generated program that builds is schedulable on its own executive, under its wcet claims (see the Schedulability section above). Existential output clocks are computed from their pinned guards; wcet values and the task set (period, offset per instance) are fully ground after monomorphization.

The Dataflow Graph

--emit-graph also remains available as a machine-readable summary: it dumps sensors, actuators, per-node equations, and a topological order of each node's flows in which the stream inputs of fby/cons are non-strict; a cycle through strict edges yields an instantaneous- loop warning (full causality analysis is future work).

Compiler Pipeline

The compiler phases for Overture mirror ATS2's own (src/overture_*):

1. lexing — byte-oriented; the only multibyte sequences accepted are ∀, ∃, ∣; these symbolic operators simplify reasoning about the statics.
2. parsing — recursive descent; expressions as operand/operator item lists resolved by precedence climbing against the fixity table (infixl/infixr/prefix declarations take effect immediately)
3. typechecking — scope resolution, sort checking, type translation; equations checked as a set with exactly-once definedness 3.1 trans3 — application instantiation, guard obligations, existential opening/witnessing, clock-equality goals, collected into c3nstr trees 3.2 solving — the linear integer solver above
4. erasure — the JSON dataflow graph
5. codegen - compiling to executable code

Statics follow pats_staexp2's shape: no per-operation constructors; clock operators, arithmetic, relations, and projections are built-in static constants applied via S2Eapp, with sort-based overload resolution (int <= rat).

Status and Future Work

• ATS/C code generation against an RTOS runtime (consuming the graph)
• full causality analysis
• rational-valued static variables in the solver (literal rationals are fully supported; symbolic ones are rejected as nonlinear)
• user-declared static constants and richer payload types
• gated flows on extern node interfaces (a presence-bit ABI)

License

Licensed under the GNU General Public License, version 3 or later, matching ATS2/Postiats; see LICENSE.