Theorem proving based Formal Verification of Distributed Dynamic Thermal Management schemes

Muhammad Usama Sardar, Osman Hasan, Muhammad Shafique, Jörg Henkel

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)157-171
Number of pages15
JournalJournal of Parallel and Distributed Computing
Volume100
DOIs
StatePublished - Feb 1 2017

Keywords

  • Dynamic Thermal Management
  • Higher-order logic
  • Many-core systems
  • Task migration
  • Theorem proving

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computer Networks and Communications
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Theorem proving based Formal Verification of Distributed Dynamic Thermal Management schemes'. Together they form a unique fingerprint.

Cite this