ABSTRACT
Cyber-physical systems (CSPs) are demanding energy-efficient design not only of hardware (HW), but also of software (SW). Dynamic Voltage and and Frequency Scaling (DVFS) and Dynamic Power Manage (DPM) are most popular techniques to improve the energy efficiency. However, contemporary complicated HW and SW designs requires more elaborate and sophisticated energy management and efficiency evaluation techniques.
This paper is concerned about energy supply planning for real-time scheduling systems (units) of which tasks need to meet deadlines. This paper presents a model based compositional energy planning technique that computes a minimal ratio of processor frequency that preserves schedulability of independent and preemptive tasks. The minimal ratio of processor frequency can be used to plan the energy supply of real-time components.
Our model-based technique is extensible by refining our model with additional features so that energy management techniques and their energy efficiency can be evaluated by model checking techniques. We exploit the compositional framework for hierarchical scheduling systems and provide a new resource model for the frequency computation. As results, our use-case for avionics software components shows that our new method outperforms the classical real-time calculus (RTC) method, requiring 36.21% less frequency ratio on average for scheduling units under RM than the RTC method.
RELATED WORK
For energy-aware scheduling techniques, early efforts, leveraged the performance slack available in real-time applications such that reducing the performance of a processor does not cause any applications to miss their deadlines. They have developed scheduling algorithms, exploiting the property of real-time tasks that the actual task execution times are much less than the assumed worst-case execution time, thus the remaining time to each deadline is a guaranteed slack time where no higher priority task would intervene. However, they are not extensible enough for contemporary scheduling systems to instantly deal with their complexity due to variety of real-time features from costumers.
PRELIMINARIES
Fig. 1. Conceptual task in SWA.
A conceptual task modeled by SWA is shown in Fig. 1, where a task tid executes between BCET [tid] and WCET [tid] time units every PRD [tid] time units (The initial location in the model is Run with double-circle by UPPAAL syntax). The execution time of tasks, the CPU-using time, is denoted by et [tid], and its running time, the time that has elapsed since its new period began, is denoted by rt [tid].
COMPOSITIONAL FRAMEWORK FOR ENERGY-AWARENESS
Fig. 2. Job executions.
In principle, the execution of a periodic task has a laxity interval where the task can delay the execution as long as it does not miss the deadline, as shown in Fig. 2(a). The laxity interval of a task can be interpreted by a frequency laxity which can throttle the processor frequency ratio, and such a lowered frequency ratio inflates the execution of a task as much as the laxity interval of a task, as shown in Fig. 2(b). the laxity interval of a periodic task in Fig. 2(a) can be split, where the split laxity and the execution of the task can interleave, as shown Fig. 2(c).
Fig. 3. The worst-case resource supply of PLRM.
Similary with PRM resource model of the compositional framework, as shown in Fig. 2, the PLRM has the worst-case resource supply pattern shown in Fig. 3. In this worst-case, the resource supply never starts before the laxity elapses. The worst-case resource supply happens when a new resource demand occurs as soon as a new period begins.
MODEL-BASED COMPOSITIONAL FRAMEWORK
Fig. 7. Architecture of SWA models.
Fig. 7 shows the structure of our SWA scheduling unit model for multi-processor, however we limit the number of core running tasks to 1 in our experiments. It is structured in a similar way with a real-time operating system. Interrupt Handler in Fig. 7 handles interrupts from HW/SW components and requests a scheduler to instantiate and schedule jobs.
Fig. 8. SWA model of task.
Given a CSWA and a PLRMSWA, the schedulability is checked by checking the property A[] not error. The variable error in the temporal logic happens when a running task misses its deadline, i.e., the task model Fig. 8 stops on the location DLMissed). If the model checker cannot find out any counterexample against the property, a given task set is proved schedulable.
COMPARISON OF MINIMAL FREQUENCY RATIOS
Fig. 9. Improvements of new methods against the RTC method.
Fig. 9 shows that our new method outperforms the classical RTC technique, requiring the average 36.21% less frequency ratio for scheduling units under RM. However, the RTC technique outperforms the new method in the case of EDF.
Fig. 10. Variation of minimal frequency ratios.
For the RM cases, Fig 10(a) compares the deviations of minimal frequencies from the CPU utilizations of given task sets computed by our model-based technique and the RTCbased technique. Fig. 10(b) the variation of frequencies by the number of tasks (from 2 to 7). Using the same CPU utilization (50%), the frequency ratio satisfying the the components increases by the number of tasks in our method, but the RTCbased technique is sensitive to the number of tasks.
Fig. 11. Verification times of UPPAAL MC.
Fig. 11 shows the variation of UPPAAL MC verification time using our models by the number of tasks. The scalability of our model-based framework is impacted by two major factors: the number of tasks and the complexity of task properties.
CONCLUSION
The static power dissipation is more important than ever as dynamic power dissipation reduce by the advance of CMOS technologies. Moreover, parameters of real-time components to consider for real-time guarantee are so diverse that the classical energy management and efficiency analysis techniques shows a lot of limitations.
This paper presents a novel model-based technique based on the schedulability theory of the compositional framework to compute a static minimal frequency ratio of processors. To the end, this paper presented a new supply bound function depending on a periodic resource model, PLRM, that provides a minimal CPU cycles to a given task set in the worst-case. Using the periodic model, a real-time component is verified schedulable for a given frequency ratio.
In addition, using the new periodic resource model for frequency ratio, we presented schedulability conditions for preemptive task set limited by a minimal frequency ratio of a processor. To enlarge the extensibility of our framework, we captured scheduling units under EDF and RM and the PLRM resource model in formal models of UPPAAL so that more various resource demand can be represented by the scheduling unit model in automaton models and analyzed against the resource model given in the same formalism. In the comparison with a RTC-based method, we showed that our method requires the average 36.21% less frequency ratio for the task sets under RM than the comparable RTC method does.
In the future work, we will study an automated computation technique for a frequency interface for a given component based on our new schedulability conditions and apply this approach to energy-aware composition of hierarchical scheduling systems.
Source: University of Pennsylvania
Authors: Jin Hyun Kim | Deepak Gangadharan | Oleg Sokolsky | Axel Legay | Insup Lee