www.prismmodelchecker.org

Real-Time Dynamic Voltage Scaling

(Pillai and Shin)

Contents

Related publications: [KNP05c]

Introduction:

This case study concerns the performance of real-time embedded systems under dynamic voltage scaling schedulers. Dynamic voltage scaling is a technique used to address the trade-off between the battery life and the performance of battery powered processors.

In the classic model of real-time embedded systems we have a set of tasks T1,...Tn that need to be executed periodically. Each task Ti has an associated period (Pi) and worst case execution time (Ci). The task Ti is released every Pi time units and is required to complete its execution before some deadline which is typically defined as the end of its period, i.e. it must finish before its next release. A real time scheduler must guarantee that tasks will meet their deadline given that both the task set is schedulable and no task exceeds its worst case computation time.

Schedulers:

The real-time DVS schedulers we consider are taken from [PS01], which are based on two of the standard real-time schedulers, namely Rate Monotonic (RM) and Earliest-Deadline First (EDF) schedulers.

  • RM schedulers are static and assign the task priority according to the period of the tasks - they always select the task with the shortest period that is ready to run.
  • EDF schedulers are dynamic and order tasks by their deadlines, giving highest priority to the released task with the most immediate deadline.

As in [PS01], we assume that the task deadline equals the period, scheduling and preemption overheads are negligible and the tasks are independent.

Static voltage scaling schedulers

The first schedulers that [PS01] consider simply extend RM and EDF by selecting the lowest possible operating frequency that will allow the scheduler to meet all the deadlines of the task set. The frequency is set statically and is only changed when the task set is changed.

When selecting the operating frequency, one must take into account that, if the frequency is scaled by a factor of α(∈(0,1]), then the worst case execution time is scaled by a factor of 1/α, while the period and deadline remain unchanged. Extending the standard schedulability tests for RM and EDF schedulers in [PS01], the following static voltage scaling algorithms were reached:

Static_RM:

rm_test(α):
    if (∀ Ti ∈ { T1, … ,Tn | P1≤ … ≤Pn }. ceil(Pi/P1) × C1 + … + ceil(Pi/Pi) × Ci ≤ α) return true
    else return false

select_frequency
    use lowest frequency fi such that RM_test(fi/f1) is true

Static_EDF:

edf_test(α):
    if (C1/P1+ … +Cn/Pn ≤ α) return true
    else return false

select_frequency
    use lowest frequency fi such that EDF_test(fi/f1) is true

Cycle conserving schedulers

In general tasks are completed far sooner than their worst case execution time and the following algorithms of [PS01] aim to take advantage of this. In particular, when a task uses less than its worst case execution time, the scheduler can use this fact to reduce the operating frequency. Note that, when a task is released for execution we do not know how much computation time it will require, and therefore at this point the algorithms make the conservative assumption that the task will require its worst case execution time. However, when a task completes, one can calculate the number of cycles that were not required by the task, and hence at this time the algorithms recalculate the frequency taking into account these unused cycles (hence the term "cycle conserving").

Below, we give the cycle conserving extensions of the RM and EDF schedulers introduced in [PS01].

Cycle_Conserving_RM:

assume fj is the frequency set by the static scaling algorithm

select_frequency:
    set sm to the maximum cycles until the next deadline
    use lowest frequency fi such that
    (d1+ … +dn) / smfi/fm

upon task_release(Ti):
    set c_lefti to Ci
    set cm to the maximum cycles until the next deadline
    set sj to sm × fi/fm
    allocate_cycles(sm)
    select_frequency

upon task_completion(Ti):
    set c_lefti to 0
    set di to 0
    select_frequency

during_task_execution(Ti):
    decrement c_lefti and di

allocate_cycles(k):
    for i=1 to n, Ti ∈ { T1, … Tn | P1 ≤ … ≤ Pn }   // tasks sorted by period
        if c_lefti < k
            set di equal to c_lefti
            set k equal to k-c_lefti
        else
            set di equal to k
            set k equal to 0


Cycle_Conserving_EDF:

select_frequency:
    use lowest frequency fi such that
    (U1+ … +Unfi/f1)

upon task_release(Ti):
    set Ui to Ci/Pi
    select_frequency

upon task_completion(Ti):
    set Ui to ci/Pi where ci equals the actual cycles used in the invocation
    select_frequency

PRISM Models:

For this case study, we consider a processor with three operating frequencies, 1, 0.75 and 0.5, with corresponding voltages 5,4 and 3. The task set is of size three with the following parameters:

