Load Balancing Monitor

  • Description
  • HyTech Code for the associated EFSM (see full paper)
  • DMC Code for the associated EFSM
    LBM
    Load Balancing Monitor

    Description
    The figure shows an abstraction of a multiprocess system with a load balancing monitor. In the initial configuration of the system the processes are in state req, whereas the monitor is in state idle. When the monitor broadcasts the message swap\_out (and moves to busy all processes in the CPU are suspended. Two different priorities are assigned to the suspended processes. This is simulated through the non-deterministic reaction to swap-out with target states {high,low}. When the CPU is released by the monitor (through the broadcast release), it is assigned to processes with high priority. Processes with low-priority go back to the request state. This behaviour is simulated through the deterministic reaction to the broadcast swap_in.
    HyTech Code
    
    --- LOAD BALANCING MONITOR 
    
    var  req,use,high,low,idle,busy: discrete;  	
    
    automaton p
    synclabs : ;
    
    initially ss & True;
               
    
    loc ss : while req >= 0 & use >=0 & idle >=0 & busy >=0 &  
                   high >= 0 & low >=0 wait {} 
             when req >=1 & idle >=1 
             do {req'=req-1,use'=use+1} goto ss;
             when use >=1 & idle >=1 
             do {req'=req+1,use'=use-1} goto ss;
             when idle >=1  
             do {
                 idle'=idle-1,
                 busy'=busy+1,
                 high'+low'=high+low+use,
                 high'>=high,
                 use'=0
             } 
              goto ss;
             when busy >=1  
             do {busy'=busy-1,
                 idle'=idle+1,
                 high'=0,
                 low'=0,
                 use'=use+high,
                 req'=req+low
             } 
             goto ss;
    end
    
    var 
       init_reg, final_reg, reached, old, new, Aux : region;
    
    init_reg  := loc[p]=ss & idle=1 & busy=0 & req>=0 &
                             use =0 & high=0 & low=0 ;
    final_reg := loc[p]=ss & use >=1 & busy >= 1;
    
    reached:= reach backward from final_reg endreach;
    
    if empty(reached & init_reg)
      then prints "Target not reached (safety hold!)";
           print reached;
      else prints "Target reached (safety does not hold!)";
    
    endif;
    

    DMC Code
    :-dynamic r/4.
    :-dynamic info/4.
    
    info(1,[p],6,[req,use,high,low,idle,busy]).
    
    r(init,p(s_s,R,U,H,L,I,B),{R>=0,U=0,H=0,L=0,I=1,B=0},1).
    
    r(p(s_s,R,U,H,L,I,B),p(s_s,R1,U1,H,L,I,B), 
        {R>=1,U>=0,H>=0,L>=0,I>=1,B>=0,  R1=R-1,U1=U+1},2). 
    
    r(p(s_s,R,U,H,L,I,B),p(s_s,R1,U1,H,L,I,B), 
        {R>=1,U>=1,H>=0,L>=0,I>=0,B>=0,  R1=R+1,U1=U-1},3). 
    
    r(p(s_s,R,U,H,L,I,B),p(s_s,R,U1,H1,L1,I1,B1), 
        {R>=0,U>=0,H>=0,L>=0,I>=1,B>=0, 
          I1=I-1,
          B1=B+1,
          H1>=H,
          L1>=L,
          H1+L1=H+L+U,
          U1=0},4). 
    
    r(p(s_s,R,U,H,L,I,B),p(s_s,R1,U1,H1,L1,I1,B1), 
        {R>=0,U>=0,H>=0,L>=0,I>=0,B>=1,
         B1=B-1,
         I1=I+1,
         H1=0,
         L1=0,
         U1=U+H,
         R1=R+L 
        },5). 
    
    prop(unsafe,p:s * (busy >=1) * (use >=1) * 
                      (req >=0)  * (low >=0) * 
                      (high >=0) * (idle >=0)).