Middleware Models
The first major contribution of this research has been the development a new set of models for the timing and event semantics of reusable middleware abstractions found in the widely used ACE framework. These models are based on timed automata and can be used within timed model checking tools such as the IF toolkit and UPPAAL to verify safety and timing properties of a system, including the middleware platform on which the system is deployed.The architecture diagram below depicts the different models we have developed, and how they cover different parts of the ACE architecture. In this figure, unshaded rectangles in the diagram represent models expressed directly as timed automata, while shaded rectangles represent models expressed as data structures that are shared among the automata:
Model Refinements
The second major contribution of this research has been the identification and application of model refinements that are specific to the middleware domain from which out models are derived, but also are generally valid across a variety of applications using such middleware. These refinements both more accurately reflect the semantics of the middleware domain, and also in several cases reduce the amount of state space exploration that must be performed in checking the models.
Modeling Threads
The first such refinement was to model threads of control flowing concurrently through multiple objects as chains of object method invocations are performed, a feature that is not provided by existing model checkers for timed automata. The following figure shows a flow of control from one object to another object (Foo1 to Foo2, Bar1 to Bar2), with both of these objects modeled as timed automata. To model a distinct thread flow of control, we added a thread id that is maintained by each automaton, which serves as a unique reference to the thread whose execution it represents.
Modeling Priority Scheduling
The second refinement was to model the prioritization of threads of control that is used in many real-time systems (e.g., to enforce a rate monotonic scheduling policy efficiently). The following figure shows how a model checker's ability to enforce specified priority rules can be used to ensure the execution of automaton transitions in the models adheres to the prioritization of threads in the actual system.
Modeling Run-to-Completion Semantics
The third refinement was to model run-to-completion semantics among threads with the same thread priority (e.g., under the SCHED_FIFO policy in Linux and other operating systems), a widely used feature of real-time systems. To achieve this, we added a global thread identifier to track which thread is currently executing. This allows us to specify another model checker priority rule which will ensure the current thread continues executing unless a higher priority thread becomes eligible to run. The following figure illustrates this semantics.
However, simply maintaining a current thread identifier and continuing the execution of the automaton whose thread is current may accidentally over-constrain the model by eliminating concurrent execution that is possible in the actual system. The left side of the following figure illustrates this problem. We therefore refined the run-to-completion semantics further by adding a low priority automaton that only runs when the automata modeling threads are idle. As the right side of the following figure illustrates, this "idle catcher" automaton sets the current thread id back to nil, ensuring non-deterministic choice of the next thread to be run after an idle interval.
Verification Studies
The third major contribution of this research has been to demonstrate the use of our models in verifying properties of specific applications and protocols based on the middleware abstractions we have modeled.As a representative example of verification scenarios for ACE-based applications, we used our models to verify a version of the Gateway example that is distributed with ACE, in which notification of event delivery establishes a potential for deadlock. We used model checking in the IF toolkit to explore the effects of alternative event dispatching strategies for the ACE Reactor ("wait-on-connection" in which remote method invocations block in the calling object until the reply is received, versus "wait-on-reactor" in which the thread of execution making the call is returned to the reactor and the reply is handled asynchronously) in that example.
The following figure illustrates the results of those studies, which demonstrate the use of our models in detecting timing and concurrency hazards in non-trivial software systems. The left side of the figure shows an event sequence in which a deadlock occurs with the "wait-on-connection" strategy, which was detected automatically by the IF model checker using our models. With the "wait-on-reactor" strategy, model checking verified deadlock freedom, as one representative trace shown on the right side of the figure below illustrates.
Wait-on-Connection Strategy | Wait-on-Reactor Strategy |
 |  |
