Skip to content

Commit 4d4a2d0

Browse files
committed
tool: add support for kernel domain scheduler
Signed-off-by: James Archer <j.archer@unsw.edu.au>
1 parent e3bb1a7 commit 4d4a2d0

File tree

4 files changed

+202
-7
lines changed

4 files changed

+202
-7
lines changed

tool/microkit/src/main.rs

Lines changed: 35 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,7 @@ const INIT_VSPACE_CAP_ADDRESS: u64 = 3;
7272
const IRQ_CONTROL_CAP_ADDRESS: u64 = 4; // Singleton
7373
const INIT_ASID_POOL_CAP_ADDRESS: u64 = 6;
7474
const SMC_CAP_ADDRESS: u64 = 15;
75+
const DOMAIN_CAP_ADDRESS: u64 = 11;
7576

7677
// const ASID_CONTROL_CAP_ADDRESS: u64 = 5; // Singleton
7778
// const IO_PORT_CONTROL_CAP_ADDRESS: u64 = 7; // Null on this platform
@@ -895,6 +896,7 @@ fn build_system(
895896
cap_address_names.insert(INIT_ASID_POOL_CAP_ADDRESS, "ASID Pool: init".to_string());
896897
cap_address_names.insert(IRQ_CONTROL_CAP_ADDRESS, "IRQ Control".to_string());
897898
cap_address_names.insert(SMC_CAP_IDX, "SMC".to_string());
899+
cap_address_names.insert(DOMAIN_CAP_ADDRESS, "Domain Cap".to_string());
898900

899901
let system_cnode_bits = system_cnode_size.ilog2() as u64;
900902

@@ -2699,6 +2701,19 @@ fn build_system(
26992701
system_invocations.push(tcb_cap_copy_invocation);
27002702
}
27012703

2704+
for (pd_idx, pd) in system.protection_domains.iter().enumerate() {
2705+
if let Some(domain_id) = pd.domain_id {
2706+
system_invocations.push(Invocation::new(
2707+
config,
2708+
InvocationArgs::DomainSetSet {
2709+
domain_set: DOMAIN_CAP_ADDRESS,
2710+
domain: domain_id as u8,
2711+
tcb: pd_tcb_objs[pd_idx].cap_addr,
2712+
},
2713+
));
2714+
}
2715+
}
2716+
27022717
// Set VSpace and CSpace
27032718
let mut pd_set_space_invocation = Invocation::new(
27042719
config,
@@ -3345,6 +3360,7 @@ fn main() -> Result<(), String> {
33453360
arm_pa_size_bits,
33463361
arm_smc,
33473362
riscv_pt_levels: Some(RiscvVirtualMemory::Sv39),
3363+
domain_scheduler: json_str_as_u64(&kernel_config_json, "NUM_DOMAINS")? != 1,
33483364
};
33493365

33503366
if let Arch::Aarch64 = kernel_config.arch {
@@ -3378,9 +3394,27 @@ fn main() -> Result<(), String> {
33783394
system_invocation_count_symbol_name: "system_invocation_count",
33793395
};
33803396

3381-
let kernel_elf = ElfFile::from_path(&kernel_elf_path)?;
3397+
let mut kernel_elf = ElfFile::from_path(&kernel_elf_path)?;
33823398
let mut monitor_elf = ElfFile::from_path(&monitor_elf_path)?;
33833399

3400+
if let Some(domain_schedule) = &system.domain_schedule {
3401+
let schedule = &domain_schedule.schedule;
3402+
kernel_elf.write_symbol(
3403+
"ksDomScheduleLength",
3404+
&(schedule.len() as u64).to_le_bytes(),
3405+
)?;
3406+
3407+
let mut out = Vec::new();
3408+
out.reserve_exact(schedule.len() * 16);
3409+
3410+
for timeslice in schedule.iter() {
3411+
out.extend(timeslice.id.to_le_bytes());
3412+
out.extend(timeslice.length.to_le_bytes());
3413+
}
3414+
3415+
kernel_elf.write_symbol("ksDomSchedule", &out)?;
3416+
}
3417+
33843418
if monitor_elf.segments.iter().filter(|s| s.loadable).count() > 1 {
33853419
eprintln!(
33863420
"Monitor ({}) has {} segments, it must only have one",

tool/microkit/src/sdf.rs

Lines changed: 143 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
use crate::sel4::{Config, IrqTrigger, PageSize};
88
use crate::util::str_to_bool;
99
use crate::MAX_PDS;
10+
use std::collections::HashMap;
1011
use std::path::{Path, PathBuf};
1112

1213
///
@@ -45,6 +46,9 @@ const PD_DEFAULT_STACK_SIZE: u64 = 0x1000;
4546
const PD_MIN_STACK_SIZE: u64 = 0x1000;
4647
const PD_MAX_STACK_SIZE: u64 = 1024 * 1024 * 16;
4748

49+
/// The maximum length of domain schedule supported by the kernel
50+
const DOMAIN_SCHEDULE_MAX_LENGTH: usize = 256;
51+
4852
/// The purpose of this function is to parse an integer that could
4953
/// either be in decimal or hex format, unlike the normal parsing
5054
/// functionality that the Rust standard library provides.
@@ -159,6 +163,8 @@ pub struct ProtectionDomain {
159163
pub parent: Option<usize>,
160164
/// Location in the parsed SDF file
161165
text_pos: roxmltree::TextPos,
166+
/// Index into the domain schedule vector if the system is using domain scheduling
167+
pub domain_id: Option<u64>,
162168
}
163169

164170
#[derive(Debug, PartialEq, Eq, Hash)]
@@ -176,6 +182,18 @@ pub struct VirtualCpu {
176182
pub id: u64,
177183
}
178184

185+
#[derive(Debug, PartialEq, Eq, Hash)]
186+
pub struct DomainTimeslice {
187+
pub id: u64,
188+
pub length: u64,
189+
}
190+
191+
#[derive(Debug, PartialEq, Eq)]
192+
pub struct DomainSchedule {
193+
pub domain_ids: HashMap<String, u64>,
194+
pub schedule: Vec<DomainTimeslice>,
195+
}
196+
179197
impl SysMapPerms {
180198
fn from_str(s: &str) -> Result<u8, ()> {
181199
let mut perms = 0;
@@ -277,6 +295,7 @@ impl ProtectionDomain {
277295
xml_sdf: &XmlSystemDescription,
278296
node: &roxmltree::Node,
279297
is_child: bool,
298+
domain_schedule: &Option<DomainSchedule>,
280299
) -> Result<ProtectionDomain, String> {
281300
let mut attrs = vec![
282301
"name",
@@ -289,6 +308,7 @@ impl ProtectionDomain {
289308
// The SMC field is only available in certain configurations
290309
// but we do the error-checking further down.
291310
"smc",
311+
"domain",
292312
];
293313
if is_child {
294314
attrs.push("id");
@@ -418,6 +438,27 @@ impl ProtectionDomain {
418438
));
419439
}
420440

441+
let mut domain_id = None;
442+
match (domain_schedule, checked_lookup(xml_sdf, node, "domain")) {
443+
(Some(domain_schedule), Ok(domain_name)) => {
444+
domain_id = domain_schedule.domain_ids.get(domain_name);
445+
if domain_id.is_none() {
446+
return Err(format!("Protection domain {} specifies a domain {} that is not in the domain schedule", name, domain_name));
447+
}
448+
}
449+
(Some(_), _) => {
450+
return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name))
451+
}
452+
(_, Ok(domain)) => {
453+
if config.domain_scheduler {
454+
return Err(format!("Protection domain {} specifies a domain {} but system does not specify a domain schedule", name, domain));
455+
} else {
456+
return Err("Assigning PDs to domains is only supported if SDK is built with --experimental-domain-support".to_string());
457+
}
458+
}
459+
(_, _) => {}
460+
}
461+
421462
let mut maps = Vec::new();
422463
let mut irqs = Vec::new();
423464
let mut setvars: Vec<SysSetVar> = Vec::new();
@@ -549,9 +590,13 @@ impl ProtectionDomain {
549590
vaddr: None,
550591
})
551592
}
552-
"protection_domain" => {
553-
child_pds.push(ProtectionDomain::from_xml(config, xml_sdf, &child, true)?)
554-
}
593+
"protection_domain" => child_pds.push(ProtectionDomain::from_xml(
594+
config,
595+
xml_sdf,
596+
&child,
597+
true,
598+
domain_schedule,
599+
)?),
555600
"virtual_machine" => {
556601
if virtual_machine.is_some() {
557602
return Err(value_error(
@@ -604,6 +649,7 @@ impl ProtectionDomain {
604649
has_children,
605650
parent: None,
606651
text_pos: xml_sdf.doc.text_pos_at(node.range().start),
652+
domain_id: domain_id.copied(),
607653
})
608654
}
609655
}
@@ -860,13 +906,82 @@ impl Channel {
860906
}
861907
}
862908

909+
impl DomainSchedule {
910+
fn from_xml(
911+
xml_sdf: &XmlSystemDescription,
912+
node: &roxmltree::Node,
913+
) -> Result<DomainSchedule, String> {
914+
let pos = xml_sdf.doc.text_pos_at(node.range().start);
915+
916+
check_attributes(xml_sdf, node, &[])?;
917+
918+
let mut next_domain_id = 0;
919+
let mut domain_ids = HashMap::new();
920+
let mut schedule = Vec::new();
921+
for child in node.children() {
922+
if !child.is_element() {
923+
continue;
924+
}
925+
926+
let child_name = child.tag_name().name();
927+
if child_name != "domain" {
928+
return Err(format!(
929+
"Error: invalid XML element '{}': {}",
930+
child_name,
931+
loc_string(xml_sdf, pos)
932+
));
933+
}
934+
935+
if schedule.len() == DOMAIN_SCHEDULE_MAX_LENGTH {
936+
return Err(format!(
937+
"Error: length of domain schedule exceeds maximum of {}: {}",
938+
DOMAIN_SCHEDULE_MAX_LENGTH,
939+
loc_string(xml_sdf, pos)
940+
));
941+
}
942+
943+
check_attributes(xml_sdf, &child, &["name", "length"])?;
944+
let name = checked_lookup(xml_sdf, &child, "name")?;
945+
let length = checked_lookup(xml_sdf, &child, "length")?.parse::<u64>();
946+
if length.is_err() {
947+
return Err(format!(
948+
"Error: invalid domain timeslice length '{}': {}",
949+
name,
950+
loc_string(xml_sdf, pos)
951+
));
952+
}
953+
954+
let id = match domain_ids.get(name) {
955+
Some(&id) => id,
956+
None => {
957+
let id = next_domain_id;
958+
next_domain_id += 1;
959+
domain_ids.insert(name.to_string(), id);
960+
id
961+
}
962+
};
963+
964+
schedule.push(DomainTimeslice {
965+
id,
966+
length: length.unwrap(),
967+
});
968+
}
969+
970+
Ok(DomainSchedule {
971+
domain_ids,
972+
schedule,
973+
})
974+
}
975+
}
976+
863977
struct XmlSystemDescription<'a> {
864978
filename: &'a str,
865979
doc: &'a roxmltree::Document<'a>,
866980
}
867981

868982
#[derive(Debug)]
869983
pub struct SystemDescription {
984+
pub domain_schedule: Option<DomainSchedule>,
870985
pub protection_domains: Vec<ProtectionDomain>,
871986
pub memory_regions: Vec<SysMemoryRegion>,
872987
pub channels: Vec<Channel>,
@@ -1041,6 +1156,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result<SystemDescrip
10411156
doc: &doc,
10421157
};
10431158

1159+
let mut domain_schedule = None;
10441160
let mut root_pds = vec![];
10451161
let mut mrs = vec![];
10461162
let mut channels = vec![];
@@ -1059,18 +1175,38 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result<SystemDescrip
10591175
// then parse the channels.
10601176
let mut channel_nodes = Vec::new();
10611177

1178+
if config.domain_scheduler {
1179+
if let Some(domain_schedule_node) = system
1180+
.children()
1181+
.filter(|&child| child.is_element())
1182+
.find(|&child| child.tag_name().name() == "domain_schedule")
1183+
{
1184+
domain_schedule = Some(DomainSchedule::from_xml(&xml_sdf, &domain_schedule_node)?);
1185+
}
1186+
}
1187+
10621188
for child in system.children() {
10631189
if !child.is_element() {
10641190
continue;
10651191
}
10661192

10671193
let child_name = child.tag_name().name();
10681194
match child_name {
1069-
"protection_domain" => {
1070-
root_pds.push(ProtectionDomain::from_xml(config, &xml_sdf, &child, false)?)
1071-
}
1195+
"protection_domain" => root_pds.push(ProtectionDomain::from_xml(
1196+
config,
1197+
&xml_sdf,
1198+
&child,
1199+
false,
1200+
&domain_schedule,
1201+
)?),
10721202
"channel" => channel_nodes.push(child),
10731203
"memory_region" => mrs.push(SysMemoryRegion::from_xml(config, &xml_sdf, &child)?),
1204+
"domain_schedule" => {
1205+
if !config.domain_scheduler {
1206+
let pos = xml_sdf.doc.text_pos_at(child.range().start);
1207+
return Err(format!("Domain schedule is only supported if SDK is built with --experimental-domain-support: {}", loc_string(&xml_sdf, pos)));
1208+
}
1209+
}
10741210
_ => {
10751211
let pos = xml_sdf.doc.text_pos_at(child.range().start);
10761212
return Err(format!(
@@ -1286,6 +1422,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result<SystemDescrip
12861422
}
12871423

12881424
Ok(SystemDescription {
1425+
domain_schedule,
12891426
protection_domains: pds,
12901427
memory_regions: mrs,
12911428
channels,

tool/microkit/src/sel4.rs

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ pub struct Config {
5656
pub arm_smc: Option<bool>,
5757
/// RISC-V specific, what kind of virtual memory system (e.g Sv39)
5858
pub riscv_pt_levels: Option<RiscvVirtualMemory>,
59+
pub domain_scheduler: bool,
5960
}
6061

6162
impl Config {
@@ -1094,6 +1095,15 @@ impl Invocation {
10941095
arg_strs.push(Invocation::fmt_field_cap("tcb", tcb, cap_lookup));
10951096
(vcpu, cap_lookup.get(&vcpu).unwrap())
10961097
}
1098+
InvocationArgs::DomainSetSet {
1099+
domain_set,
1100+
domain,
1101+
tcb,
1102+
} => {
1103+
arg_strs.push(Invocation::fmt_field("domain", domain as u64));
1104+
arg_strs.push(Invocation::fmt_field_cap("tcb", tcb, cap_lookup));
1105+
(domain_set, cap_lookup.get(&domain_set).unwrap().as_str())
1106+
}
10971107
};
10981108
_ = writeln!(
10991109
f,
@@ -1129,6 +1139,7 @@ impl Invocation {
11291139
InvocationLabel::CnodeCopy | InvocationLabel::CnodeMint => "CNode",
11301140
InvocationLabel::SchedControlConfigureFlags => "SchedControl",
11311141
InvocationLabel::ArmVcpuSetTcb => "VCPU",
1142+
InvocationLabel::DomainSetSet => "DomainSet",
11321143
_ => panic!(
11331144
"Internal error: unexpected label when getting object type '{:?}'",
11341145
self.label
@@ -1157,6 +1168,7 @@ impl Invocation {
11571168
InvocationLabel::CnodeMint => "Mint",
11581169
InvocationLabel::SchedControlConfigureFlags => "ConfigureFlags",
11591170
InvocationLabel::ArmVcpuSetTcb => "VCPUSetTcb",
1171+
InvocationLabel::DomainSetSet => "Set",
11601172
_ => panic!(
11611173
"Internal error: unexpected label when getting method name '{:?}'",
11621174
self.label
@@ -1198,6 +1210,7 @@ impl InvocationArgs {
11981210
InvocationLabel::SchedControlConfigureFlags
11991211
}
12001212
InvocationArgs::ArmVcpuSetTcb { .. } => InvocationLabel::ArmVcpuSetTcb,
1213+
InvocationArgs::DomainSetSet { .. } => InvocationLabel::DomainSetSet,
12011214
}
12021215
}
12031216

@@ -1349,6 +1362,11 @@ impl InvocationArgs {
13491362
vec![sched_context],
13501363
),
13511364
InvocationArgs::ArmVcpuSetTcb { vcpu, tcb } => (vcpu, vec![], vec![tcb]),
1365+
InvocationArgs::DomainSetSet {
1366+
domain_set,
1367+
domain,
1368+
tcb,
1369+
} => (domain_set, vec![domain as u64], vec![tcb]),
13521370
}
13531371
}
13541372
}
@@ -1462,4 +1480,9 @@ pub enum InvocationArgs {
14621480
vcpu: u64,
14631481
tcb: u64,
14641482
},
1483+
DomainSetSet {
1484+
domain_set: u64,
1485+
domain: u8,
1486+
tcb: u64,
1487+
},
14651488
}

0 commit comments

Comments
 (0)