sparrow-kata-full/kernel/round_robin_domain.c
June Tate-Gans c8e27dab0a domains: Remove TPA sandbox domain for now
At the moment, the scheduler is wasting 50% of its time in an idle thread for
the application sandbox domain. Until we can figure out how to use these domains
more effectively, we'll reduce to a single domain.

Bug: 238811077
Change-Id: If40d01d5c94e31cc8d522dd5f906f857e363cc42
GitOrigin-RevId: 911f6fe046c61b8ce7e9ba00f8de0ec872997ec3
2022-10-06 18:57:17 +00:00

32 lines
1.4 KiB
C

#include <model/statedata.h>
#include <object/structures.h>
/* Dual-domain schedule for Kata to isolate third party applications from system
* applications.
*
* Note that this doesn't actually implement the schedule -- that's hardwired in
* seL4's kernel source. See also kata/kernel/src/kernel/thread.c, in the
* nextDomain function around line 302 and the timerTick function around 630.
*
* Effectively this is a round-robin scheduler, so half of the CPU time is given
* to system applications, while third party applications are allocated the
* other half. Note that even if there's nothing to run in the third-party
* application domain, the scheduler will schedule an idle thread to ensure that
* domain gets it's allocated share of time.
*
* TODO(jtgans,sleffler): Figure out how to better use these domains for
* scheduling applications. We don't really want to use a full 50% duty cycle
* for third party applications -- this wastes too much time. See also
* b/238811077.
*
* NOTE: Only a single domain is currently enabled, as per the commented section
* below. Any time the below schedule is changed, the number of domains
* configured in easy-settings.cmake must also be changed.
*/
const dschedule_t ksDomSchedule[] = {
{.domain = 0, .length = 1}, // System domain
/* {.domain = 1, .length = 1}, // Third party application domain */
};
const word_t ksDomScheduleLength = sizeof(ksDomSchedule) / sizeof(dschedule_t);