Temperature- and energy-constrained scheduling in multitasking systems: a model checking approach

The ongoing scaling of semiconductor technology is causing severe increase of on-chip power density and temperature in microprocessors. This has raised urgent requirement for both power and thermal management during each level of system design. In this paper, we propose a formal technique based on model checking using extended timed automata to solve the processor frequency assignment problem in a temperature- and energy- constrained multitasking system. The state space explosion problem is alleviated by transforming and solving a Pseudo-Boolean satisfiability problem. Our approach is capable of finding efficient solutions under various constraints and applicable to other problem variants as well. Our method is independent of any system and task characteristics. Experimental results demonstrate the usefulness of our approach. Categories and Subject Descriptors C.3 [SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS]: Real-time systems and embedded systems General Terms Algorithm, Design Ke...

• Type: Conference
• Year: 2010
• Where: ISLPED
• Authors: Weixun Wang, Xiaoke Qin, Prabhat Mishra
• Keywords: Frequency Assignment Problem, Hardware, ISLPED 2010, On-chip Power Density, Pseudo-Boolean Satisfiability Problem