Dependent Types for Multi-Rate Flows in Synchronous Programming

TL;DR

This paper demonstrates how dependent types in ATS can be used to verify real-time primitives in a synchronous programming language, enabling advanced static checking through automatic code generation.

Contribution

It introduces a method to encode real-time primitives in Prelude using ATS's dependent and linear types, and modifies the Prelude compiler for automatic ATS code generation.

Findings

Verification of real-time primitives via dependent types in ATS

Automatic generation of ATS code from Prelude source

Enhanced static checking capabilities in synchronous programming

Abstract

Synchronous programming languages emerged in the 1980s as tools for implementing reactive systems, which interact with events from physical environments and often must do so under strict timing constraints. In this report, we encode inside ATS various real-time primitives in an experimental synchronous language called Prelude, where ATS is a statically typed language with an ML-like functional core that supports both dependent types (of DML-style) and linear types. We show that the verification requirements imposed on these primitives can be formally expressed in terms of dependent types in ATS. Moreover, we modify the Prelude compiler to automatically generate ATS code from Prelude source. This modified compiler allows us to solely rely on typechecking in ATS to discharge proof obligations originating from the need to typecheck Prelude code. Whereas ATS is typically used as a general purpose programming language, we hereby demonstrate that it can also be conveniently used to support some forms of advanced static checking in languages equipped with less expressive types.

Equations

$$\exists n\in {\mathbb{N}}^{+}.\forall i\in \mathbb{N}.t_{i+1}-t_i=n$$

$$\forall i\in \mathbb{N}.(v_i,t_i)\in F$$

$$\begin{array}[]{rcl}$\mbox{\tt cons}$&:&\forall a:\mbox{\it type}\,\forall n:\mbox{\it int}\,\forall p:\mbox{\it rat}.~{}(a,\mbox{\bf SFlow}(a,n,p))\rightarrow\mbox{\bf SFlow}(a,n,p-1)\\ \end{array}$$

$$\begin{array}[]{rcl}$\mbox{\tt tail}$&:&\forall a:\mbox{\it type}\,\forall n:\mbox{\it int}\,\forall p:\mbox{\it rat}.~{}\mbox{\bf SFlow}(a,n,p)\rightarrow\mbox{\bf SFlow}(a,n,p+1)\\ \end{array}$$

$$\begin{array}[]{rcl}\mbox{\tt mul}&\kern-3.0pt:\kern-3.0pt&\forall a:\mbox{\it type}\,\forall n:\mbox{\it int}\,\forall p:\mbox{\it rat}\,\forall k:\mbox{\it nat}.~{}(k\mid n)\supset(\mbox{\bf SFlow}(a,n,p),\textbf{int}(k))\rightarrow\mbox{\bf SFlow}(a,n/k,p\cdot k)\\ \mbox{\tt div}&\kern-3.0pt:\kern-3.0pt&\forall a:\mbox{\it type}\,\forall n:\mbox{\it int}\,\forall p:\mbox{\it rat}\,\forall k:\mbox{\it nat}.~{}(k\mid n)\supset(\mbox{\bf SFlow}(a,n,p),\mbox{\bf int}(k))\rightarrow\mbox{\bf SFlow}(a,n\cdot k,p/k)\\ \mbox{\tt shift}&\kern-3.0pt:\kern-3.0pt&\forall a:\mbox{\it type}\,\forall n:\mbox{\it int}\,\forall p:\mbox{\it rat}\,\forall k:\mbox{\it rat}.~{}(n\cdot k\in\mathbb{N})\supset\ (\mbox{\bf SFlow}(a,n,p),\textbf{rat}(k))\rightarrow\mbox{\bf SFlow}(a,n,p+k)\\ \mbox{\tt fby}&\kern-3.0pt:\kern-3.0pt&\forall a:\mbox{\it type}\,\forall n:\mbox{\it int}\,\forall p:\mbox{\it rat}.~{}(a,\mbox{\bf SFlow}(a,n,p))\rightarrow\mbox{\bf SFlow}(a,n,p)\\ \end{array}$$

