seL4-test/domain_schedule.c

77 lines
2.0 KiB
C

/*
* Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/* This is a domain schedule that is suitable for the domains tests in sel4test. All
* sel4test actually needs is for every domain to be executable for some period of time
* in order for the tests to make progress.
*
* Most tests run only in domain 0, so we give it the longest period to reduce
* overall idle time. We pick 2 ticks as the shortest period so that tests can
* make some progress if they exist, and we pick some variety in the first four
* domains so that not everything is equal.
*/
/* remember that this is compiled as part of the kernel, and so is referencing kernel headers */
#include <config.h>
#include <object/structures.h>
#include <model/statedata.h>
/* Default schedule. */
const dschedule_t ksDomSchedule[] = {
{ .domain = 0, .length = 60 },
#if CONFIG_NUM_DOMAINS > 1
{ .domain = 1, .length = 4 },
#endif
#if CONFIG_NUM_DOMAINS > 2
{ .domain = 2, .length = 3 },
#endif
#if CONFIG_NUM_DOMAINS > 3
{ .domain = 3, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 4
{ .domain = 4, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 5
{ .domain = 5, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 6
{ .domain = 6, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 7
{ .domain = 7, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 8
{ .domain = 8, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 9
{ .domain = 9, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 10
{ .domain = 10, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 11
{ .domain = 11, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 12
{ .domain = 12, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 13
{ .domain = 13, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 14
{ .domain = 14, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 15
{ .domain = 15, .length = 2 },
#endif
#if CONFIG_NUM_DOMAINS > 16
#error Unsupportd number of domains set
#endif
};
const word_t ksDomScheduleLength = sizeof(ksDomSchedule) / sizeof(dschedule_t);