Transcript Verification-Aware Microprocessor Design

Multicore Power Management:
Ensuring Robustness via EarlyStage Formal Verification
Anita Lungu*, Pradip Bose**, Daniel Sorin*,
Steven German**, Geert Janssen**
*Duke
University
**IBM
T. J. Watson
Research Center
High Level Motivation and Goal
• Dynamic Power Management (DPM) is useful for
multicore processors with power constraints
• Goal: Enable DPM to be more easily adopted in
current processors
– Observation: A DPM that is easier to verify is more
robust and more likely to be included in processors
– Proposal: Design verification-aware DPM schemes
Memocode 2009
DPM for Multicore Processors
• We expect DPM to
–
–
–
–
Increase power efficiency
Avoid power spikes
Cap power to allocated budget
Etc.
• But, if incorrect, DPM can
– Throttle performance to unacceptable level
– Exceed allocated power budget
– Lead to data corruption
Need to verify DPM
schemes for correctness!
Memocode 2009
DPM Scheme Verification Goals
• Safety: Power usage within desired levels & no
deadlocks in DPM protocol
– Bug: Power capping DPM often exceeds budget
• Performance: resulting performance loss is
acceptable
• Functional Correctness: correct results with DPM
– Bug: DPM increases dI/dt problem  data corruption
DPM verification is important!
Memocode 2009
Importance of DPM Verification Effort
• Design verification is challenging even without
DPM!
– ~60% of resources for new processor
development allocated to verification
- Increased time to market
Add difficult-to-verify
DPM
- Coverage goals not reached
?
- Missed bugs
- Disable DPM scheme?
• Important to consider DPM verification effort!
– We approximate it as number of reachable states
Memocode 2009
Current DPM Design and Verification
DPM Scheme Concept
• Early design stage
– Focus on DPM
performance, power
– DPM verifiability often
not considered
High-Level Model
Early in
Design
No
Acceptable
Power/Performance?
• Late design stage
– Verify DPM scheme
– DPM can have
enormous reachable
state space
– Difficult to change DPM
concept
Detailed Simulation
Late in
Design
Memocode 2009
Found Bug?
No
No
Sufficient
Coverage?
Yes
Done
Yes
Proposed DPM Design and Verification
• Validate high-level DPM
concept through formal
Early in
verification
Design
• Formal verification
benefits:
– Exhaustive traversal of
reachable state space
(of high-level model)
– Estimation of size of
reachable state space
(verifiability)
– Catch design bugs early
DPM Scheme Concept
High-Level Formal Model
High-Level Model
No
Acceptable
Power/Performance?
Verification
Scalability?
Yes
Successful
Verification?
Detailed Simulation
Late in
Design
Memocode 2009
Found Bug?
No
No
Sufficient
Coverage?
Yes
Done
Yes
No
Research Contributions
• Use verifiability as
additional metric
considered at early
DPM design stage
Verification Effort
• Compare verifiability of
different DPM schemes
• Evaluate trade-offs
between verification
effort, efficiency and
safety of DPM schemes
Performance
X
Memocode 2009
X
DPM Parameter
Outline
 Motivation & Proposed Approach