$$\forall a:\text{mbox}type\forall n:\text{mbox}int\forall p:\text{mbox}rat.(\text{mbox}\mathbf{SFlow}(\text{mbox}\mathbf{bool},n,p),\text{mbox}\mathbf{SFlow}(a,n,p),\text{mbox}\mathbf{SFlow}(a,n,p))\to \text{mbox}\mathbf{SFlow}(a,n,p)$$

$$\forall a:\text{mbox}type\forall n:\text{mbox}int\forall p:\text{mbox}rat.(\text{mbox}\mathbf{SFlow}(\text{mbox}\mathbf{bool},n,p),\text{mbox}\mathbf{SFlow}(a,n,p))\to \text{mbox}\mathbf{BFlow}(a,n,p)$$

$$\forall a:\text{mbox}type\forall n:\text{mbox}int\forall p:\text{mbox}rat\forall k:\text{mbox}int.(k>0)\supset (\text{mbox}\mathbf{SFlow}(a,n,p),\text{mbox}\mathbf{int}(k))\to \text{mbox}\mathbf{SFlow}(array(a,k),n\cdot k,p/k)$$

Full text

1 Introduction

Building software that must work reliably is an undeniably challenging process. Yet, engineers can still construct reliable real-time systems that operate under strict temporal requirements. Companies have long adopted model-based methods for designing real-time software[2]. Model-based design methods emphasize automatically generating code from high-level models that formally describe the behavior of a system. In fact, synchronous programming languages helped start a movement towards this paradigm (of model-based automatic code generation) when they were introduced in the 1980s.

In synchronous programs, tasks communicate through data flows with the assumption that each data flow produces values instantaneously at every step of a global logical clock. However, the simplicity of a single system-wide global logical clock can be the source of serious limitation in practice. If a system consists of communicating periodic tasks that need to run at different rates, the global logical clock can become an obstacle as the programmer must synchronize all the tasks manually. The process of manual synchronization is likely to be both tedious and error-prone with little support provided by the compiler for preventing subtle timing bugs. As a part of his PhD thesis, Julien Forget developed Prelude[7], a synchronous language that features primitives for describing the real-time behavior of tasks in a multi-rate periodic system. Synchronizing data flows with different clocks in Prelude is still left to the programmer, but the language provides operators to directly modify real-time clocks. For example, a programmer can stretch a clock to accomplish under-sampling or shrink it for over-sampling. The typechecker of Prelude then automatically verifies that all communicating tasks are synchronized. The advantage of this system is that the language offers the ability to easily adjust the temporal behavior of tasks while providing support for verification in the type system.

In this report, we encode inside ATS the clock calculus presented in Prelude, where ATS is a statically typed programming language with a functional core of ML-style. The type system of ATS is rooted in the Applied Type System framework[12], which gives the language its name. In ATS, both dependent types[14, 13] (of DML-style) and linear types are supported. We assign dependent types to the real-time clocks available in Prelude and then develop functions to capture the behavior of clock transformation operators. With these functions, we can typecheck the automatically generated ATS code from Prelude source (by a modified Prelude compiler) and formally verify that the data flows in the original Prelude source are properly synchronized. A running version of our modified compiler can be found online111An end-to-end demonstration of our system is available at https://travis-ci.org/wdblair/overture.

Although ATS is typically used as a source programming language, we hereby demonstrate that it can also be conveniently used as a target language for the purpose of supporting advanced static checking in a host language equipped with less expressive types. In addition, the reported use of dependent types for reasoning about temporal properties should be interesting in its own regard.

2 Multi-Rate Flows in Prelude

An embedded real-time system continuously interacts with its own environment and often must do so under strict timing constraints. For example, a task may periodically sample a sensor and provide data that can in turn be used by the application logic to adjust the output of an actuator. In order to guarantee that the system is responsive, engineers need to demonstrate that the worst case execution time (WCET) for the communication from the sensor, to the application logic, and then to the actuator can never exceed a required deadline. Synchronous programming languages simplify development by abstracting time for the designer and providing well-defined semantics to enable verification and automatic code generation from a model of the system.

When a synchronous program is compiled, all of the nodes and flows are translated into a single-step function that is invoked repeatedly. The time between steps is the period of the system, and the Synchronous Hypothesis states that all the flows must be re-evaluated before the end of each step. It is up to the system designer to ensure that this requirement is met. Several synchronous languages[3, 4] have been developed since the 1980s, with Lustre[5] currently serving as the underlying language powering the SCADE Suite developed by Esterel Systems.

