www.prismmodelchecker.org

Dynamic Power Management - IBM Disk Drive

(Benini, Bogliolo, Paleologo and De Micheli)

Contents

Specification:

This case study is based on a DTMC model of a IBM disk drive taken from [BBPM99]. As in [BBPM99] we suppose that the maximum size of the service request queue (SRQ) is 2.

The service provider (SP) has five different states which are shown below.

It is only in state active that the SP can perform data reads and writes. In state idle the disk is spinning while some of the electronic components of the disk drive have been switched off. The state idlelp (idle low power) is similar except that it has a lower power dissipation. The states stby and sleep correspond to the disk being spun down. The specification of the SP is given in the following tables.

  • Power Dissipation for states of the SP (W)

    active 2.5
    idle 1.5
    idlelp 0.8
    stby 0.3
    sleep 0.1
  • Expected transition times for state transitions of the SP

      active idle idlelp stby sleep
    active - 1ms 5ms 2.2sec 6sec
    idle 1ms - 5ms 2.2sec 6sec
    idlelp 5ms - - 2.2sec 6sec
    stby 2.2sec - - - 6sec
    sleep 6sec - - - -

Modelling the System in PRISM:

To model the system, we have chosen a time resolution of 1ms based on the fastest possible transition performed by the SP.

To model the PM issuing instructions to the SP, we split each time step of the system into two parts: in the first, the PM (instantaneously) decides what the SP should do next (based on the current state); and in the second, the system makes a transition (with the SP's move based on the choice made by the PM). To achieve this we include the following module:

module CLOCK

	c : [0..1];

	[tick1] c=0 -> (c'=1);
	[tick2] c=1 -> (c'=0);
	
endmodule
View: printable version          Download: power_dtmc_clock.pm

and construct the PM to synchronise with the CLOCK on tick1 and the remaining components of the system to synchronise with the clock on tick2.

Modelling the PM: As mentioned above the PM synchronises with the clock on tick1 and bases its choices on the current state of the system. Therefore the PM has the following form:

// POWER MANAGER 

module PM
	
	pm  :  [0..4]; 
	// 0 - go to active 
	// 1 - go to idle 
	// 2 - go to idlelp 
	// 3 - go to stby  
	// 4 - go to sleep 
	
	[tick1] cond1 -> p01 : (pm'=0) + p11 : (pm'=1) + p21 : (pm'=2) + p31 : (pm'=3) + p41 : (pm'=4);
	[tick1] cond2 -> p02 : (pm'=0) + p12 : (pm'=1) + p22 : (pm'=2) + p32 : (pm'=3) + p42 : (pm'=4);
	[tick1] cond3 -> p02 : (pm'=0) + p13 : (pm'=1) + p23 : (pm'=2) + p33 : (pm'=3) + p43 : (pm'=4);

endmodule
View: printable version          Download: power_dtmc_pm.pm

For example, if a state of the system satisfies cond1, then the PM decides that with probability p01 the SP moves to active, with probability p11 the SP moves to idle, with p21 to idlelp, p31 to stby, and p41 to sleep.

Modelling the SP: Recall that the SP synchronises with the clock on tick2 and the behaviour of the SP depends on the PM. Furthermore, since a time resolution of 1ms has been chosen, to correctly model transitions with delays longer than this time resolution, transient states are introduced. For example, the transient state active_idlelp is used to model the non-unitary time transition from active to idlelp. Note that, we suppose that the power dissipation in these transient states is high (2.5W). The module representing the SP has the following form:

// SERVICE PROVIDER

module SP 

	sp : [0..10] init 9;
	// 0 active
	// 1 idle
	// 2 active_idlelp
	// 3 idlelp
	// 4 idlelp_active
	// 5 active_stby
	// 6 stby
	// 7 stby_active
	// 8 active_sleep
	// 9 sleep
	// 10 sleep_active
	
	// states where PM has no control (transient states)
	[tick2] sp=2  -> 0.75   : (sp'=2) + 0.25   : (sp'=3);  // active_idlelp
	[tick2] sp=4  -> 0.25   : (sp'=0) + 0.75   : (sp'=4);  // idlelp_active
	[tick2] sp=5  -> 0.995  : (sp'=5) + 0.005  : (sp'=6);  // active_stby
	[tick2] sp=7  -> 0.005  : (sp'=0) + 0.995  : (sp'=7);  // stby_active
	[tick2] sp=8  -> 0.9983 : (sp'=8) + 0.0017 : (sp'=9);  // active_sleep
	[tick2] sp=10 -> 0.0017 : (sp'=0) + 0.9983 : (sp'=10); // sleep_active

	// states where PM has control
	// goto_active
	[tick2] sp=0 & pm=0 -> (sp'=0); // active
	[tick2] sp=1 & pm=0 -> (sp'=0); // idle
	[tick2] sp=3 & pm=0 -> (sp'=4); // idlelp
	[tick2] sp=6 & pm=0 -> (sp'=7); // stby
	[tick2] sp=9 & pm=0 -> (sp'=10); // sleep
	// goto_idle
	[tick2] sp=0 & pm=1 -> (sp'=1); // active
	[tick2] sp=1 & pm=1 -> (sp'=1); // idle
	[tick2] sp=3 & pm=1 -> (sp'=3); // idlelp
	[tick2] sp=6 & pm=1 -> (sp'=6); // stby
	[tick2] sp=9 & pm=1 -> (sp'=9); // sleep
	// goto_idlelp
	[tick2] sp=0 & pm=2 -> (sp'=2); // active
	[tick2] sp=1 & pm=2 -> (sp'=2); // idle
	[tick2] sp=3 & pm=2 -> (sp'=3); // idlelp
	[tick2] sp=6 & pm=2 -> (sp'=6); // stby
	[tick2] sp=9 & pm=2 -> (sp'=9); // sleep
	// goto_stby
	[tick2] sp=0 & pm=3 -> (sp'=5); // active
	[tick2] sp=1 & pm=3 -> (sp'=5); // idle
	[tick2] sp=3 & pm=3 -> (sp'=5); // idlelp
	[tick2] sp=6 & pm=3 -> (sp'=6); // stby
	[tick2] sp=9 & pm=3 -> (sp'=9); // sleep
	// goto_sleep
	[tick2] sp=0 & pm=4 -> (sp'=8); // active
	[tick2] sp=1 & pm=4 -> (sp'=8); // idle
	[tick2] sp=3 & pm=4 -> (sp'=8); // idlelp
	[tick2] sp=6 & pm=4 -> (sp'=8); // stby
	[tick2] sp=9 & pm=4 -> (sp'=9); // sleep
	  
endmodule
View: printable version          Download: power_dtmc_sp.pm

Modelling the SR and SRQ: As mentioned above, both the SRQ and the SR will synchronise with the clock on tick2. The SR has two states: idle, where no requests are generated; and 1req, where one request is generated per time step (1ms). The transitions between these states are based on time-stamped traces of disk access measured on real machines. The module of the SR is given by:

// SERVICE REQUESTER
module SR

	sr : [0..1] init 0; // 0 - idle and 1 - 1req
	
	[tick2] sr=0 -> 0.898: (sr'=0) + 0.102: (sr'=1);
	[tick2] sr=1 -> 0.454: (sr'=0) + 0.546: (sr'=1);

endmodule
View: printable version          Download: power_dtmc_sr.pm

In the case of the SRQ, to model the arrival and service of requests the transitions of the SRQ are dependent on the state of both the SR and the SP. Since, either the SR is in state idle and no requests arrive or in state 1req and one request arrives, and the SP can only serve requests when it is in state active, the module of the SRQ is as given below:

// SERVICE REQUEST QUEUE
module SRQ

	q : [0..2] init 0;
	
	[tick2] sr=0 & sp>0 -> true; // do not serve and nothing arrives
	[tick2] sr=1 & sp>0 -> (q'=min(q+1,2)); // do not serve and a request arrives
	[tick2] sr=0 & sp=0 -> (q'=max(q-1,0)); // serve and nothing arrives
	[tick2] sr=1 & sp=0 -> true; // serve and a request arrives arrives

endmodule
View: printable version          Download: power_dtmc_srq.pm

Reward Structures: We include the following reward structures for the power consumption, queue size and number of lost requests.

// power consumption
rewards "power"

	sp=0 & c=1 : 2.5;
	sp=1 & c=1 : 1.5;
	sp=2 & c=1 : 2.5;
	sp=3 & c=1 : 0.8;
	sp=4 & c=1 : 2.5;
	sp=5 & c=1 : 2.5;
	sp=6 & c=1 : 0.3;
	sp=7 & c=1 : 2.5;
	sp=8 & c=1 : 2.5;
	sp=9 & c=1 : 0.1;
	sp=10 & c=1 : 2.5;

endrewards

// queue size
rewards "queue"

	c=1 : q;

endrewards

// customers lost
rewards "lost"

	[tick2] q=2 & sr=1 & sp>0 : 1;

endrewards

// time
rewards "time"

    [tick2] true : 1;

endrewards
View: printable version          Download: power_dtmc_rewards.pm

Optimal Stochastic Policies:

The policies we have calculated are the optimum policies for minimizing power consumption under different performance constraints, where these constraints concern the average number of requests awaiting service. In addition, we suppose that there is a time horizon of one million time steps. To model this horizon we include an additional module representing a battery which has an expected life span of 1 million time steps.

// BATTERY
module BAT

	bat : [0..1] init 1; // 0 empty, 1 - operational
	
	[] bat=0 -> (bat'=0); // loop when battery empty
	[tick2] bat=1 -> 0.000001 : (bat'=0) + 0.999999 : (bat'=1);

endmodule
View: printable version          Download: power_dtmc_battery.pm

Note that, once the battery reaches state 0 it cannot perform the action tick2 which prevents the rest of the system performing the action tick2, and hence prevents the rest of the system from moving (i.e. the states where bat=0 act as sink states).

We obtained these policies by constructing the generator matrix of the system in PRISM and then, from this, constructing a linear optimization problem which we solve with Maple using its Simplex package.

Results:

We have computed the following performance measures for the optimal policies under different constraints:

  • The average power consumption, average number of requests awaiting service and average number of lost requests (see here and here for graphs comparing power against performance).
  • The expected power consumption by time T (see here for the results).
  • The expected number of requests awaiting service at time T (see here for the results).
  • The expected number of lost requests by time T (see here for the results).
  • The probability, starting from the initial state, that more than N requests are awaiting service by time T (see here for the the case when N=1 and here for N=2).

The above properties can be represented in the PRISM specification language as follows.

const int T; // time
const int K; // queue size

// average power consumption
R{"power"}=?[ F (bat=0) ]/R{"time"}=?[ F (bat=0) ]

// average queue size
R{"queue"}=?[ F (bat=0) ]/R{"time"}=?[ F (bat=0) ]

// average number of lost requests
R{"lost"}=?[ F (bat=0) ]/R{"time"}=?[ F (bat=0) ]

// the expected power consumption by time T
R{"power"}=?[ C<=2*T ]

// the expected number of requests awaiting service at time T .
R{"queue"}=?[ I=2*T ]

// the expected number of lost requests by time T .
R{"lost"}=?[ C<=2*T ]

// probability queue of size k before time T
P=?[ F q=K ]
View: printable version          Download: power_dtmc.pctl

The remaining properties below, reduce to calculating reachability probabilities after augmenting the model with a variable to record the property of interest.

  • The probability that a request is served by time T, given that it arrived into a certain position in the queue (see here for the case when the request arrives into the first position in the queue, and here for the request arrving into the second position in the queue).
  • From the initial state, the probability that N requests get lost by time T (see here for the results when N=500 and here in the case that N=1,000).

Case Studies