HomeEventsPhd Defence Waheed Ahmad

Phd Defence Waheed Ahmad

green computing: efficient energy management of multiprocessor streaming applications via model checking

Consumer electronics such as televisions, telephones, and computers have become an essential part of a human life. An important subclass of consumer electronics termed embedded multimedia systems deal with applications from the multimedia and Digital Signal Processing (DSP) domain executing on multiprocessors. Such applications repetitively process an input stream of indefinite length, for example a video decoder that decodes a video stream. These applications are often referred to as streaming applications in literature. Examples of embedded multimedia systems are mobile phones, virtual reality gaming consoles, 3D-enabled televisions, and car navigation systems. The Synchronous Dataflow (SDF) model of computation naturally captures the characteristics of streaming applications and allows design-time analysis of timing and resource utilisation.


Embedded multimedia systems have evolved significantly in recent decades, and are becoming ubiquitous in our daily lives. This trend is also giving rise to challenges such as (1) increasing energy demand leading to global warming, (2) requirement of seamless and robust performance, and (3) growing complexity of embedded multimedia systems resulting in higher development cost and longer time-to-market.

To address these challenges, we introduce several methods that combine resource and power management with scheduling decisions. As an analysis environment, we consider model checking because of its ability to generate optimal traces (schedules).

The first approach is throughput-optimal scheduling of SDF graphs on a given number of processors via the proven formalism of timed automata. In this work, SDF graphs along with hardware platforms are translated compositionally to timed automata. The problem of throughput optimisation is encoded as a query over timed automata. The model checker UPPAAL extracts a trace representing a throughput-optimal schedule. In this way, we can efficiently determine a trade-off between number of processors and throughput for a certain streaming application.

The second approach generates energy-optimal schedules of SDF graphs. The hardware architecture is decorated with novel energy management techniques like dynamic power management (DPM, switching to low power state) and dynamic voltage and frequency scaling (DVFS, throttling processor frequency). To balance flexibility and design complexity, the concept of Voltage and Frequency Islands (VFIs) is considered. It achieves fine-grained system-level power management, by operating all processors in the same VFI at a common frequency/voltage.

In this work, we utilise priced timed automata, a model checking formalism that extends timed automata with costs, which are used to model the power consumption of processors. After SDF graphs and hardware platforms are translated to priced timed automata, the model checker UPPAAL CORA generates a trace representing an energy-optimal schedule. We demonstrate that the combination of DPM and DVFS provides an energy reduction beyond considering DVFS or DPM separately. Moreover, we show that by clustering processors in VFIs, DPM can be combined with any granularity of DVFS.

The third approach derives the Quality of Service of SDF graphs mapped on hardware platforms powered by multiple batteries. In this approach, we use hybrid automata which are an extension of timed automata with continuous variables. Furthermore,  using the model checker UPPAAL SMC, we evaluate (1) system lifetime, and (2) minimum required initial battery capacities to achieve the desired application performance.

In today's agile world, there is a fierce competition that requires low development cost and short time-to-market. To achieve this purpose, an efficient modelling approach is needed which can provide modularity, extensibility and interoperability. We have developed a Model-Driven Engineering (MDE) based framework which fulfils these requirements. In this framework, we introduce the so-called metamodels for SDF graphs and hardware platforms. The SDF graphs and hardware platforms are translated to the model-checking domain automatically using model transformations.

Finally, we evaluate the performance of our approach of throughput analysis by applying it in an industrial case study of face recognition systems provided by Recore Systems, Netherlands. With this case study, the performance of our approach is validated in realistic scenarios and, thus, the problem is shown to be solvable with acceptable concessions.