Load Balancing Monitor

HyTech Code for the associated EFSM (see full paper)

DMC Code for the associated EFSM
LBM

Load Balancing Monitor

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)).