Because of the lower complexity (and accordingly lower overhead) of the "wait-on-connection" strategy, we have been collaborating with Cesar Sanchez, Henny Sipma, and Zohar Manna at Stanford University who are working to develop a suite of deadlock avoidance protocols that can overcome the potential for deadlock hazards noted above for the "wait-on-connection" strategy. We have implemented the simplest of these protocols, called the BASIC-P protocol, in ACE's thread pool reactor, and have developed timed automata models of the protocol operating within the reactor. We are also working to implement and model the other protocols in this family to offer applications having different characteristics and requirements a range of flexible and verifiable options. The following figure shows a comparison of the execution traces produced by checking the models, and by running the same example using our implementation in ACE.
Model Based Scheduling Policy Generation, Evaluation, and Refinement
The fourth major contribution of this research has been to initiate and culminate a separate branch of research on how state space representations of resource utilization can be leveraged to generate, evaluate, and refine policies for scheduling (particularly non-preemptive) access to resources.Preliminary results developed under this grant (published in Washington University Department of Computer Science and Engineering Technical Reports WUCSE-2006-34 and WUCSE-2007-34) were significantly expanded with support from NSF grant CNS-0716764 (Cybertrust) titled CT-ISG: Collaborative Research: Non-bypassable Kernel Services for Execution Security, to show how non-preemptive scheduling of a resource between tasks whose durations of use are stochastic could (through modeling as a Markov Decision Process) be achieved optimally with respect to a value measure that initially represented simple proportional sharing of the resource and then was generalized to a wider range of utility-based reward functions.
Although the concluding results of that research (published at RTSS 2010) established a good foundation towards on-line use of time-utility based value-optimal schedling policies in real systems, they also suffered from significant time and space complexity in generating and storing the scheduling policies themselves. Several additional advances were needed to make those techniques more applicable to real-world systems, which were pursued as the final phase of this project.
Utility-Aware Scheduling Heuristics
The first advance was to formulate and evaluate alternative heuristic approaches to see how well they could approximate value-optimal scheduling policies under different conditions. The figures below illustrate three representative heuristics that our results indicate are useful under different conditions. The figure on the left below illustrates a "deadline" heuristic that schedules tasks according to the earliest discontinuity in the first derivative of their utility curve. The middle figure below illustrates a pseudo-slope heuristic called "pseudo 0" that is derived from a generalization of the Utility Accrual Packet Scheduling Algorithm developed by Wang and Ravindran (IEEE TPDS vol. 15 no. 1, 2004) to scheduling problems involving stochastic task durations. The figure on the right below illustrates a "greedy" heuristic that considers the immediate expectation of utility for each alternative scheduling action.Deadline Heuristic
Pseudo 0 Heuristic
Greedy Heuristic
We evaluated the different heuristics using varying loads and also differently shaped utility curves. The figure to the left below illustrates "downward step" curves in which a particular value is accrued by completion prior to a termination time, after which no value is accrued. The middle figure below illustrates "linear drop" utility curves that give a fixed value for completion before a critical point, and then give linearly decreasing vale from the critical point until a termination time after which no value is accrued. The figure on the right below illustrates "target sensitive" utility curves in which value increases linearly until a critical point, then decreases linearly until the termination time, and is zero after that. In addition to these "soft real-time" utility curves, we also evaluated "hard real-time" versions in which instead of remaining at zero after the termination time the utilities were (randomly) assigned a large negative value.
In general, the deadline heuristic was the most effective for soft real-time cases with a downward step utiity curve, as the upper left figure below illustrates. For soft real-time cases with linear drop utility curves or target sensitive utility curves under high or medium load, the pseudo 0 heuristic performed best as the upper right figure below illustrates. For hard real-time cases, except for target sensitive utility curves under low load, the greedy algorithm performed best as the lower left figure below illustrates. As the lower right figure below illustrates, none of the heuristics was able to capture a significant fraction of the optimal value for target-sensitive utility curves under low load (in either soft real-time or hard real-time versions).
The tables below summarize the recommended heuristics for the cases we evaluated (with no heuristic being suitable for target-sensitive utility curves under low load).
Decision Tree Representations
The second advance was to examine whether value-optimal policies could be approximated in a manner that is more broadly effective than was achieved by the heuristics we investigated. The figure on the left below illustrates the problem that in general an optimal policy is a mapping from each possible system state to a value-optimal scheduling action to take in that state, requiring storage proportional to the number of system states at run-time, which may not be achievable in practice for even moderately large numbers of states. Furthermore, if the model from which the policy was obtained is not perfectly accurate it may consider a system state unreachable and not specify an action for it - if in practice the state is in fact reached, the policy cannot correctly guide the system at that point.The middle figure below shows how decision trees can be used to reduce the size of the policy representation in many cases, by combining related states (using greedy entropy minimization) into tree nodes that are organized hierarchically according to constraints on the state variables. The decision trees also implicitly provide decisions for states the value-optimal policy may have omitted.
To evaluate the effectiveness of this approach, we conducted evaluations to determine at what tree sizes (over randomly selected policies) the best encoding of the policy occurred. As the figure on the right below shows, in a noticable fraction of the cases a tree of size at most 10 was sufficient while in other cases a larger tree representation was needed.
Integrated Approach: Pruned Decision Trees with Heuristics at the Leaves
The third advance was to combine results of the two previous advances into a cohesive approach to on-line scheduling that could accrue a significant fraction of the optimal value, with significantly lower complexity overall. In particular this advance allows a large fraction of the value to be achieved in a high percentage of the cases, while allowing even more value to be extracted in cases where most of the value already has been achieved.The figure on the left below illustrates the approach, in which a leaf of the tree may use a heuristic to recommend an action, rather than having a fixed action always be specified. The figure on the right below shows the benefit of this approach: when the best combination of tree and heuristics at the leaves (labeled "best" in the figure) was used it outperformed the tree approach alone (labeled "tree" in the figure) in a small number of cases and was otherwise comparable, but significantly outperformed the best performing heuristic (labeled "heuristic" in the figure).
Further discussion of all of these culminating contributions, and details of the models and techniques used, is available in Terry Tidwell's doctoral dissertation.