• Illustrative DPM Verification Examples
• Experiments and Results
• Conclusion
Memocode 2009
Considered DPM Scheme
• Goal: Maintain
multiprocessor power
usage below an
allocated budget
• Important problem for
multicores
– Increase in number of
cores  increase in
gap between average
and peak power use
Power
Budget
Global Controller
Actuate VDD,
Frequency
VDD
Freq
Monitor
Power Use
VDD
Freq
VDD
Freq
IPC
IPC
IPC
Core 1
Core 2
Core 3
Memocode 2009
Considered DPM Scheme
Power
Budget
• Global controller
Global
Controller
– Monitor power usage
– Actuate VDD and
Frequency of cores to
cap power
• Actuate VDD and
Frequency every
500us
• Actuate only
Frequency every
100us
Actuate VDD,
Frequency
Frequency
VDD
Global
Power Use
Max Power
Frequency
VDD
VDD
Frequency
IPC
IPC
IPC
Core 1
Core 2
Core 3
Actuate
Frequency
Actuate VDD
*
* *
*
Budget
1
Memocode 2009
Monitor
Power Use
2
3
4
5
6
7
8
9
10 11 12 13 14
Time
DPM Parameters and Verifiability
Utilization (IPC)
• Controller algorithm:
Budget
– Set next VDD and Frequency so
power usage < budget
+
Actuator
System
Approximate
Power Usage
f(IPC, VDD, Freq)
• Design parameters:
– Voltage levels, Frequency
levels, Cores per controller
– Homogeneous vs.
heterogeneous VDD values
• Questions:
Controller
2 Cores per controller
3 Cores per controller
– What is the impact on verifiability of above design decisions?
– What are the tradeoffs between performance, verifiability
and safety?
Memocode 2009
DPM Verification with PRISM Model Checker
• Model Description
– State variables
• Current VDD, Frequency, Utilization
values for all cores (~IPC)
• Possible State:
State
Variables
Transition
Rules
Correctness
Properties
Model
Checker
– One assignment of values to state
variables from their domain
• Reachable State:
0.2
– One assignment of values to state
variables allowed under DPM
– Probabilistic transition rules
• Probabilistic changes in utilization
– State rewards
• To each state, assign tokens
representing power & performance
Memocode 2009
0.4
0.3
0.4
0.6
0.1
0.2
0.4
0.4
1
NO
Correct?
YES
Done
DPM Verification with PRISM Model Checker
• Correctness Properties
– For every reachable state
• VDD and Frequency values matched
and within range
• No deadlock
State
Variables
Transition
Rules
Model
Checker
– Along model execution paths
• Power over budget < X% of total
power
• Performance loss < Y% of baseline
0.2
0.4
0.3
0.4
0.6
0.1
0.2
• Model Check
Correctness
Properties
0.4
0.4
1
NO
– Build model
• Reachable states, expected values
of rewards
– Check correctness properties
Memocode 2009
Correct?
YES
Done
Outline
 Motivation & Proposed Approach
 Illustrative DPM Verification Examples
• Experiments and Results
• Conclusion
Memocode 2009
Methodology
• Modeled 6 SPEC2000 benchmarks and their combinations
– Art, bzip, crafty, eon, mcf, parser
– Used probabilistic utilization transitions from simulation
– Budget set to 25%, 40%, 50%, 70%, 100% of maximum
• Trade-offs analysis
– Verifiability metric
• Number of reachable states and transitions
– Performance metric
• % Performance (Frequency) vs. baseline without DVFS
– Safety metrics
• % Power over budget of baseline system without DVFS
• % Intervals over budget
Memocode 2009
Results: Voltage Levels
2 CPC
3 CPC
95
% Power Excess
% Performance
1 CPC
93
91
89
87
85
2
3
4
5
6
5
4
3
2
1
0
2
3
10
8
6
4
2
0
2
3
4
5
6
Voltage Levels
5
6
Reachable States
% Intervals Over
Budget
Voltage Levels
4
1600
1400
1200
1000
800
600
400
200
0
Voltage Levels
2
3
4
Voltage Levels
Memocode 2009
5
6
Results: Freq. Levels per Voltage Level
2 CPC
3 CPC
95
% Power Excess
% Performance
1 CPC
93
91
89
87
85
1
2
3
4
5
10
8
6
4
2
0
1
2
3
4
4
3
2
1
0
1
2
3
4
5
Frequency Levels / Voltage Level
Reachable States
% Intervals Over
Budget
Frequency Levels / Voltage Level
5
1400
1200
1000
800
600
400
200
0
5
1
Frequency Levels / Voltage Level
2
3
4
5
Frequency Levels / Voltage Level
Memocode 2009
Conclusions
• Making design choices with verification in mind
does impact the resulting verification effort
• Adding verifiability as a separate metric to be
considered together with performance, reliability,
and safety may lead to different design choices
Memocode 2009
Thank You!
Memocode 2009