This abstraction for time in a synchronous language is of great convenience because it not only alleviates the need for the programmer to worry about low-level timing details but also produces fully deterministic code. However, it makes it difficult at the same time to compose systems where tasks may run at different rates. In order to make tasks execute at the desired rates, the programmer must essentially schedule tasks by hand in terms of a global logical clock, which can be both tedious and error-prone.

Prelude addresses the problem of manual synchronization for multi-rate periodic systems by removing the notion of a single system-wide global clock. Instead, it assigns each periodic flow $F$ its own clock $C$ represented as a pair $(n,p)$ where $n\in\mathbb{N}^{+}$ (that is, $n$ is a positive integer) and $p\in\mathbb{Q}^{+}$ (that is, $p$ is a positive rational number); the integer $n$ is referred to as the period of $C$ and $p$ the phase offset. Note that the period of a flow $F$ is just the inter-arrival time of values produced by $F$ and the phase offset is the initial delay of the flow. The activation time of a flow (that is, its start date) is given by $n\cdot p$. In Prelude’s clock calculus, every date (that is, a point in time in the program) is required to be an integer so as to simplify schedulability analysis. Therefore, we need to ensure that the date $t_{0}$ is an integer for every flow. In other words, a clock defined as $(n,p)$ is valid if and only if both $n\in\mathbb{N}^{+}$ and $n\cdot p\in\mathbb{N}^{+}$ hold.

In Prelude, a generic flow consists of an infinite list of tuples $\forall i\in\mathbb{N}.~{}(v_{i},t_{i})$, where $v_{i}$ is the value of the flow produced at time $t_{i}$. Under the normal synchronous paradigm, every flow produces some value during each tick of the logical clock. There is no longer the notion of a global time scale in Prelude. Instead, every flow is assigned its own clock, which can be lengthened as well as shortened. By modifying a clock, we alter the rate at which values are produced in a program. If a value contained in a flow is undefined for some arbitrary date, we cannot adjust its real-time behavior while expecting deterministic results. As such, it is useful to define a class of data flows that are strictly periodic. Formally speaking, a data flow is strictly periodic if and only if

[TABLE]

where $n$ is the period of the clock assigned to the flow and $t_{i}$ is the date when value $i$ is produced by the flow[7]. Intuitively, a strictly periodic data flow produces a value after each period. In Prelude, a set of operators are provided to transform the clocks assigned to strictly periodic flows which greatly facilitates communication between tasks that execute at different rates. In Figure 2 presented in Section 1 we describe how to encode the semantics of these operators into the ATS programming language.

As an example, let us consider a simple system where a controller runs with a clock of $(100,0)$ and interacts with a fast running task that provides critical data from the environment with a clock of $(10,0)$. Figure 1 implements this system where the controller node sends a command to the database node and receives a response back from it. Observe that the controller executes 10 times slower than the database. If we want the controller node’s output command to be synchronized with the database, we must over-sample it using the *^} operator. Likewise, we under-sample the \textbfdatabase node’s output response in order to synchronize it with the controller node by using the /^} operator. In the rest of the paper, we will define the Prelude operators necessary to implement this program in ATS so that all synchronization constraints are checked by the type checker. Then, we will describe how we can transform Prelude programs like this one into ATS to verify all communication is synchronized. \section% Assigning Types to Flows in ATS

At a high level, Prelude modifies the semantics of traditional synchronous languages by refining the basic flow type to have its own clock as opposed to a global clock. This refinement generates a proof obligation for the compiler as a flow going from one task to another is not necessarily synchronized. We can readily defer this obligation to typechecking in ATS by assigning the following type (written in the concrete syntax of ATS) to strictly periodic flows:

⬇

abstype SFlow(a: type, n: int, p: rat)

Note that int and rat refer to the sorts for integers and rational numbers, respectively. There is another sort nat for natural numbers that will appear later. Given $a$, $n$, and $p$, the type $\mbox{\bf SFlow}(a,n,p)$ is for a strictly periodic flow of values of the type $a$ such that the clock assigned to the flow is of the period $n$ and phase offset $p$. Formally speaking, a flow $F$ of the type $\mbox{\bf SFlow}(a,n,p)$ consists of the following pairs:

