12,8 → 12,9 |
//===================================================================== |
|
#include "fsf_contract.h" |
#include "fsf_server.h" |
|
extern int fsf_cbsstar_level; |
extern int fsf_server_level; |
|
//#define FSF_DEBUG |
|
71,8 → 72,8 |
TIME T,Q; |
int budget, local_scheduler_level, scheduler_id; |
|
local_scheduler_level = CBSSTAR_get_local_scheduler_level_from_pid(fsf_cbsstar_level, exec_shadow); |
scheduler_id = CBSSTAR_get_local_scheduler_id_from_pid(fsf_cbsstar_level, exec_shadow); |
local_scheduler_level = SERVER_get_local_scheduler_level_from_pid(fsf_server_level, exec_shadow); |
scheduler_id = SERVER_get_local_scheduler_id_from_pid(fsf_server_level, exec_shadow); |
|
if (proc_table[exec_shadow].task_level != local_scheduler_level) return 0; |
|
93,7 → 94,7 |
|
if (next_budget != NULL && next_period != NULL) { |
|
CBSSTAR_getbudgetinfo(fsf_cbsstar_level, &Q, &T, budget); |
SERVER_getbudgetinfo(fsf_server_level, &Q, &T, budget); |
|
#ifdef FSF_DEBUG |
kern_printf("(budget %d Q=%d T=%d)",budget,(int)Q,(int)T); |
139,8 → 140,8 |
TIME T,Q; |
int budget, local_scheduler_level, scheduler_id; |
|
local_scheduler_level = CBSSTAR_get_local_scheduler_level_from_pid(fsf_cbsstar_level, exec_shadow); |
scheduler_id = CBSSTAR_get_local_scheduler_id_from_pid(fsf_cbsstar_level, exec_shadow); |
local_scheduler_level = SERVER_get_local_scheduler_level_from_pid(fsf_server_level, exec_shadow); |
scheduler_id = SERVER_get_local_scheduler_id_from_pid(fsf_server_level, exec_shadow); |
|
if (proc_table[exec_shadow].task_level != local_scheduler_level) return 0; |
|
161,7 → 162,7 |
|
if (next_budget != NULL && next_period != NULL) { |
|
CBSSTAR_getbudgetinfo(fsf_cbsstar_level, &Q, &T, budget); |
SERVER_getbudgetinfo(fsf_server_level, &Q, &T, budget); |
|
#ifdef FSF_DEBUG |
kern_printf("(budget %d Q=%d T=%d)",budget,(int)Q,(int)T); |