From a6e34f9e8192a6958f2293d42e262b9a5a05412c Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Fri, 19 Jun 2026 10:10:14 +1000 Subject: [PATCH 1/5] tool/elf: decouple program headers from segments Previously, the ELF code treats program headers = segments. While this worked originally, it broke for cases that requires >= 2 program headers to refer to the same segment. Now, when the ELF is parsed, the code will create a 1-1 mapping of segments to program headers like before. But the allow for additional program headers to be inserted. Signed-off-by: Bill Nguyen --- tool/microkit/src/elf.rs | 57 ++++++++++++++++++++++++++++++---------- 1 file changed, 43 insertions(+), 14 deletions(-) diff --git a/tool/microkit/src/elf.rs b/tool/microkit/src/elf.rs index 4ef82d9e0..71996ab11 100644 --- a/tool/microkit/src/elf.rs +++ b/tool/microkit/src/elf.rs @@ -197,6 +197,12 @@ impl ElfSegment { } } +#[derive(Eq, PartialEq, Clone)] +pub struct ProgramHeader { + pub segment_idx: usize, + pub type_: u32, +} + #[derive(Eq, PartialEq, Clone)] pub struct ElfFile { pub path: PathBuf, @@ -204,6 +210,7 @@ pub struct ElfFile { pub entry: u64, pub machine: u16, pub segments: Vec, + pub program_headers: Vec, symbols: HashMap, } @@ -215,6 +222,7 @@ impl ElfFile { entry, machine, segments: [].into(), + program_headers: [].into(), symbols: HashMap::new(), } } @@ -233,12 +241,24 @@ impl ElfFile { Some(path_for_symbols) => ElfFileReader::from_path(path_for_symbols)?.symbols()?, None => reader.symbols()?, }; + // Initially create a one to one mapping of segments -> program headers. + // So that we can create two program headers of different types that point to the same segment. + let program_headers = segments + .iter() + .enumerate() + .map(|(i, _)| ProgramHeader { + segment_idx: i, + type_: PHENT_TYPE_LOADABLE, + }) + .collect(); + Ok(ElfFile { path: path.to_owned(), word_size: reader.word_size, entry: reader.hdr.entry, machine: reader.hdr.machine, segments, + program_headers, symbols, }) } @@ -522,6 +542,11 @@ impl ElfFile { attrs: r | w | x, }; self.segments.push(elf_segment); + + self.program_headers.push(ProgramHeader { + segment_idx: self.segments.len() - 1, + type_: PHENT_TYPE_LOADABLE, + }); } pub fn loadable_segments(&self) -> Vec<&ElfSegment> { @@ -532,7 +557,7 @@ impl ElfFile { pub fn reserialise(&self, out: &std::path::Path) -> Result { let ehsize = size_of::(); - let phnum = self.loadable_segments().len(); + let phnum = self.program_headers.len(); let phentsize = size_of::(); // First entry is reserved, last entry is dummy strtab @@ -587,21 +612,27 @@ impl ElfFile { let mut data_off_watermark = (ehsize as u64) + (phnum as u64) * (phentsize as u64) + (shnum as u64) * (shentsize as u64); - let mut data_offs = [].to_vec(); - // First write out the program headers table + // First thing to do is work out where to place all the data segments + let mut seg_idx_to_data_off: HashMap = Default::default(); for (i, seg) in self.loadable_segments().iter().enumerate() { + seg_idx_to_data_off.insert(i, data_off_watermark); + data_off_watermark += seg.file_size(); + } + + // Then write out the program headers table + for (i, program_header) in self.program_headers.iter().enumerate() { + let linked_segment = &self.segments[program_header.segment_idx]; let ph_serialised = ElfProgramHeader64 { - type_: PHENT_TYPE_LOADABLE, // loadable - flags: seg.attrs, - offset: data_off_watermark, - vaddr: seg.virt_addr, - paddr: seg.phys_addr, - filesz: seg.file_size(), - memsz: seg.mem_size(), + type_: program_header.type_, + flags: linked_segment.attrs, + offset: seg_idx_to_data_off[&program_header.segment_idx], + vaddr: linked_segment.virt_addr, + paddr: linked_segment.phys_addr, + filesz: linked_segment.file_size(), + memsz: linked_segment.mem_size(), align: 0, }; - data_offs.push(data_off_watermark); elf_file .write_all(unsafe { struct_to_bytes(&ph_serialised) }) @@ -612,8 +643,6 @@ impl ElfFile { out.display() ) }); - - data_off_watermark += seg.file_size(); } // Then the section headers table, which describe the same thing as the program headers. @@ -634,7 +663,7 @@ impl ElfFile { type_: SHT_PROGBITS, flags: seg.section_flags(), addr: seg.phys_addr, - offset: data_offs[i], + offset: seg_idx_to_data_off[&i], size: seg.file_size(), link: 0, info: 0, From 0c8df6339aee7c6cdb3042da2d4cbc8b04c16033 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Fri, 19 Jun 2026 13:43:33 +1000 Subject: [PATCH 2/5] tool/elf: refactored program headers table mgmt Added `pub fn phdrs_table(&self) -> Vec<(ElfProgramHeader64, usize)>` to ELF code. Signed-off-by: Bill Nguyen --- tool/microkit/src/elf.rs | 47 ++++++++++++++++++++++++++-------------- 1 file changed, 31 insertions(+), 16 deletions(-) diff --git a/tool/microkit/src/elf.rs b/tool/microkit/src/elf.rs index 71996ab11..688815a15 100644 --- a/tool/microkit/src/elf.rs +++ b/tool/microkit/src/elf.rs @@ -62,7 +62,7 @@ struct ElfSectionHeader64 { } #[repr(C, packed)] -struct ElfProgramHeader64 { +pub struct ElfProgramHeader64 { type_: u32, flags: u32, offset: u64, @@ -553,6 +553,29 @@ impl ElfFile { self.segments.iter().filter(|s| s.loadable).collect() } + /// Returns a vec of program headers in ELF format without the file data offset filled and its linked segment. + pub fn phdrs_table_serialised(&self) -> Vec<(ElfProgramHeader64, usize)> { + let mut table = vec![]; + for program_header in self.program_headers.iter() { + let linked_segment = &self.segments[program_header.segment_idx]; + + let phdr = ElfProgramHeader64 { + type_: program_header.type_, + flags: linked_segment.attrs, + offset: 0, + vaddr: linked_segment.virt_addr, + paddr: linked_segment.phys_addr, + filesz: linked_segment.file_size(), + memsz: linked_segment.mem_size(), + align: 0, + }; + + table.push((phdr, program_header.segment_idx)); + } + + table + } + /// Re-create a minimal ELF file with all the program and section headers. pub fn reserialise(&self, out: &std::path::Path) -> Result { let ehsize = size_of::(); @@ -621,25 +644,17 @@ impl ElfFile { } // Then write out the program headers table - for (i, program_header) in self.program_headers.iter().enumerate() { - let linked_segment = &self.segments[program_header.segment_idx]; - let ph_serialised = ElfProgramHeader64 { - type_: program_header.type_, - flags: linked_segment.attrs, - offset: seg_idx_to_data_off[&program_header.segment_idx], - vaddr: linked_segment.virt_addr, - paddr: linked_segment.phys_addr, - filesz: linked_segment.file_size(), - memsz: linked_segment.mem_size(), - align: 0, - }; + for (phdr, seg_idx) in self.phdrs_table_serialised().iter_mut() { + phdr.offset = seg_idx_to_data_off[seg_idx]; + let phdr_type = phdr.type_; elf_file - .write_all(unsafe { struct_to_bytes(&ph_serialised) }) + .write_all(unsafe { struct_to_bytes(phdr) }) .unwrap_or_else(|_| { panic!( - "Failed to write ELF program header #{} for '{}'", - i, + "Failed to write ELF program header type {:x} linked to segment index {} for '{}'", + phdr_type, + seg_idx, out.display() ) }); From c7abd5a410122460c573ec001a9f4a1774669872 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Fri, 19 Jun 2026 13:46:57 +1000 Subject: [PATCH 3/5] tool/elf: + segment with multiple program headers Modified `pub fn add_segment()` to allow for an additional program header in the ELF to describe the segment with a user defined type identifier. Signed-off-by: Bill Nguyen --- tool/microkit/src/capdl/initialiser.rs | 2 ++ tool/microkit/src/elf.rs | 13 ++++++++++++- tool/microkit/src/loader.rs | 1 + 3 files changed, 15 insertions(+), 1 deletion(-) diff --git a/tool/microkit/src/capdl/initialiser.rs b/tool/microkit/src/capdl/initialiser.rs index 250203b55..78c3284a2 100644 --- a/tool/microkit/src/capdl/initialiser.rs +++ b/tool/microkit/src/capdl/initialiser.rs @@ -67,6 +67,7 @@ impl CapDLInitialiser { false, spec_vaddr, ElfSegmentData::RealData(spec_payload.into()), + None, ); let embedded_frame_data_vaddr = self.elf.next_vaddr(INITIALISER_GRANULE_SIZE); @@ -76,6 +77,7 @@ impl CapDLInitialiser { false, embedded_frame_data_vaddr, ElfSegmentData::RealData(embedded_frame_data), + None, ); // These symbol names must match rust-sel4/crates/sel4-capdl-initializer/src/main.rs diff --git a/tool/microkit/src/elf.rs b/tool/microkit/src/elf.rs index 688815a15..0606fd882 100644 --- a/tool/microkit/src/elf.rs +++ b/tool/microkit/src/elf.rs @@ -522,6 +522,9 @@ impl ElfFile { round_down(self.highest_vaddr() + page_size as u64, page_size as u64) } + /// Add a segment, its data and a corresponding program header with loadable type to the ELF. + /// The caller can pass a Some value to `meta_phdr_type_maybe` to create an additional + /// program header with a specific type identifier. pub fn add_segment( &mut self, read: bool, @@ -529,6 +532,7 @@ impl ElfFile { execute: bool, vaddr: u64, data: ElfSegmentData, + meta_phdr_type_maybe: Option, ) { let r = if read { PF_R } else { 0 }; let w = if write { PF_W } else { 0 }; @@ -547,6 +551,13 @@ impl ElfFile { segment_idx: self.segments.len() - 1, type_: PHENT_TYPE_LOADABLE, }); + + if let Some(meta_phdr_type) = meta_phdr_type_maybe { + self.program_headers.push(ProgramHeader { + segment_idx: self.segments.len() - 1, + type_: meta_phdr_type, + }); + } } pub fn loadable_segments(&self) -> Vec<&ElfSegment> { @@ -660,7 +671,7 @@ impl ElfFile { }); } - // Then the section headers table, which describe the same thing as the program headers. + // Next step is the section headers table, which describe mostly the same thing as the program headers. // This is needed for U-Boot's `bootelf` command to work properly without adding the `-p` flag // when booting the loader image on ARM and RISC-V platforms. // First entry is reserved! diff --git a/tool/microkit/src/loader.rs b/tool/microkit/src/loader.rs index 5e4ec89b9..53a2597e2 100644 --- a/tool/microkit/src/loader.rs +++ b/tool/microkit/src/loader.rs @@ -572,6 +572,7 @@ impl<'a> Loader<'a> { true, self.entry, ElfSegmentData::RealData(self.to_bytes()), + None, ); loader_elf From d9b1e0ac1369af70b4ceee159c34ac113cbf7833 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Mon, 22 Jun 2026 14:15:44 +1000 Subject: [PATCH 4/5] Switch rust-sel4 to mainline commit Which also required changes to how the spec is packed into the intialiser. Signed-off-by: Bill Nguyen --- Cargo.lock | 93 +++++++++++++++++--------- Cargo.toml | 8 +-- tool/microkit/src/capdl/initialiser.rs | 93 ++++++++++++++++++-------- tool/microkit/src/elf.rs | 21 +++--- 4 files changed, 143 insertions(+), 72 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 2a0442d20..310899960 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -494,7 +494,7 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "sel4" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "cfg-if", "sel4-config", @@ -504,7 +504,7 @@ dependencies = [ [[package]] name = "sel4-alloca" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "cfg-if", ] @@ -512,7 +512,7 @@ dependencies = [ [[package]] name = "sel4-bitfield-ops" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "rustversion", ] @@ -520,12 +520,12 @@ dependencies = [ [[package]] name = "sel4-build-env" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" [[package]] name = "sel4-capdl-initializer" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "log", "rkyv", @@ -534,13 +534,16 @@ dependencies = [ "sel4-immediate-sync-once-cell", "sel4-immutable-cell", "sel4-logging", + "sel4-no-allocator", + "sel4-phdrs", + "sel4-phdrs-patched", "sel4-root-task", ] [[package]] name = "sel4-capdl-initializer-types" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "miniz_oxide", "rkyv", @@ -552,7 +555,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types-derive" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "proc-macro2", "quote", @@ -562,7 +565,7 @@ dependencies = [ [[package]] name = "sel4-config" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "prettyplease", "proc-macro2", @@ -576,7 +579,7 @@ dependencies = [ [[package]] name = "sel4-config-data" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "sel4-build-env", "sel4-config-types", @@ -586,7 +589,7 @@ dependencies = [ [[package]] name = "sel4-config-macros" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "fallible-iterator", "proc-macro2", @@ -599,7 +602,7 @@ dependencies = [ [[package]] name = "sel4-config-types" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "serde", ] @@ -607,36 +610,31 @@ dependencies = [ [[package]] name = "sel4-ctors-dtors" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" [[package]] name = "sel4-dlmalloc" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "dlmalloc", "lock_api", ] -[[package]] -name = "sel4-elf-header" -version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" - [[package]] name = "sel4-immediate-sync-once-cell" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" [[package]] name = "sel4-immutable-cell" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" [[package]] name = "sel4-initialize-tls" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "cfg-if", "sel4-alloca", @@ -645,16 +643,21 @@ dependencies = [ [[package]] name = "sel4-logging" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "lock_api", "log", ] +[[package]] +name = "sel4-no-allocator" +version = "0.1.0" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" + [[package]] name = "sel4-panicking" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "cfg-if", "sel4-immediate-sync-once-cell", @@ -665,12 +668,39 @@ dependencies = [ [[package]] name = "sel4-panicking-env" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" + +[[package]] +name = "sel4-phdrs" +version = "0.1.0" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +dependencies = [ + "sel4-phdrs-constants", +] + +[[package]] +name = "sel4-phdrs-constants" +version = "0.1.0" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" + +[[package]] +name = "sel4-phdrs-patched" +version = "0.1.0" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +dependencies = [ + "sel4-phdrs", + "sel4-rodata-static", +] + +[[package]] +name = "sel4-rodata-static" +version = "0.1.0" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" [[package]] name = "sel4-root-task" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "sel4", "sel4-dlmalloc", @@ -685,7 +715,7 @@ dependencies = [ [[package]] name = "sel4-root-task-macros" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "proc-macro2", "quote", @@ -695,14 +725,15 @@ dependencies = [ [[package]] name = "sel4-runtime-common" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "cfg-if", "sel4", "sel4-ctors-dtors", - "sel4-elf-header", + "sel4-immutable-cell", "sel4-initialize-tls", "sel4-panicking-env", + "sel4-phdrs", "sel4-stack", "unwinding", ] @@ -710,12 +741,12 @@ dependencies = [ [[package]] name = "sel4-stack" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" [[package]] name = "sel4-sync" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "lock_api", "sel4", @@ -725,7 +756,7 @@ dependencies = [ [[package]] name = "sel4-sys" version = "0.1.0" -source = "git+https://github.com/au-ts/rust-sel4?rev=33cb132571121a8d846ad3be9066617087ee5c32#33cb132571121a8d846ad3be9066617087ee5c32" +source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" dependencies = [ "bindgen", "glob", diff --git a/Cargo.toml b/Cargo.toml index e3c561ebb..166c88961 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,12 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/au-ts/rust-sel4" -rev = "33cb132571121a8d846ad3be9066617087ee5c32" +git = "https://github.com/seL4/rust-sel4" +rev = "c30d0e44fb32c15239049ce402ef2a8c72499aa3" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/au-ts/rust-sel4" -rev = "33cb132571121a8d846ad3be9066617087ee5c32" +git = "https://github.com/seL4/rust-sel4" +rev = "c30d0e44fb32c15239049ce402ef2a8c72499aa3" [profile.release.package.microkit-tool] strip = true diff --git a/tool/microkit/src/capdl/initialiser.rs b/tool/microkit/src/capdl/initialiser.rs index 78c3284a2..45cca4930 100644 --- a/tool/microkit/src/capdl/initialiser.rs +++ b/tool/microkit/src/capdl/initialiser.rs @@ -8,14 +8,19 @@ use std::ops::Range; use rkyv::util::AlignedVec; -use crate::elf::ElfSegmentData; -use crate::util::round_up; +use crate::elf::{ElfProgramHeader64, ElfSegmentData, PF_R, PHENT_TYPE_LOADABLE, PHENT_TYPE_PHDR}; +use crate::util::{round_up, struct_to_bytes}; use crate::{elf::ElfFile, sel4::PageSize}; use crate::{serialise_ut, UntypedObject}; // Page size used for allocating the spec and embedded frames segments. pub const INITIALISER_GRANULE_SIZE: PageSize = PageSize::Small; +// Magic numbers for the initialiser to identify the data type. +// See rust-sel4 crates/sel4-phdrs/constants/src/lib.rs +const PT_SEL4_CAPDL_SPEC: u32 = 0x64c3_4003; +const PT_SEL4_CAPDL_FRAME_DATA: u32 = 0x64c3_4004; + pub struct CapDLInitialiserSpecMetadata { pub spec_size: u64, } @@ -59,6 +64,7 @@ impl CapDLInitialiser { self.spec_metadata = None; } + // Follow implementation in rust-sel4: crates/sel4-capdl-initializer/add-spec/src/lib.rs let spec_vaddr = self.elf.next_vaddr(INITIALISER_GRANULE_SIZE); let spec_size = spec_payload.len() as u64; self.elf.add_segment( @@ -67,7 +73,7 @@ impl CapDLInitialiser { false, spec_vaddr, ElfSegmentData::RealData(spec_payload.into()), - None, + Some(PT_SEL4_CAPDL_SPEC), ); let embedded_frame_data_vaddr = self.elf.next_vaddr(INITIALISER_GRANULE_SIZE); @@ -77,40 +83,73 @@ impl CapDLInitialiser { false, embedded_frame_data_vaddr, ElfSegmentData::RealData(embedded_frame_data), - None, + Some(PT_SEL4_CAPDL_FRAME_DATA), ); - // These symbol names must match rust-sel4/crates/sel4-capdl-initializer/src/main.rs - self.elf - .write_symbol( - "sel4_capdl_initializer_embedded_frames_data_start", - &embedded_frame_data_vaddr.to_le_bytes(), - ) - .unwrap(); + // Now make the program headers table and inject it into the ELF as the initialiser look at + // it to figure out its virtual address bound, spec location in memory etc. + // It would have been nicer if we can perform this step in ElfFile::reserialise() but + // that function is only relevant for x86. + let phdrs_table_vaddr = self.elf.next_vaddr(INITIALISER_GRANULE_SIZE); + let phdrs_table = self.elf.phdrs_table_serialised(); + // Accounts for a PHENT_TYPE_PHDR meta phdr + PHENT_TYPE_LOADABLE phdr when we eventually inject + // the table as a segment. + let expected_phnum = phdrs_table.len() + 2; + let expected_phdrs_table_size_bytes = size_of::() * expected_phnum; + + let mut phdrs_table_bytes = vec![]; + phdrs_table.iter().for_each(|phdr| { + phdrs_table_bytes.extend(unsafe { struct_to_bytes(&phdr.0) }); + }); + + // Simulate what happens in ElfFile::add_segment() to derive the final program headers table. + // We do this due to a chicken and egg problem, the real program headers table won't be finalised + // until we add it as a segment. But we can't add it as a segment until we finalise it. + phdrs_table_bytes.extend(unsafe { + struct_to_bytes(&ElfProgramHeader64 { + type_: PHENT_TYPE_PHDR, + flags: PF_R, + offset: 0, + vaddr: phdrs_table_vaddr, + paddr: phdrs_table_vaddr, + filesz: expected_phdrs_table_size_bytes as u64, + memsz: expected_phdrs_table_size_bytes as u64, + align: 0, + }) + }); + phdrs_table_bytes.extend(unsafe { + struct_to_bytes(&ElfProgramHeader64 { + type_: PHENT_TYPE_LOADABLE, + flags: PF_R, + offset: 0, + vaddr: phdrs_table_vaddr, + paddr: phdrs_table_vaddr, + filesz: expected_phdrs_table_size_bytes as u64, + memsz: expected_phdrs_table_size_bytes as u64, + align: 0, + }) + }); - self.elf - .write_symbol( - "sel4_capdl_initializer_serialized_spec_data_start", - &spec_vaddr.to_le_bytes(), - ) - .unwrap(); - self.elf - .write_symbol( - "sel4_capdl_initializer_serialized_spec_data_size", - &spec_size.to_le_bytes(), - ) - .unwrap(); + self.elf.add_segment( + true, + false, + false, + phdrs_table_vaddr, + ElfSegmentData::RealData(phdrs_table_bytes), + Some(PHENT_TYPE_PHDR), + ); self.elf .write_symbol( - "sel4_capdl_initializer_image_start", - &self.elf.lowest_vaddr().to_le_bytes(), + "sel4_phdrs_patched__vaddr", + &phdrs_table_vaddr.to_le_bytes(), ) .unwrap(); + self.elf .write_symbol( - "sel4_capdl_initializer_image_end", - &self.elf.highest_vaddr().to_le_bytes(), + "sel4_phdrs_patched__phnum", + &(expected_phnum as u16).to_le_bytes(), ) .unwrap(); diff --git a/tool/microkit/src/elf.rs b/tool/microkit/src/elf.rs index 0606fd882..7fb1a4305 100644 --- a/tool/microkit/src/elf.rs +++ b/tool/microkit/src/elf.rs @@ -63,14 +63,14 @@ struct ElfSectionHeader64 { #[repr(C, packed)] pub struct ElfProgramHeader64 { - type_: u32, - flags: u32, - offset: u64, - vaddr: u64, - paddr: u64, - filesz: u64, - memsz: u64, - align: u64, + pub type_: u32, + pub flags: u32, + pub offset: u64, + pub vaddr: u64, + pub paddr: u64, + pub filesz: u64, + pub memsz: u64, + pub align: u64, } #[repr(C, packed)] @@ -100,12 +100,13 @@ struct ElfHeader64 { const ELF_MAGIC: &[u8; 4] = b"\x7FELF"; -const PHENT_TYPE_LOADABLE: u32 = 1; +pub const PHENT_TYPE_LOADABLE: u32 = 1; +pub const PHENT_TYPE_PHDR: u32 = 6; /// ELF program-header flags (`p_flags`) const PF_X: u32 = 0x1; const PF_W: u32 = 0x2; -const PF_R: u32 = 0x4; +pub const PF_R: u32 = 0x4; /// ELF section-header type (`sh_type`) const SHT_PROGBITS: u32 = 0x1; From a1e7268eb693d05b039dccd015563f0c6dcaed7e Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Mon, 22 Jun 2026 16:05:51 +1000 Subject: [PATCH 5/5] Make passive PD in initialiser rather than monitor Previously, when a task wants to be passive, it signals the monitor after its `init()` entrypoint returns. While this is fine for single core, there are 2 problems: 1. It will not scale/work in multi-core setups. Given that it is a non-blocking send, a scenario may occur where the monitor is already dealing with a message from one PD (meaning that it is not waiting on an endpoint) and another PD that wants to make itself passive on another core which means the message will be lost. 2. It affects verification as it leads to assumptions needing to be made about the scheduling of the system. Now, the process happens inside the capDL initialiser itself, which fixes all the problems above. Signed-off-by: Bill Nguyen --- Cargo.lock | 60 +++++++++++++++--------------- Cargo.toml | 8 ++-- libmicrokit/include/microkit.h | 2 +- libmicrokit/src/main.c | 13 ------- monitor/src/main.c | 16 -------- tool/microkit/src/capdl/builder.rs | 41 +++----------------- 6 files changed, 40 insertions(+), 100 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 310899960..8a7cbdad2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -494,7 +494,7 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "sel4" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "cfg-if", "sel4-config", @@ -504,7 +504,7 @@ dependencies = [ [[package]] name = "sel4-alloca" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "cfg-if", ] @@ -512,7 +512,7 @@ dependencies = [ [[package]] name = "sel4-bitfield-ops" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "rustversion", ] @@ -520,12 +520,12 @@ dependencies = [ [[package]] name = "sel4-build-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-capdl-initializer" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "log", "rkyv", @@ -543,7 +543,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "miniz_oxide", "rkyv", @@ -555,7 +555,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types-derive" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "proc-macro2", "quote", @@ -565,7 +565,7 @@ dependencies = [ [[package]] name = "sel4-config" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "prettyplease", "proc-macro2", @@ -579,7 +579,7 @@ dependencies = [ [[package]] name = "sel4-config-data" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "sel4-build-env", "sel4-config-types", @@ -589,7 +589,7 @@ dependencies = [ [[package]] name = "sel4-config-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "fallible-iterator", "proc-macro2", @@ -602,7 +602,7 @@ dependencies = [ [[package]] name = "sel4-config-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "serde", ] @@ -610,12 +610,12 @@ dependencies = [ [[package]] name = "sel4-ctors-dtors" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-dlmalloc" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "dlmalloc", "lock_api", @@ -624,17 +624,17 @@ dependencies = [ [[package]] name = "sel4-immediate-sync-once-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-immutable-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-initialize-tls" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "cfg-if", "sel4-alloca", @@ -643,7 +643,7 @@ dependencies = [ [[package]] name = "sel4-logging" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "lock_api", "log", @@ -652,12 +652,12 @@ dependencies = [ [[package]] name = "sel4-no-allocator" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-panicking" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "cfg-if", "sel4-immediate-sync-once-cell", @@ -668,12 +668,12 @@ dependencies = [ [[package]] name = "sel4-panicking-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-phdrs" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "sel4-phdrs-constants", ] @@ -681,12 +681,12 @@ dependencies = [ [[package]] name = "sel4-phdrs-constants" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-phdrs-patched" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "sel4-phdrs", "sel4-rodata-static", @@ -695,12 +695,12 @@ dependencies = [ [[package]] name = "sel4-rodata-static" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-root-task" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "sel4", "sel4-dlmalloc", @@ -715,7 +715,7 @@ dependencies = [ [[package]] name = "sel4-root-task-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "proc-macro2", "quote", @@ -725,7 +725,7 @@ dependencies = [ [[package]] name = "sel4-runtime-common" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "cfg-if", "sel4", @@ -741,12 +741,12 @@ dependencies = [ [[package]] name = "sel4-stack" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [[package]] name = "sel4-sync" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "lock_api", "sel4", @@ -756,7 +756,7 @@ dependencies = [ [[package]] name = "sel4-sys" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=c30d0e44fb32c15239049ce402ef2a8c72499aa3#c30d0e44fb32c15239049ce402ef2a8c72499aa3" +source = "git+https://github.com/au-ts/rust-sel4?rev=d20b04cc16f4e5f1018213a3d3e9a45e0352724b#d20b04cc16f4e5f1018213a3d3e9a45e0352724b" dependencies = [ "bindgen", "glob", diff --git a/Cargo.toml b/Cargo.toml index 166c88961..703c9329d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,12 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/seL4/rust-sel4" -rev = "c30d0e44fb32c15239049ce402ef2a8c72499aa3" +git = "https://github.com/au-ts/rust-sel4" +rev = "d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/seL4/rust-sel4" -rev = "c30d0e44fb32c15239049ce402ef2a8c72499aa3" +git = "https://github.com/au-ts/rust-sel4" +rev = "d20b04cc16f4e5f1018213a3d3e9a45e0352724b" [profile.release.package.microkit-tool] strip = true diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 1b59319d2..3551334f2 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -19,7 +19,7 @@ typedef unsigned int microkit_child; typedef unsigned int microkit_ioport; typedef seL4_MessageInfo_t microkit_msginfo; -#define MONITOR_EP 5 +/* Index 5 is unused */ /* Only valid in the 'benchmark' configuration */ #define TCB_CAP 6 /* Only valid when the PD has been configured to make SMC calls */ diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c index 8719d4950..668bb2b3c 100644 --- a/libmicrokit/src/main.c +++ b/libmicrokit/src/main.c @@ -200,18 +200,5 @@ void main(void) { run_init_funcs(); init(); - - /* - * If we are passive, now our initialisation is complete we can - * signal the monitor to unbind our scheduling context and bind - * it to our notification object. - * We delay this signal so we are ready waiting on a recv() syscall - */ - if (microkit_passive) { - microkit_have_signal = seL4_True; - microkit_signal_msg = seL4_MessageInfo_new(0, 0, 0, 0); - microkit_signal_cap = MONITOR_EP; - } - handler_loop(); } diff --git a/monitor/src/main.c b/monitor/src/main.c index 028600477..a954d3ec6 100644 --- a/monitor/src/main.c +++ b/monitor/src/main.c @@ -26,8 +26,6 @@ #define REPLY_CAP 2 #define BASE_PD_TCB_CAP 10 #define BASE_VM_TCB_CAP 74 -#define BASE_SCHED_CONTEXT_CAP 138 -#define BASE_NOTIFICATION_CAP 202 extern seL4_IPCBuffer __sel4_ipc_buffer_obj; seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj; @@ -731,20 +729,6 @@ static void monitor(void) seL4_Word pd_id = badge - 1; seL4_Word tcb_cap = BASE_PD_TCB_CAP + pd_id; - if (label == seL4_Fault_NullFault && pd_id < MAX_PDS) { - /* This is a request from our PD to become passive */ - err = seL4_SchedContext_Bind(BASE_SCHED_CONTEXT_CAP + pd_id, BASE_NOTIFICATION_CAP + pd_id); - if (err != seL4_NoError) { - puts("MON|ERROR: could not bind scheduling context to notification object\n"); - } else { - puts("MON|INFO: PD '"); - puts(pd_names[pd_id]); - puts("' is now passive!\n"); - } - - continue; - } - puts("MON|ERROR: received message "); puthex32(label); puts(" badge: "); diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 5bb401be0..cc7bbf6db 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -74,16 +74,13 @@ const MON_FAULT_EP_CAP_IDX: u64 = 1; const MON_REPLY_CAP_IDX: u64 = 2; const MON_BASE_PD_TCB_CAP: u64 = 10; const MON_BASE_VM_TCB_CAP: u64 = MON_BASE_PD_TCB_CAP + 64; -const MON_BASE_SCHED_CONTEXT_CAP: u64 = MON_BASE_VM_TCB_CAP + 64; -const MON_BASE_NOTIFICATION_CAP: u64 = MON_BASE_SCHED_CONTEXT_CAP + 64; // Where caps must be in a PD's CSpace const PD_INPUT_CAP_IDX: u64 = 1; const PD_FAULT_EP_CAP_IDX: u64 = 2; const PD_VSPACE_CAP_IDX: u64 = 3; const PD_REPLY_CAP_IDX: u64 = 4; -// Valid only if the PD is passive. -const PD_MONITOR_EP_CAP_IDX: u64 = 5; +// Index 5 is unused // Valid only in benchmark configuration. const PD_TCB_CAP_IDX: u64 = 6; const PD_ARM_SMC_CAP_IDX: u64 = 7; @@ -346,6 +343,7 @@ impl CapDLSpecContainer { gprs: Vec::new(), master_fault_ep: None, domain: None, + passive: false, }; let tcb_inner_obj = object::Tcb { @@ -742,21 +740,6 @@ pub fn build_capdl_spec( pd_fault_ep_cap.clone(), )); - // Step 3-6 Create cap to Monitor's endpoint for passive PDs. - if pd.passive { - let pd_monitor_ep_cap = capdl_util_make_endpoint_cap( - mon_fault_ep_obj_id, - true, - true, - true, - pd_global_idx as u64 + 1, - ); - caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( - PD_MONITOR_EP_CAP_IDX as u32, - pd_monitor_ep_cap, - )); - } - // Step 3-7 Create endpoint object for the PD if it has children or can receive PPCs, else it will be a notification let pd_ntfn_obj_id = capdl_util_make_ntfn_obj(&mut spec_container, &pd.name); let pd_ntfn_cap = capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0); @@ -970,6 +953,7 @@ pub fn build_capdl_spec( gprs: [].to_vec(), master_fault_ep: None, // Not used on MCS kernel. domain: None, + passive: false, // VMs should not be passive. }), }; let vm_vcpu_tcb_obj_id = spec_container.add_root_object(NamedObject { @@ -1033,6 +1017,7 @@ pub fn build_capdl_spec( pd_tcb.extra.max_prio = pd.priority; pd_tcb.extra.fpu_disabled = !pd.fpu; pd_tcb.extra.resume = true; + pd_tcb.extra.passive = pd.passive; pd_tcb.slots.extend(caps_to_bind_to_tcb); // Stylistic purposes only @@ -1043,29 +1028,13 @@ pub fn build_capdl_spec( // Step 3-15 bind this PD's TCB to the monitor, this accomplish two purposes: // 1. Allow PDs' TCBs to be named to their proper name in SDF in debug config. - // 2. Allow passive PDs. + // 2. Allow the PD's execution thread registers to be printed on a fault. capdl_util_insert_cap_into_cspace( &mut spec_container, mon_cnode_obj_id, (MON_BASE_PD_TCB_CAP as usize + pd_global_idx) as u32, capdl_util_make_tcb_cap(pd_tcb_obj_id), ); - if pd.passive { - // When a PD is passive, it will signal the Monitor once init() returns. The monitor will - // then unbind the PD's TCB from its Scheduling Context and bind it to its Notification. - capdl_util_insert_cap_into_cspace( - &mut spec_container, - mon_cnode_obj_id, - (MON_BASE_SCHED_CONTEXT_CAP as usize + pd_global_idx) as u32, - capdl_util_make_sc_cap(pd_sc_obj_id), - ); - capdl_util_insert_cap_into_cspace( - &mut spec_container, - mon_cnode_obj_id, - (MON_BASE_NOTIFICATION_CAP as usize + pd_global_idx) as u32, - capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0), - ); - } pd_shadow_cspaces.insert( pd_global_idx,