[TABLE]

where each $v_{i}$ is a (defined) value of the type $a$ and $t_{i}=n\cdot(p+i)$. Flows that are not strictly periodic are also useful in Prelude. For instance, the following type BFlow is for boolean flows:

⬇

abstype BFlow(a: type, n: int, p: rat)

Boolean flows differ from strictly periodic flows by allowing values to be produced only on a subset of the dates given by a flow’s clock. In Figure 2, we define a boolean flow alert} to give the value of a temperature sensor only at dates when \mintinlinepreludefault produces a true} value. \beginfigure

⬇

node

monitor (temperature: int rate (10, 0), fault: bool rate(100, 0))

returns (alert: int rate (100, 0))

let

alert = (temperature /^ 10) when fault

tel

The boolean flow given here produces data only when produces .

Modifying a flow’s clock affects the values that are included in the flow. In order to determine precisely what values remain in a flow after its clock is modified, Prelude requires that every flow passed to a clock transformation operator be strictly periodic. By the same token, all clock operators yield strictly periodic flows. In Prelude, only integer dates are considered valid. Therefore, any flow’s clock is subject to the requirement that $n\cdot p\in\mathbb{N}$ holds, where $n$ and $p$ are the period and phase offset of the clock, respectively. If this was not true, then a task’s start time could not be represented as an integer date. When assigning types to a clock transformation operator, we often add a precondition to ensure that only a clock satisfying the requirement can be actually returned by the operator.

The clock transformation operators in Prelude are to be translated into regular functions in ATS. Synchronous flows resemble infinite lazy streams in traditional functional programming languages. For instance, we can introduce an operator cons of the following type:

[TABLE]

Basically, cons adds a given value to the beginning of a given flow to form a new flow that starts one period ahead of the given flow; the first produced value of the new flow is simply the given value, and the rest are those produced by the given flow. As another example, we can introduce an operator tail of the following type:

[TABLE]

Given a flow, tail returns another one that simply delays the given flow’s activation by one period.

There are four commonly used clock transformation operators in Figure 2 plus the types assigned to them. The mul operator (that is, *^ in Prelude) speeds up a clock by shrinking its period; it implements over-sampling where every element in the flow is repeated $k$ times to meet its timing constraint. Likewise, the div operator (that is, /^ in Prelude) slows a clock by stretching its period; it implements under-sampling where only one element is taken out of every $k$ elements of the input flow. Given a flow and a rational number $k$, the shift operator shifts the phase offset of the clock assigned to the flow by $k$, thus delaying the activation of the flow. Given an element and a flow, the fby operator does not modify the flow’s clock at all; it instead simply shifts the flow by one period and sets the first element of the flow with the given one. For instance, fby can be implemented based on cons and shift in the concrete syntax of ATS as follows:

⬇

implement fby (x, f) = cons(x, shift(f, 1))

Another interesting operator merge is given the following type:

[TABLE]

where bool is the type for booleans. Essentially, merge takes three strictly periodic flows and returns one; for each $i$, if the value in the first flow at $t_{i}$ is true, then the value in the second flow at $t_{i}$ is picked to be the value of the returned flow at $t_{i}$; otherwise, the value in the third flow at $t_{i}$ is picked. Yet another interesting operator when is given the following type:

[TABLE]

where BFlow is for boolean flows. Given two strictly periodic flows, when returns a boolean flow; for each $i$, if the value of the first flow is true at $t_{i}$, then the value of the second flow at $t_{i}$ is picked to be the value of the returned flow at $t_{i}$; otherwise, the returned flow is undefined at $t_{i}$. Note that when is so far the only operator that does not return a strictly periodic flow. So far we have only thought of communication through flows in Prelude as individual values arriving at dates (that is, points in time). Please recall the simple example presented in Figure 1, where a controller queries a faster data task for information. In order to make the communication between them synchronous, we specified that only one out of every 10 values produced by the faster task is to be read by the controller.

