More Web Proxy on the site http://driver.im/

Article

Multicore power management: ensuring robustness via early-stage formal verification

Authors:

Daniel J. Sorin,

Geert JanssenAuthors Info & Claims

MEMOCODE'09: Proceedings of the 7th IEEE/ACM international conference on Formal Methods and Models for Codesign

Pages 78 - 87

Published: 13 July 2009 Publication History

Abstract

Dynamic power management (DPM) is important for multicore architectures. One important challenge for multicore DPM schemes is verifying that they are both safe (cannot lead to power or thermal catastrophes) and efficient (achieve as much performance as possible without exceeding power constraints). The verification difficulty varies among designs, depending, for example, on the particular power management mechanisms utilized and the algorithms used to adjust them. However, verification effort is often not considered in the early stages of DPM scheme design, leading to proposals that can be extremely difficult to verify.

To address this problem, we propose using formal verification (with probabilistic model checking) of a high-level, early-stage model of the DPM scheme. Using the model checker, we estimate the required verification effort, providing insight on how certain design parameters impact this effort. Furthermore, we supplement the verifiability results with high-level estimates of power consumption and performance, which allow us to perform a trade-off analysis between power, performance, and verification. We show that this trade-off analysis uncovers design points that are better than those that consider only power and performance.

References

[1]

P. Bose, D. H. Albonesi, and D. Marculescu. Guest Editors' Introduction: Power and Complexity Aware Design. IEEE Micro, pages 8-11, Sept/Oct 2003.

Digital Library

[2]

J. Choi et al. Thermal-aware Task Scheduling at the System Software Level. In Proc. of the Int'l Symposium on Low Power Electronics and Design, Aug. 2007.

Digital Library

[3]

D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol Verification as a Hardware Design Aid. In 1992 IEEE Int'l Conference on Computer Design: VLSI in Computers and Processors, pages 522-525, 1992.

Digital Library

[4]

G. Dubost, S. Granier, and G. Berry. An Esterel-Based Formal Specification Methodology for Power Manager Development. Presented at the SAME Forum, Oct. 2007.

[5]

D. Dunn. Intel Delays Montecito in Roadmap Shakeup. EE Times, October 24 2005.

[6]

R. Hum. How to Boost Verification Productivity. EE Times, January 10 2005.

[7]

C. Isci, A. Buyuktosunoglu, C.-Y. Cher, P. Bose, and M. Martonosi. An Analysis of Efficient Multi-Core Global Power Management Policies: Maximizing Performance for a Given Power Budget. In Proc. of the 39th Annual IEEE/ACM Int'l Symposium on Microarchitecture, Dec. 2006.

Digital Library

[8]

M. Kwiatkowska, G. Norman, and D. Parker. PRISM 2.0: A Tool for Probabilistic Model Checking. In Proc. of the 1st Int'l Conference on Quantitative Evaluation of Systems, pages 322-323, Sept. 2004.

Digital Library

[9]

M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic Model Checking and Power-Aware Computing. In Proc. of the 7th Int'l Workshop on Performability Modeling of Computer and Communication Systems, pages 6-9, Sept. 2005.

[10]

A. Lungu and D. J. Sorin. Verification-Aware Microprocessor Design. In Proc. of the Int'l Conference on Parallel Architectures and Compilation Techniques, pages 83-93, Sept. 2007.

Digital Library

[11]

M. M. K. Martin. Formal Verification and its Impact on the Snooping versus Directory Protocol Debate. In Proc. of the Int'l Conference on Computer Design, Oct. 2005.

Digital Library

[12]

M. R. Marty et al. Improving Multiple-CMP Systems Using Token Coherence. In Proc. of the Eleventh Int'l Symposium on High-Performance Computer Architecture, pages 328-339, Feb. 2005.

Digital Library

[13]

R. McGowen et al. Power and Temperature Control on a 90-nm Itanium Family Processor. IEEE Journal of Solid-State Circuits, 41(1):229-237, Jan. 2006.

