Skip to content

Commit ed49ef8

Browse files
committed
tool: use kernel config instead of feature flag
Signed-off-by: James Archer <j.archer@unsw.edu.au>
1 parent fdad16f commit ed49ef8

6 files changed

Lines changed: 19 additions & 13 deletions

File tree

build_sdk.py

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -239,11 +239,10 @@ def test_tool() -> None:
239239
assert r == 0
240240

241241

242-
def build_tool(tool_target: Path, target_triple: str, experimental_domain_support: bool = False) -> None:
243-
build_cmd = f"cd tool/microkit && cargo build --release --target {target_triple}"
244-
if experimental_domain_support:
245-
build_cmd = f"{build_cmd} --features experimental-domain-support"
246-
r = system(build_cmd)
242+
def build_tool(tool_target: Path, target_triple: str) -> None:
243+
r = system(
244+
f"cd tool/microkit && cargo build --release --target {target_triple}"
245+
)
247246
assert r == 0
248247

249248
tool_output = f"./tool/microkit/target/{target_triple}/release/microkit"
@@ -502,7 +501,7 @@ def main() -> None:
502501
if not args.skip_tool:
503502
tool_target = root_dir / "bin" / "microkit"
504503
test_tool()
505-
build_tool(tool_target, args.tool_target_triple, args.experimental_domain_support)
504+
build_tool(tool_target, args.tool_target_triple)
506505

507506
if not args.skip_docs:
508507
build_doc(root_dir)

tool/microkit/Cargo.toml

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,6 @@ edition = "2021"
1313
name = "microkit"
1414
path = "src/main.rs"
1515

16-
[features]
17-
experimental-domain-support = []
18-
1916
[dependencies]
2017
roxmltree = "0.19.0"
2118
serde = "1.0.203"

tool/microkit/src/main.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2906,6 +2906,7 @@ fn main() -> Result<(), String> {
29062906
fan_out_limit: json_str_as_u64(&kernel_config_json, "RETYPE_FAN_OUT_LIMIT")?,
29072907
arm_pa_size_bits: 40,
29082908
hypervisor: json_str_as_bool(&kernel_config_json, "ARM_HYPERVISOR_SUPPORT")?,
2909+
domain_scheduler: json_str_as_u64(&kernel_config_json, "NUM_DOMAINS")? != 1,
29092910
};
29102911

29112912
match kernel_config.arch {

tool/microkit/src/sel4.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ pub struct Config {
4848
pub fan_out_limit: u64,
4949
pub hypervisor: bool,
5050
pub arm_pa_size_bits: usize,
51+
pub domain_scheduler: bool,
5152
}
5253

5354
pub enum Arch {

tool/microkit/src/sysxml.rs

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ fn loc_string(xml_sdf: &XmlSystemDescription, pos: roxmltree::TextPos) -> String
7575
pub struct PlatformDescription {
7676
/// Note that we have the invariant that page sizes are be ordered by size
7777
page_sizes: [u64; 2],
78+
domain_scheduler: bool,
7879
}
7980

8081
impl PlatformDescription {
@@ -83,7 +84,10 @@ impl PlatformDescription {
8384
Arch::Aarch64 => [0x1000, 0x200_000],
8485
};
8586

86-
PlatformDescription { page_sizes }
87+
PlatformDescription {
88+
page_sizes,
89+
domain_scheduler: kernel_config.domain_scheduler,
90+
}
8791
}
8892
}
8993

@@ -291,6 +295,7 @@ impl ProtectionDomain {
291295
node: &roxmltree::Node,
292296
is_child: bool,
293297
domain_schedule: &Option<DomainSchedule>,
298+
plat_desc: &PlatformDescription,
294299
) -> Result<ProtectionDomain, String> {
295300
let mut attrs = vec![
296301
"name", "priority", "pp", "budget", "period", "passive", "domain",
@@ -375,7 +380,7 @@ impl ProtectionDomain {
375380
return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name))
376381
}
377382
(_, Ok(domain)) => {
378-
if cfg!(feature = "experimental-domain-support") {
383+
if plat_desc.domain_scheduler {
379384
return Err(format!("Protection domain {} specifies a domain {} but system does not specify a domain schedule", name, domain));
380385
} else {
381386
return Err(format!("Assigning PDs to domains is only supported if SDK is built with --experimental-domain-support"));
@@ -498,6 +503,7 @@ impl ProtectionDomain {
498503
&child,
499504
true,
500505
&domain_schedule,
506+
&plat_desc,
501507
)?),
502508
"virtual_machine" => {
503509
if virtual_machine.is_some() {
@@ -1050,7 +1056,7 @@ pub fn parse(
10501056
// then parse the channels.
10511057
let mut channel_nodes = Vec::new();
10521058

1053-
if cfg!(feature = "experimental-domain-support") {
1059+
if plat_desc.domain_scheduler {
10541060
if let Some(domain_schedule_node) = system
10551061
.children()
10561062
.filter(|&child| child.is_element())
@@ -1072,11 +1078,12 @@ pub fn parse(
10721078
&child,
10731079
false,
10741080
&domain_schedule,
1081+
&plat_desc,
10751082
)?),
10761083
"channel" => channel_nodes.push(child),
10771084
"memory_region" => mrs.push(SysMemoryRegion::from_xml(&xml_sdf, &child, plat_desc)?),
10781085
"domain_schedule" => {
1079-
if !cfg!(feature = "experimental-domain-support") {
1086+
if !plat_desc.domain_scheduler {
10801087
let pos = xml_sdf.doc.text_pos_at(child.range().start);
10811088
return Err(format!("Domain schedule is only supported if SDK is built with --experimental-domain-support: {}", loc_string(&xml_sdf, pos)));
10821089
}

tool/microkit/tests/test.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ const DEFAULT_KERNEL_CONFIG: sel4::Config = sel4::Config {
1717
fan_out_limit: 256,
1818
hypervisor: true,
1919
arm_pa_size_bits: 40,
20+
domain_scheduler: false,
2021
};
2122

2223
const DEFAULT_PLAT_DESC: sysxml::PlatformDescription =

0 commit comments

Comments
 (0)