Skip to content

Commit 8b3b6e6

Browse files
committed
domains: remove seperate configs
Signed-off-by: Krishnan Winter <krishnan.winter@unsw.edu.au>
1 parent ba3f824 commit 8b3b6e6

2 files changed

Lines changed: 6 additions & 5 deletions

File tree

build_sdk.py

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -478,8 +478,10 @@ class KernelPath:
478478

479479

480480
def elaborate_all_board_configs(board: BoardInfo) -> list[ConfigInfo]:
481-
elaborated_configs = list(SUPPORTED_CONFIGS)
481+
elaborated_configs = list()
482482

483+
# We cannot build configs supporting SMP and domains. We will first elaborate
484+
# the configs for smp, then for domains
483485
if board.smp_cores is not None:
484486
for config in SUPPORTED_CONFIGS:
485487
config = copy.deepcopy(config)
@@ -491,7 +493,6 @@ def elaborate_all_board_configs(board: BoardInfo) -> list[ConfigInfo]:
491493

492494
for config in SUPPORTED_CONFIGS:
493495
config = copy.deepcopy(config)
494-
config.name = f"domain-{config.name}"
495496
config.kernel_options |= {
496497
"KernelTimerFrequency": True,
497498
"KernelNumDomains": 32,

docs/manual.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -355,7 +355,7 @@ I/O ports are x86 mechanisms to access certain physical devices (e.g. PC serial
355355

356356
# Domain Scheduling {#domain}
357357

358-
Microkit can be built with experimental support for a method of temporally isolating different groups of PDs called domain scheduling. On a Microkit system, only one domain is active at a time, and the kernel alternates between domains according to a round-robin schedule. A domain schedule consists of an ordered list of domains, each with an associated length of time to run. The kernel will then activate a domain for the specified length of time; after that time has passed, it will deactivate that domain and activate the next domain for its length of time, and so on, proceeding through the list until it wraps back to the first domain. PDs are assigned to domains, such that when a certain domain is active, only PDs belonging to that domain will be scheduled to run.
358+
Microkit also supports a method of temporally isolating different groups of PDs called domain scheduling. On a Microkit system, only one domain is active at a time, and the kernel alternates between domains according to a round-robin schedule. A domain schedule consists of an ordered list of domains, each with an associated length of time to run. The kernel will then activate a domain for the specified length of time; after that time has passed, it will deactivate that domain and activate the next domain for its length of time, and so on, proceeding through the list until it wraps back to the first domain. PDs are assigned to domains, such that when a certain domain is active, only PDs belonging to that domain will be scheduled to run.
359359

360360
# SDK {#sdk}
361361

@@ -1012,7 +1012,7 @@ It supports the following attributes:
10121012
Must be be between 4KiB and 16MiB and be 4K page-aligned. Defaults to 8KiB.
10131013
* `cpu`: (optional) set the physical CPU core this PD will run on. Defaults to zero.
10141014
* `smc`: (optional, only on ARM) Allow the PD to give an SMC call for the kernel to perform.. Defaults to false.
1015-
* `domain`: (optional, experimental) Specifies the name of the scheduling domain the PD belongs to.
1015+
* `domain`: (optional) Specifies the name of the scheduling domain the PD belongs to.
10161016

10171017
Additionally, it supports the following child elements:
10181018

@@ -1166,7 +1166,7 @@ The `domain_idx_shift` element has the following attribute:
11661166
The `domain_start` element has the following attribute:
11671167
* `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. This index is an offset into the user defined schedule, and not an absolute index. If no domain start index is set, then the Microkit tool will set this to 0 by default.
11681168

1169-
The `domain_schedule` element is only valid if the using one of the domain configs (`domain-release`, `domain-debug`, `domain-benchmark`).
1169+
The `domain_schedule` element is only valid of using non-smp configs.
11701170

11711171
# Board Support Packages {#bsps}
11721172

0 commit comments

Comments
 (0)