[14]

K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

[15]

M. Moudgill, P. Bose, and J. H. Moreno. Validation of Turandot, a Fast Processor Model for Microarchitecture Exploration. In Proc. of the IEEE Int'l Performance, Computing and Communications Conference, pages 451- 457, Feb. 1999.

[16]

M. Moudgill, J.-D. Wellman, and J. H. Moreno. Environment for PowerPC Microarchitecture Exploration. IEEE Micro, 19(3):15-25, May/June 1999.

Digital Library

[17]

G. Norman, D. Parker, M. Kwiatkowska, and S. Shukla. Using Probabilistic Model Checking for Dynamic Power Management. Formal Aspects of Computing, 17(2):160- 176, Aug. 2005.

[18]

C. Poirier, R. McGowen, C. Bostak, and S. Naffziger. Power and Temperature Control on a 90nm Itanium-family Processor. In Proc. of the IEEE Int'l Solid-State Circuits Conference, Feb. 2005.

[19]

J. Sartori and R. Kumar. Proactive Peak Power Management for Many-Core Architectures. Technical Report CRHC-07-04, UIUC CRHC, Oct. 2007.

[20]

J. Sharkey, A. Buyuktosunoglu, and P. Bose. Evaluating Design Tradeoffs in On-Chip Power Management for CMPs. In Proc. of the Int'l Symposium on Low Power Electronics and Design, Aug. 2007.

Digital Library

[21]

T. Sherwood, E. Perelman, G. Hamerly, and B. Calder. Automatically Characterizing Large Scale Program Behavior. In Proc. of the Tenth Int'l Conference on Architectural Support for Programming Languages and Operating Systems, Oct. 2002.

Digital Library

[22]

S. Shukla and R. K. Gupta. A Model Checking Approach to Evaluating System Level Dynamic Power Management Policies for Embedded Systems. In Proc. of the High-Level Design Validation and Test Workshop, pages 53- 57, 2001.

Digital Library

Cited By

Schreiner SSeyyedi RFakih MGrüttner KNebel WMudge TPnevmatikatos D(2018)Towards power management verification of time-triggered systems using virtual platformsProceedings of the 18th International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation10.1145/3229631.3235025(81-88)Online publication date: 15-Jul-2018
https://dl.acm.org/doi/10.1145/3229631.3235025
Simonović MŽivojnović VSaranovac L(2017)Formal model for system-level power management designProceedings of the Conference on Design, Automation & Test in Europe10.5555/3130379.3130752(1603-1606)Online publication date: 27-Mar-2017
https://dl.acm.org/doi/10.5555/3130379.3130752
Bukhari SLodhi FHasan OShafique MHenkel J(2017)CAnDy-TMProceedings of the Conference on Design, Automation & Test in Europe10.5555/3130379.3130683(1289-1292)Online publication date: 27-Mar-2017
https://dl.acm.org/doi/10.5555/3130379.3130683
Show More Cited By

Index Terms

Multicore power management: ensuring robustness via early-stage formal verification
1. Hardware
  1. Hardware validation
    1. Functional verification
2. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
    2. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Traffic-aware power optimization for network applications on multicore servers
DAC '12: Proceedings of the 49th Annual Design Automation Conference

In this paper, we design, implement, and evaluate a traffic-aware and power-efficient multicore server system by translating incoming traffic rate to appropriate system operating level, which is then translated to optimal per-core frequency ...
MAximum Multicore POwer (MAMPO): an automatic multithreaded synthetic power virus generation framework for multicore systems
SC '11: Proceedings of 2011 International Conference for High Performance Computing, Networking, Storage and Analysis

The practically attainable worst case power consumption for a computer system is a significant design parameter and it is a very tedious process to determine it by manually writing high power consuming code snippets called power viruses. Previous ...
A Middleware for Power Management in Multicore Smartphones
MOBIQUITOUS'15: proceedings of the 12th EAI International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services on 12th EAI International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services

