Theorem proving based Formal Verification of Distributed Dynamic Thermal Management schemes

Distributed Dynamic Thermal Management (DDTM) schemes are widely being used nowadays to cater for the elevated chip temperatures for many-core systems. Traditionally, DDTM schemes are analyzed using simulation or emulation but the non-exhaustive and incomplete nature of these analysis techniques may compromise on the reliability of the chip. Recently, model checking has been proposed for formally verifying simple DDTM schemes but, despite several abstractions, the analysis is limited to less than 100 cores due to the state-space explosion problem. As a more scalable approach for next-generation many-core systems, we propose a methodology based on theorem proving to perform formal verification of DDTM schemes. The proposed approach allows specification and verification of both functional and timing properties for any number of cores and for all times. For this purpose, the paper provides a higher-order-logic formalization of a generic DDTM scheme. The proposed generic model can be specialized to formally specify most of the existing DDTM schemes and thus formally verify their thermal properties, like temperature bounds and balancing and time to reach thermal stability, as higher-order-logic theorems. As an illustrative example, the paper presents a formal model and analysis of a Distributed Task Migration based DDTM scheme for many-core systems.