Techniques and analysis for mixed-criticality scheduling with mode-dependent server execution budgets