Suppose that the controller needs all values produced by the database since it was last invoked. This requires a queuing mechanism in the clock calculus, which is a feature outlined in Prelude’s specification but yet to be supported by the compiler. We can readily add verification support for this feature with dependent types in ATS. Suppose we have a strictly periodic flow $F$ that we want to under-sample by some factor $k$. We can think of the flow as having values of the type $array(a:type,k:int)$ for arrays that each contain $k$ elements of the type $a$. This gives us the following type for a divide operation that performs queuing rather than under-sampling. In this way, every time the node that consumes this flow is activated, it has access to all $k$ of the most recent values emitted from the flow. Putting this formally, the type for such an operator is as follows:

[TABLE]

Clearly, this type directly relates the number of accumulated values produced by a given flow to the factor by which the flow’s clock is expected to be stretched.

3 Using ATS as a Target Language

With the above outlined operators plus their types, we can write ATS programs that correspond semantically to their Prelude counterparts in terms of the synchronization checks that must be performed. In this work, we modified the Prelude compiler to automatically generate ATS code with type signatures from Prelude source. As we will see in this section, the translation is largely straightforward. Every imported node is declared as an external function with their input and output flows having the same clock, and every node that is actually implemented in Prelude is translated into a function definition in ATS. Probably the biggest issue is to bridge the semantic gap between Prelude, a concurrent declarative language, and ATS, a call-by-value language with an ML-like functional core. This is especially evident when we translate programs where certain flows are passed as arguments before they are actually defined. For instance, please take a careful look at the code presented in Figure 1. This issue cannot be addressed by simply reordering expressions as circular definitions are both legal and common in Prelude. Instead, we address this issue by using a combination of linear types and support for proof terms in ATS. For each locally declared flow, we generate a linear proof term. In order to consume this proof term, we specify a proof function our Prelude compiler must call with two ATS flows that have equal clocks to ensure the Prelude flow they represent is given exactly one clock. In Figure 3 you can see this approach used to verify the response} and \mintinlinepreludecommand flows maintain their specified clock.

After modifying the Prelude compiler, we automatically generate ATS code directly from the abstract syntax tree of Prelude source; potential synchronization errors in the Prelude source can be captured by typechecking the ATS code translated from it. For instance, the Prelude example in Figure 1 is translated into the ATS program in Figure 3 for the purpose of typechecking. Note that the lines starting with the keyword prval are theorem-proving code related to the circularly defined flows in this function.

4 Conclusion and Future Work

Prelude simplifies the process of composing communicating real-time tasks, that possibly run at different rates, into a fully deterministic system. This desire for rooting out nondeterminism in the development process was present when synchronous languages were first introduced[8] and it continues with methods applied for industrial tools like Matlab’s Simulink[6] and Esterel Technologie’s SCADE which uses the synchronous language Lustre in mission critical software across aerospace, automotive, and industrial applications. There is also research on synchronous languages that addresses the implementation of Mixed Criticality Systems[15], where some tasks may be allowed to violate the Synchronous Hypothesis and miss deadlines. One could imagine extending a language like Prelude to guarantee synchronized deterministic communication between both hard real-time tasks and less critical soft real-time tasks. The Liquid Clocks[11] framework defines a type system for designing new synchronous languages across different models of time and communication. Liquid Clocks uses refinement types and an inference algorithm inspired by Liquid Types[10] to verify time and causality constraints in a network defined by data flows. Our approach differs from Liquid Clocks in that we use the expressive types found in ATS, an existing programming language, to support the implementation of a domain specific synchronous language for multi-rate periodic systems. In this report, dependent types in ATS of DML-style [14, 13] are assigned to the multi-rate flows introduced in Prelude and also to various clock transformation operators on these flows. Note that there is explicit use of quantifiers in the types assigned to these operators, far exceeding what is accomplished in Prelude, where every clock is either fixed to be a constant or can be inferred from a constant one. For instance, a constraint stating that a node must always produce a flow whose clock is twice as fast as its input node can be readily expressed in ATS but cannot currently in Prelude. The basic building block of composition in synchronous languages like Prelude is a unidirectional flow. Yet, in complex embedded systems, individual components may communicate using various different protocols. While these protocols are implemented on top of flows, there is no formal description for them in an architecture design language like Prelude. One avenue for future work is to develop a synchronous domain specific version of ATS that can use typed channels like those found in Session Types[9] to describe both the temporal behavior of the system and what is communicated inside of it. The latter information, for instance, can help verify node implementations in a synchronous program or detect possible errors.

5 Bibliography