Use the PRISM simulator to generate some random paths through the model. Then, have a look at the definition of the SQĪnd try to understand what they describe.ĭownload the model file power.sm from above and load it into PRISM. Read the section on synchronisation in the manual. (in square brackets at the start of the line). Secondly, notice that all the commands are labelled with actions Which is a constant defined just above in the file. Which describes the arrival of a request into the queue, The first command in the module SQ, for example, There are a couple of important things to note.įirstly, since this is a CTMC, updates in guarded commands are labelled with rates, not probabilities. Presently, we just have two modules, representing the Service Queue (SQ) and Service Provider (SP). This model is a continuous-time Markov chain (CTMC),Īs denoted by the keyword at the start of the file. View: printable version Download: power.sm sp= 2 -> rate_serve : ( sp'= 1) Įndmodule //- // Reward structures rewards " queue_size" If in other power states when a request arrives, do nothing // (need to add this explicitly because otherwise SP blocks SQ from moving) Synchronise with service queue (SQ): // If in the idle state, switch to busy when a request arrives in the queue Module SP // Power state of SP: 0=sleep, 1=idle, 2=busy sp : init 1 The SP has 3 power states: sleep, idle and busy // Rate of service (average service time = 0.008s) const double rate_serve = 1/ 0.008 true -> rate_arrive : ( q'= min( q+ 1, q_max)) Įndmodule //- // Service Provider (SP) // Processes requests from service queue. Request arrival rate const double rate_arrive = 1/ 0.72 // (mean inter-arrival time is 0.72 seconds) module SQ // q = number of requests currently in queue q : init 0 Maximum queue size const int q_max = 20 International Symposium on Low Power Electronics and Design, pages 194-199, ACM Press, 1999 ctmc //- // Service Queue (SQ) // Stores requests which arrive into the system to be processed. Simple dynamic power management (DPM) model // Based on: // Qinru Qiu, Qing Wu and Massoud Pedram // Stochastic modeling of a power-managed system: Construction and optimization // Proc. Our initial PRISM model is the following: Switches between power states are either performed by the Service Provider itselfĪ good strategy for switching between these states will be one that keeps power consumptionĪs low as possible whilst maintaining an acceptable level of service. The idea is these three states have different power consumptionsīut also different response times when a service is to be performed. The Service Provider has several different power states, The Service Provider (SP) which responds to these requests (read/write requests to the disk in this case), The Service Queue (SQ) into which requests for a particular service are placed The DPM system comprises three components: We describe the DPM system in a fairly generic way. This example is actually based on a specific case study from the literature -Ī Fujitsu disk drive with 3 power states - but in the following, Which are sets of instructions used to switch between different power states of computing devices. This example concerns dynamic power management (DPM) schemes,
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |