An Interface Algebra for Task Graphs
Slobodan Matic and Thomas A. Henzinger
In this research we study interface-based verification of task graphs under time and resource constraints. We focus on a class of component interfaces that enable efficient and flexible composability checking. We are also interested in how the form and complexity of interfaces affect the guaranteed performance of composition.
In our formalism a component implements a task graph: a directed graph where each node represents a task, i.e., a sequential piece of code, and each edge represents the data flow between tasks. Since input degree of a node can be greater than one, a task may execute only after data is available on all input edges (AND type of task causality). Each task executes asynchronously from other tasks. The graph is allowed to have cycles, i.e., we allow for cyclic functional dependencies between tasks. We assume that the primary inputs of a process graph are specified with event arrival curves that bound the number of task executions. In particular, we concentrate either on periodic event models with jitter and burst, or on rate-based event models.
A component interface typically consists of: a resource consumption abstraction, an arrival curve for each input and output port, and a latency for each input-output pair with dependency. The resource abstraction is either a fraction of processing power that is reserved for the component, or, more generally, a bounded-delay resource model. Thus, the interface specifies that the component guarantees certain output latencies depending on assumptions about input event arrivals and allocated resources. The interface can take other forms depending on the topology of the underlying graph that the component implements. Also, to increase composability of the framework, the interface for a component may be described with a more complex predicate that allows for multiple assumption-guarantee pairs.
We present a simple assume-guarantee interface algebra that defines three operations. The compose, connect, and join operations enable construction of composition process graphs from the graphs implemented by individual components. These operations compute as new interface assumptions, the weakest constraints on the unknown components that are necessary to satisfy the specified guarantees. The composition that results in a process graph that contains cycles is more difficult to analyze. If component details are known, this typically entails fixed-point computation on event arrival curves or their abstractions. We recall and modify existing event model propagation techniques to enable interface composition in this case.
The composition operations should allow for incremental interface-based design. According to this property the composition of interfaces can be performed in any order, i.e., the algebra operations are associative. The property results in a flexible framework, and it also means being able to check compatibility and compute composition of the two interfaces without specifying interfaces of other components.
Beside compatibility relation we also define a refinement relation on interfaces. A more refined version of a component may make weaker input assumptions and stronger output guarantees than a more abstract description. Therefore, in a design we can always substitute a refined version for an abstract one. An algebra enables independent implementability if, for composable interfaces, the refinement property is preserved under composition operations. One of the objectives of our work is a formal study of conditions under which the proposed interface algebra supports both the incremental design and the independent implementability methodology.