task:   Pi (period) Ci (WCET)
T18 3
T2103
T3141

To model the system in PRISM, we discretise time and, to simplify the modelling process, the division of one time unit is such that, for each of the possible frequencies, the number of discrete time steps required by a task to finish on its WCET is an integer. For example, if a task is run at the frequency 0.75 and the task takes WCET time units, it will require WCET*4/3 time units to complete. Furthermore, we suppose that the completion time distribution of a task is uniformly distributed between 1 and its WCET.

By way of example, the PRISM models for the EDF schedulers are given below.

Static EDF model

// MODEL OF REAL TIME DYNAMIC VOLTAGE SCALING SYSTEM
// static edf scheduler (chooses job with the most immediate deadline)
// gxn/dxp 11/11/03

// non-deterministic (may have cases when two or more jobs have the same deadline)
mdp

//-------------------------------------------------------------------------------------------------
// FREQUENCIES (assume Vi greater than Vj if i<j)
const double V1 = 1;   // corresponding voltage is 5
const double V2 = 3/4; // corresponding voltage is 4
const double V3 = 1/2; // corresponding voltage is 3

//-------------------------------------------------------------------------------------------------
// DISCRETISE TIME
// choose a division of one time unit (one time step) such that to finish on WCET 
// is an integer when the task is run on any of the frequencies
// (e.g. WCET at frequency 3/4 is now WCET*4/3 time steps)
const int N=3;
// rescale units of work such that in one step an integer amount of work is done
// since depending on the frequency the work in one time unit is 1, 3/4 or 1/2 
// we scale by 4 to get integer values
const int K=4; 
// for frequencies V1, V2 and V3 in one time unit we now do 4,3 or 2 units of work respectively

//-------------------------------------------------------------------------------------------------
// CONSTANTS OF THE SYSTEM (assume task deadline equals the period)
// scaled by the chosen discrete time step
const int P1=8*N; // period of the first task
const int C1=3*N; // worst case execution time of the first task
const int T1=3*(K*N); // worst case execution time of the first task (scaled by units of work)

const int P2=10*N; // period of the second task
const int C2=3*N;  // worst case execution time of the second task
const int T2=3*(K*N); // worst case execution time of the second task (scaled by units of work)

const int P3=14*N; // period of the third task
const int C3=1*N;  // worst case execution time of the third task
const int T3=1*(K*N); // worst case execution time of the third task (scaled by units of work)

//-------------------------------------------------------------------------------------------------
// WHEN TO CHOOSE WHAT FREQUENCY
// fi=0 means that process i has not finished in its current period
formula frequency1 = !frequency2 & !frequency3 & ((C1/P1 + C2/P2 + C3/P3) <= V1); // frequency V1
formula frequency2 = !frequency3 & ((C1/P1 + C2/P2 + C3/P3) <= V2); // frequency V2
formula frequency3 = ((C1/P1 + C2/P2 + C3/P3) <= V3); // frequency V3

// WHO TO SCHEDULE
// task with nearest deadline (fi=0 if task i has not finished)
// (only consider task1 get remaining formulae through renaming)
formula schedule   = f1=0 & (!f2=0 | (d1<=d2)) & (!f3=0 | (d1<=d3)); // schedule task1
formula noschedule = f1=1 & f2=1 & f3=1; // schedule nothing

// probabilities of finishing in one time step (uniformly distributed)
// only consider task1 get remaining probabilities through renaming
formula finish1  = min(V1*K/(T1-t1),1); // running at frequency 1 (do 4 units of work)
formula finish2  = min(V2*K/(T1-t1),1); // running at frequency 2 (do 3 units of work)
formula finish3  = min(V3*K/(T1-t1),1); // running at frequency 3 (do 2 units of work)

