Title :
TCEC: Temperature and Energy-Constrained Scheduling in Real-Time Multitasking Systems
Author :
Qin, Xiaoke ; Wang, Weixun ; Mishra, Prabhat
Author_Institution :
Dept. of Comput. & Inf. Sci. & Eng., Univ. of Florida, Gainesville, FL, USA
Abstract :
The ongoing scaling of semiconductor technology is causing severe increase of on-chip power density and temperature in microprocessors. This urgently requires both power and thermal management during system design. In this paper, we propose a model checking-based technique using extended timed automata to solve the processor frequency assignment problem in a temperature and energy-constrained multitasking system. We also develop a polynomial time-approximation algorithm to address the state-space explosion problem caused by symbolic model checker. Our approximation scheme is guaranteed to not generate any false-positive answer, while it may return false-negative answer in rare cases. Our method is universally applicable since it is independent of any system and task characteristics. Experimental results demonstrate the usefulness of our approach.
Keywords :
formal verification; low-power electronics; microprocessor chips; multiprogramming; polynomial approximation; real-time systems; semiconductor technology; thermal management (packaging); TCEC; energy-constrained multitasking system; energy-constrained scheduling; false-negative answer; false-positive answer; microprocessors temperature; model checking-based technique; on-chip power density; polynomial time-approximation algorithm; power management; processor frequency assignment problem; real-time multitasking systems; semiconductor technology; state-space explosion problem; symbolic model checker; system characteristics; system design; task characteristics; thermal management; timed automata; Algorithm design and analysis; Approximation algorithms; Approximation methods; Automata; Energy consumption; Integrated circuit modeling; Voltage control; Low-power design; model checking; power management; power modeling and estimation;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2012.2190824