You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/manual.md
+3-3Lines changed: 3 additions & 3 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1143,9 +1143,9 @@ The `end` element has the following attributes:
1143
1143
The `id` is passed to the PD in the `notified` and `protected` entry points.
1144
1144
The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functions.
1145
1145
1146
-
## `domain_schedule` (experimental)
1146
+
## `domain_schedule`
1147
1147
1148
-
The `domain_schedule` element, by default, has a list of up to 256`domain` child elements. This can be configured by changing the number of schedule entries defined in the `release_domains` and `debug_domains` configs in `build_sdk.py`. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule.
1148
+
The `domain_schedule` element, by default, has a list of up to 128`domain` child elements (bounded by the kernel config). This can be configured by changing the number of schedule entries defined in `elaborate_all_board_configs` in `build_sdk.py`. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule.
1149
1149
1150
1150
The `domain` element has the following attributes:
1151
1151
@@ -1161,7 +1161,7 @@ The `domain_idx_shift` element has the following attribute:
1161
1161
The `domain_start` element has the following attribute:
1162
1162
*`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.
1163
1163
1164
-
The `domain_schedule` element is only valid if the using one of the domain configs (`release_domains`, `debug_domains`).
1164
+
The `domain_schedule` element is only valid if the using one of the domain configs (`domain-release`, `domain-debug`, `domain-benchmark`).
0 commit comments