//-------------------------------------------------------------------------------------------------
// MODULE FOR FIRST TASK
module task1
	
	d1 : [1..P1] init P1; // time until next period
	t1 : [0..T1] init 0; // work done (time spent running scaled by the frequency)
	f1 : [0..2]  init 0; // state of task in current period 
	// 0 - not finished
	// 1 - finished 
	// 2 - error: not finished and period over
	
	// TASK BEING PERFORMED (cost is the voltage squared)
	// task is being performed at frequency 1
	[step1] schedule & frequency1 & d1>1 -> 
	  (1-finish1) : (d1'=d1-1) & (t1'=t1+4) // not finished
	    + finish1 : (d1'=d1-1) & (f1'=1) & (t1'=0); // finished
	[step1] schedule & frequency1 & d1=1 ->
	  (1-finish1) : (f1'=2)  // not finished (and error)
	    + finish1 : (d1'=P1) & (f1'=0) & (t1'=0); // finished
	// task is being performed at frequency 0.75
	[step1] schedule & frequency2 & d1>1 -> 
	  (1-finish2) : (d1'=d1-1) & (t1'=t1+3) // not finished
	    + finish2 : (d1'=d1-1) & (f1'=1) & (t1'=0); // finished
	[step1] schedule & frequency2 & d1=1 -> 
	  (1-finish2) : (f1'=2)  // not finished (and error)
	    + finish2 : (d1'=P1) & (f1'=0) & (t1'=0); // finished
	// task is being performed at frequency 0.5
	[step1] schedule & frequency3 & d1>1 -> 
	  (1-finish3) : (d1'=d1-1) & (t1'=t1+2) // not finished
	    + finish3 : (d1'=d1-1) & (f1'=1) & (t1'=0); // finished
	[step1] schedule & frequency3 & d1=1 -> 
	  (1-finish3) : (f1'=2)  // not finished (and error)
	    + finish3 : (d1'=P1) & (f1'=0) & (t1'=0); // finished
	  
	// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - task 2 is running
	// deadline goes down
	[step2] d1>1 -> (d1'=d1-1);
	// end of period and finished task - move to next period
	[step2] d1=1 & f1=1 -> (d1'=P1) & (f1'=0);
	// end of period and not finished - error
	[step2] d1=1 & f1=0 -> (f1'=2); 
	// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - task 3 is running
	// deadline goes down
	[step3] d1>1 -> (d1'=d1-1);
	// end of period and finished task - move to next period
	[step3] d1=1 & f1=1 -> (d1'=P1) & (f1'=0);
	// end of period and not finished - error
	[step3] d1=1 & f1=0 -> (f1'=2);
	// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - no task is running
	// deadline goes down 
	[step] noschedule & d1>1 -> (d1'=d1-1);
	// end of period and finished task - move to next period
	[step] noschedule & d1=1 -> (d1'=P1) & (f1'=0);
	
endmodule

//-------------------------------------------------------------------------------------------------
// CONSTRUCT OTHER TASKS THROUGH RENAMING

module task2=task1[
	  d1=d2, d2=d3, d3=d1,
	  t1=t2,
	  f1=f2, f2=f3, f3=f1,
	  P1=P2, P2=P3, P3=P1,
	  T1=T2,
	  step1=step2, step2=step3, step3=step1 ]
	  
endmodule

module task3=task1[
	  d1=d3, d2=d1, d3=d2,
	  t1=t3,
	  f1=f3, f2=f1, f3=f2,
	  P1=P3, P2=P1, P3=P2,
	  T1=T3,
	  step1=step3, step2=step1, step3=step2 ]
	  
endmodule

//-------------------------------------------------------------------------------------------------
// REWARDS - related to power consumption (equals square of current voltage)

rewards "power"
	
	// task performed at frequency 1 (voltage is 5)
	[step1] frequency1 & !noschedule : 25;
	[step2] frequency1 & !noschedule : 25;
	[step3] frequency1 & !noschedule : 25;
	// task performed at frequency 3 (voltage is 4)
	[step1] frequency2 & !noschedule : 16;
	[step2] frequency2 & !noschedule : 16;
	[step3] frequency2 & !noschedule : 16;
	// task performed at frequency 3 (voltage is 3)
	[step1] frequency3 & !noschedule : 9;
	[step2] frequency3 & !noschedule : 9;
	[step3] frequency3 & !noschedule : 9;
	
endrewards
View: printable version          Download: static_edf.nm

Cycyle Conserving EDF model

// MODEL OF REAL TIME DYNAMIC VOLTAGE SCALING SYSTEM
// cyclic conserving edf scheduler (chooses job with the most immediate deadline)
// gxn/dxp 11/11/03

// non-deterministic since may be cases when two or more jobs have the same deadline
mdp

//-------------------------------------------------------------------------------------------------
// FREQUENCIES (assume Vi greater than Vj if i<j)
const double V1 = 1;   // corresponding voltage is 5
const double V2 = 3/4; // corresponding voltage is 4
const double V3 = 1/2; // corresponding voltage is 3

//-------------------------------------------------------------------------------------------------
// DISCRETISE TIME
// choose a division of one time unit (one time step) such that to finish on WCET 
// is an integer when the task is run on any of the frequencies
// (e.g. WCET at frequency 3/4 is now WCET*4/3 time steps)
const int N=3;
// rescale units of work such that in one step an integer amount of work is done
// since depending on the frequency the work in one time unit is 1, 3/4 or 1/2 
// we scale by 4 to get integer values
const int K=4; 
// for frequencies V1, V2 and V3 in one time unit we now do 4,3 or 2 units of work respectively

//-------------------------------------------------------------------------------------------------
// CONSTANTS OF THE SYSTEM (assume task deadline equals the period)
// scaled by the chosen discrete time step
const int P1=8*N; // period of the first task
const int C1=3*N; // worst case execution time of the first task
const int T1=3*(K*N); // worst case execution time of the first task (scaled by units of work)

const int P2=10*N; // period of the second task
const int C2=3*N;  // worst case execution time of the second task
const int T2=3*(K*N); // worst case execution time of the second task (scaled by units of work)

const int P3=14*N; // period of the third task
const int C3=1*N;  // worst case execution time of the third task
const int T3=1*(K*N); // worst case execution time of the third task (scaled by units of work)

//-------------------------------------------------------------------------------------------------
// WHEN TO CHOOSE WHAT FREQUENCY
// fi=0 means that process i has not finished in its current period
formula frequency1 = !frequency2 & !frequency3 & ((u1/P1 + u2/P2 + u3/P3) <= V1);// frequency V1
formula frequency2 = !frequency3 & ((u1/P1 + u2/P2 + u3/P3) <= V2); // frequency V2
formula frequency3 = ((u1/P1 + u2/P2 + u3/P3) <= V3); // frequency V3

// WHO TO SCHEDULE
// task with nearest deadline (fi=0 if task i has not finished)
// only consider task1 get remaining formulae through renaming
formula schedule   = f1=0 & (!f2=0 | (d1<=d2)) & (!f3=0 | (d1<=d3)); // schedule task1
formula noschedule = f1=1 & f2=1 & f3=1; // schedule nothing

// probabilities of finishing in one time step (uniformly distributed)
// only consider task1 get remaining probabilities through renaming
formula finish1  = min(4/(T1-w1),1); // running at frequency 1 (4 units of work)
formula finish2  = min(3/(T1-w1),1); // running at frequency 2 (3 units of work)
formula finish3  = min(2/(T1-w1),1); // running at frequency 3 (2 units of work)

//-------------------------------------------------------------------------------------------------
// MODULE FOR FIRST TASK
module task1
	
	d1 : [1..P1] init P1; // time until next period
	f1 : [0..2]  init 0; // state of task in current period
	// 0 - not finished
	// 1 - finished 
	// 2 - error (not finished and period over)
	w1 : [0..T1] init 0; // work done (time spent running scaled by the frequency)
	t1 : [0..C1] init 0; // time spent running
	u1 : [0..C1] init C1; // used to decide who to schedule
	
	// TASK BEING PERFORMED
	// task is being performed at frequency 1
	[step1] schedule & frequency1 & d1>1 ->
	  (1-finish1) : (d1'=d1-1) & (w1'=w1+4) & (t1'=min(t1+1,C1)) // not finished
	    + finish1 : (d1'=d1-1) & (t1'=0) & (f1'=1) & (w1'=0) & (u1'=min(t1+1,C1)); // finished
	[step1] schedule & frequency1 & d1=1 ->
	  (1-finish1) : (f1'=2)  // not finished (and error)
	    + finish1 : (d1'=P1) & (t1'=0) & (f1'=0) & (w1'=0) & (u1'=C1); // finished
	// task is being performed at frequency 0.75
	[step1] schedule & frequency2 & d1>1 ->
	  (1-finish2) : (d1'=d1-1) & (w1'=w1+3) & (t1'=min(t1+1,C1)) // not finished
	    + finish2 : (d1'=d1-1) & (t1'=0) & (f1'=1) & (w1'=0) & (u1'=min(t1+1,C1)); // finished
	[step1] schedule & frequency2 & d1=1 ->
	  (1-finish2) : (f1'=2)  // not finished (and error)
	    + finish2 : (d1'=P1) & (t1'=0) & (f1'=0) & (w1'=0) & (u1'=C1); // finished
	// task is being performed at frequency 0.5
	[step1] schedule & frequency3 & d1>1 ->
	  (1-finish3) : (d1'=d1-1) & (w1'=w1+2) & (t1'=min(t1+1,C1)) // not finished
	    + finish3 : (d1'=d1-1) & (t1'=0) & (f1'=1) & (w1'=0) & (u1'=min(t1+1,C1)); // finished
	[step1] schedule & frequency3 & d1=1 -> 
	  (1-finish3) : (f1'=2)  // not finished (and error)
	    + finish3 : (d1'=P1) & (t1'=0) & (f1'=0) & (w1'=0) & (u1'=C1); // finished
	// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - task 2 is running
	// deadline goes down
	[step2] d1>1 -> (d1'=d1-1);
	// end of period and finished task - move to next period
	[step2] d1=1 & f1=1 -> (d1'=P1) & (f1'=0) & (u1'=C1);
	// end of period and not finished - error
	[step2] d1=1 & f1=0 -> (f1'=2); 
	// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - task 3 is running
	// deadline goes down
	[step3] d1>1 -> (d1'=d1-1);
	// end of period and finished task - move to next period
	[step3] d1=1 & f1=1 -> (d1'=P1) & (f1'=0) & (u1'=C1);
	// end of period and not finished - error
	[step3] d1=1 & f1=0 -> (f1'=2);
	// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - no task is running
	// deadline goes down 
	[step] noschedule & d1>1 -> (d1'=d1-1);
	// end of period and finished task - move to next period
	[step] noschedule & d1=1 -> (d1'=P1) & (f1'=0) & (u1'=C1);
	
endmodule

//-------------------------------------------------------------------------------------------------
// CONSTRUCT OTHER TASKS THROUGH RENAMING
// task 2
module task2=task1[
	  d1=d2, d2=d3, d3=d1,
	  u1=u2, u2=u3, u3=u1,
	  t1=t2,
	  w1=w2,
	  f1=f2, f2=f3, f3=f1,
	  P1=P2, P2=P3, P3=P1,
	  C1=C2, C2=C3, C3=C1,
	  T1=T2,
	  step1=step2, step2=step3, step3=step1 ]
	  
endmodule
// task 3
module task3=task1[
	  d1=d3, d2=d1, d3=d2,
	  u1=u3, u2=u1, u3=u2,
	  t1=t3,
	  w1=w3,
	  f1=f3, f2=f1, f3=f2,
	  P1=P3, P2=P1, P3=P2,
	  C1=C3, C2=C1, C3=C2,
	  T1=T3,
	  step1=step3, step2=step1, step3=step2 ]
	  
endmodule

//-------------------------------------------------------------------------------------------------
// REWARDS - related to power consumption (equals square of current voltage)

rewards "power"
	// task performed at frequency 1 (voltage is 5)
	[step1] frequency1 & !noschedule : 25;
	[step2] frequency1 & !noschedule : 25;
	[step3] frequency1 & !noschedule : 25;
	// task performed at frequency 3 (voltage is 4)
	[step1] frequency2 & !noschedule : 16;
	[step2] frequency2 & !noschedule : 16;
	[step3] frequency2 & !noschedule : 16;
	// task performed at frequency 3 (voltage is 3)
	[step1] frequency3 & !noschedule : 9;
	[step2] frequency3 & !noschedule : 9;
	[step3] frequency3 & !noschedule : 9;
	
endrewards
View: printable version          Download: cc_edf.nm

Model Statistics

The table below shows statistics for each model we have built. The first section gives the number of states in the MDP representing the model. The second part refers to the MTBDD which represents this MDP: the total number of nodes and the number of leaves (terminal nodes).

Scheduler:   States: Nodes: Leaves:
Static RM 2,761 10,984 17
Static EDF 12,692 63,845 23
Cycle Conserving RM 6,621 158,61275
Cycle Conserving EDF202,607381,86887

Model Construction Times

The table below gives the times taken to construct the models. There are two stages. Firstly, the system description (in our module-based language) is parsed and converted to the MTBDD representing it. Secondly, reachability is performed to identify non-reachable states and the MTBDD is filtered accordingly. Reachability is performed using a BDD based fixpoint algorithm. The number of iterations for this process is also given.

Scheduler:   Construction:   Reachability:
Time (s): Iter.s: Time per iter. (s):
Static RM 5.73840 0.006
Static EDF 27.2840 0.027
Cycle Conserving RM 7941,0000.67
Cycle Conserving EDF 327840 0.25

Results:

We analyse the different schedulers by comparing the (maximum) expected cost by time T as T varies. The cost function we consider is given by the square of the current voltage since this value is proportional to the energy consumption (see PRISM modules given above).

The graphs below plot the expected costs for the different schedulers as T varies. The results show a similar pattern to those reached through simulation in [PS01]: the EDF based approach can lead to greater power savings compared to the RM based algorithms.

graph of expected cost (small time bound)
graph of expected cost (small large bound)

Case Studies