Scheduling Induced Quasi-Cyclic Structure
In systems where the execution times of tasks are input dependent, and thus their worst case execution times cannot be characterized easily, the scheduler, the application, and the environment may combine to impose a variety of different constraints on the execution of tasks. Verification of these systems requires models that can integrate all four semantic domains considered in this research: application requirements, run-time behavioral information, resource management, and system software mechanisms.Because of the preemptive nature of resource management in such systems, finite timed automata (which we have applied in our previous research to model the time and event semantics of system software) alone are not able to represent the combined semantics. Instead, we have used infinite timed automata models (which we call time domain automata) to capture semantics involving alternative preemptive interleavings of execution intervals. An example of such an automaton for two preemptively interleaved threads of execution is shown in the following figure.
Dwyer, et al. have shown how repetition of "quasi-cyclic" structures in the state space can be exploited to reduce the complexity of model checking. As the figure above illustrates, our first contribution is to extend their approach from periodic real-time systems with rate-monotonic scheduling, to real-time systems whose timing and scheduling semantics are more variable, by identifying similar repeated structure within our time domain automata models.
Bounds on Threads Execution
Our second contribution is to identify how different bounds on the execution of the interleaving execution intervals described above can arise from different constraints: from fairness constraints (e.g., imposed by a scheduler); from explicit delay constraints (e.g., imposed by application requirements); and from event ordering constraints (e.g., imposed either by a scheduler or by synchronization mechanisms).These bounds are often functions not only of the variables in the (potentially quasi-cyclic) state space, but also of the temporal guards on transitions along different paths through the (infinite) time domain automaton. As quasi-cyclic structures are repeated in the state space, these bounds can be simplified by parameterizing them with an index for the current repetition of the structure in the state space. The following figure illustrates such index-parameterized bounds.
A key question is whether the bounds themselves (and thus the semantics of the executing threads) converge towards a steady state bound as time progresses, and if so whether that steady state falls within certain absolute limits (e.g., prescribed by application requirements). An example of such convergent bounds, induced by fairness constraints imposed by a scheduler, is shown in the following figure.
Note how convergence occurs in the figure above: as the index goes to infinity, the bounds converge to steady state based on constant parameters that characterize the scheduler's decision function.
Case Study
To validate this formal model in the context of a realistic combination of application constraints, system software, scheduling semantics, and behavioral monitoring, we compared the bounds predicted by that formal model to the empirical behavior of a system developed in our previous collaborative research on flexible but precise scheduling infrastructure. The following figure illustrates the architecture of an example video processing application we considered in this case study.
As illustrated by the figure above, The example application consists of multiple processing stages for real-time image capture, transmission and display, with sub-steps on the sending and receiving hosts to compress and decompress individual images to reduce transmission latency. To avoid idling CPU and network resources, and to provide fine-grained scheduling control points throughout the application, each processing stage is serviced by a pool of threads, with each thread dedicated to a particular processing pipeline that spans multiple stages end-to-end. That concurrency architecture is illustrated by the following figure.
We ran five concurrent pipelines in this example, under the scheduling constraint that the progress of each pipeline is kept within one frame of all other pipelines. We gave some of the pipelines differing ranges of variable execution times per stage (70 to 80 msec for pipelines 1 and 3, 80 to 90 msec for pipelines 2 and 4, and 100 to 110 msec for pipeline 5). The resulting quasi-cyclic structure can be described by a 5-dimensional hypercube similar to the ones shown in the following figure for the 2-dimensional and 3-dimensional cases).
In the following figures, the right hand column shows the observed raw frame-by-frame progress of all of the pipelines. The left hand column offers the same comparison at only the points where all five pipelines have made equivalent progress.
Equivalent Progress | Raw Progress |
 |  |
To validate our formal models and the bounds we derived from them, we compared the bounds predicted from our models to the actual execution of the system in terms of frames processed in each pipeline. In addition to the absolute bounds predicted by our models, we used the models and parameters calculate tighter bounds that encapsulated the empirically observed semantics for purposes of analysis. The purpose of the recalculated bounds is to give a measure of the pessimism of the specified bounds relative to the observed behavior. However, the looser bounds are the ones that must be used for verification since they capture all possible executions absent any further specified constraint.
In the next set of figures, the right hand column compares the observed raw frame-by-frame progress to the predicted (and empirically tightened) bounds. The left hand column offers the same comparison at only the points where all five pipelines have made equivalent progress (i.e., the points where the scheduler has enforced a transition from one repetition of the quasi-cyclic structure to the next).
Equivalent Progress | Raw Progress |
 |  |
 |  |
 |  |
 |  |
 |  |