816,7 → 816,19 |
void GRUBSTAR_disable_server(LEVEL l, int budget) |
{ |
GRUBSTAR_level_des *lev = (GRUBSTAR_level_des *)(level_table[l]); |
int avail_budget; |
int spare; |
|
/* force a hard reservation event */ |
avail_budget=lev->b[lev->tb[exec_shadow]].avail; |
lev->b[lev->tb[exec_shadow]].avail=0; |
|
level_table[proc_table[exec_shadow].task_level]->public_epilogue(proc_table[exec_shadow].task_level, exec_shadow); |
|
/* save the unused capacity */ |
spare=avail_budget+lev->b[lev->tb[exec_shadow]].avail; |
if (spare<=0) spare=0; |
|
/* Force the server in the NOACTIVE state */ |
lev->b[lev->tb[exec_shadow]].flags=GRUBSTAR_NOACTIVE; |
|