Increased power consumption is a critical concern for smartphone users. While multi-core processors in smartphones have already emerged in market, current applications are yet to take full advantage of this new architecture, particularly in the area of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MEMOCODE'09: Proceedings of the 7th IEEE/ACM international conference on Formal Methods and Models for Codesign

July 2009

180 pages

ISBN:9781424448067

Sponsors

Publisher

IEEE Press

Publication History

Published: 13 July 2009

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 34 of 82 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
40
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Schreiner SSeyyedi RFakih MGrüttner KNebel WMudge TPnevmatikatos D(2018)Towards power management verification of time-triggered systems using virtual platformsProceedings of the 18th International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation10.1145/3229631.3235025(81-88)Online publication date: 15-Jul-2018
https://dl.acm.org/doi/10.1145/3229631.3235025
Simonović MŽivojnović VSaranovac L(2017)Formal model for system-level power management designProceedings of the Conference on Design, Automation & Test in Europe10.5555/3130379.3130752(1603-1606)Online publication date: 27-Mar-2017
https://dl.acm.org/doi/10.5555/3130379.3130752
Bukhari SLodhi FHasan OShafique MHenkel J(2017)CAnDy-TMProceedings of the Conference on Design, Automation & Test in Europe10.5555/3130379.3130683(1289-1292)Online publication date: 27-Mar-2017
https://dl.acm.org/doi/10.5555/3130379.3130683
Sorin DMatthews OZhang M(2014)Architecting Dynamic Power Management to be Formally VerifiableProceedings of the 51st Annual Design Automation Conference10.1145/2593069.2596669(1-3)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1145/2593069.2596669
Wang WDong GDeng ZZeng GLiu WXiong HBalaji PGuo MHuang Z(2014)Reachability Analysis of Cost-Reward Timed Automata for Energy Efficiency SchedulingProceedings of Programming Models and Applications on Multicores and Manycores10.1145/2578948.2560695(140-148)Online publication date: 7-Feb-2014
https://dl.acm.org/doi/10.1145/2578948.2560695
Wang WDong GDeng ZZeng GLiu WXiong HBalaji PGuo MHuang Z(2014)Reachability Analysis of Cost-Reward Timed Automata for Energy Efficiency SchedulingProceedings of Programming Models and Applications on Multicores and Manycores10.1145/2560683.2560695(140-148)Online publication date: 7-Feb-2014
https://dl.acm.org/doi/10.1145/2560683.2560695
Ismail MHasan OEbi TShafique MHenkel JHenkel J(2013)Formal verification of distributed dynamic thermal managementProceedings of the International Conference on Computer-Aided Design10.5555/2561828.2561878(248-255)Online publication date: 18-Nov-2013
https://dl.acm.org/doi/10.5555/2561828.2561878
Bogdan PMarculescu RJain S(2013)Dynamic power management for multidomain system-on-chip platformsACM Transactions on Design Automation of Electronic Systems10.1145/250490418:4(1-20)Online publication date: 25-Oct-2013
https://dl.acm.org/doi/10.1145/2504904
Mukherjee RMukherjee SDasgupta PGhosal SShroff GChandra SNagappan N(2013)Model checking of global power management strategies in software with temporal logic propertiesProceedings of the 6th India Software Engineering Conference10.1145/2442754.2442759(29-34)Online publication date: 21-Feb-2013
https://dl.acm.org/doi/10.1145/2442754.2442759
Bose PBuyuktosunoglu ADarringer JGupta MHealy MJacobson HNair IRivers JShin JVega AWeger ARosenstiel WMacii E(2012)Power management of multi-core chipsProceedings of the Conference on Design, Automation and Test in Europe10.5555/2492708.2492953(977-982)Online publication date: 12-Mar-2012
https://dl.acm.org/doi/10.5555/2492708.2492953
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents