Dynamic Power Management - IBM Disk Drive

[andrea.t...@studenti.unicam.it]

Hi,

I am studying PRISM case study of Dynamic Power Management - IBM Disk Drive. I downloaded all module files (6 modules) and put them together in PRISM. However there are some syntax error in module SP that are defined as follow:

// 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 

The error is sp', in fact for each of the case of goto to sleep, stby, active idle there is this variable and it's return an error. How can I solve this problem? 

[Gethin Norman]

The problem is that brackets are missing each update of sp should be in brackets, e.g.

> [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

(The model used an old version which allowed the updates to be defined without brackets.)

I have updated the webpage so these should now be fixed.

thanks

Gethin

> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[andrea.t...@studenti.unicam.it]

Hi,

I am studying PRISM case study of Dynamic Power Management - IBM Disk Drive. I downloaded all module files (6 modules) and put them together in PRISM. However there are some syntax error in module PM; that are defined as follow: 

// 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

The errors are cond1, cond2 and cond3 because these variables aren't declared. So, how can I solve this problem? Are these variables considered as booleans variables (TRUE)? Moreover, in this module there are p01, p11,p21 and so on that are probability, what is the value of these probabilities?

[Gethin Norman]

This has come up before before see my replies in the discussion:

https://groups.google.com/forum/#!topic/prismmodelchecker/eW-m2K8qp9g

thanks

Gethin

[andrea.t...@studenti.unicam.it]

So, I must copy inside my model this behavior:

module PM // policy when constraint on queue size equals 0.05 

pm : [0..4]; // 0 − go to active, 1 − go to idle, 2 − go to idlelp, 3 − go to standby, 4 − go to sleep 

[tick1] sr=0 ∧ sp=0 ∧ q=0 → 0.63683933 : (pm0=0) // go to active + 0.36316067 : (pm0=1); // go to idle 

[tick1] sp=1 ∨ sp=9 → (pm0=0); // go to active 

[tick1] ¬(sp=9 ∨ sp=1 ∨ (sr=0 ∧ sp=0 ∧ q=0)) → (pm0=pm); 

endmodule 

I have the necessary to have a correct model because I should module this scenario with another language and then do a match between this two scenarios. 

Thanks

[Gethin Norman]

If you want the power manager policy that optimises power consumption under the requirement that the expected queue size is less than or equal to 0.05, then yes this is the power manager module you need. Other policies are also included in the paper (see table 3).

thanks

Gethin

[andrea.t...@studenti.unicam.it]

I'm testing the pctl property for this case study but it returns me some errors. I know that is a non deterministic model and for this reason I change R with Rmin o Rmax but it doesn't work! How can I solve this?

[Gethin Norman]

Andrea,

can you let us know what the errors are (without knowing what the errors are, I cannot see how we can help you).

thanks

Gethin