github/sparrow-kata-full
1
0
Fork 0
mirror of https://github.com/AmbiML/sparrow-kata-full.git synced 2025-09-17 15:38:18 +00:00
Code Issues Projects Releases Wiki Activity

kata-os-model: misc fixups

Browse Source 
Fallout from rootserver memory reclamation work:
- add CDL_Object::next_free_slot
- add CONFIG_NOISY_UNTYPEDS feature for spammy debug msgs
- add CONFIG_NOISY_CREATE_OBJECT msgs
- assert if bootinfo/untyped_cnode setup is wrong instead of
  logging msgs and then failing later
- bury ugly BIT usage in is_obj_inside_untyped
- revise handoff_cap api for future use in memory reclamation
- remove some unneeded type coercions
- streamline printing seL4_CPath's
- simplify get_object & get_asid

Change-Id: Ib2c3d717dd41b307cb7afd4821dee4b6be173d57
GitOrigin-RevId: 99f4b79e1df257d373accf96190a77a65ba3305f
This commit is contained in:
Sam Leffler
2022-07-13 19:04:23 +00:00
parent 0539aae221
commit a28057ea73
4 changed files with 62 additions and 54 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
apps/system/components/kata-os-common/src/capdl/mod.rs
View File

@@ -649,6 +649,15 @@ impl<'a> CDL_Object {
pub fn num_slots(&self) -> seL4_Word {
self.slots.num
}
// Returns the next available slot past those specified in the spec.
// Note we cannot use num_slots since there may be gaps in the
// numbering due to empty slots.
#[inline]
pub fn next_free_slot(&self) -> seL4_Word {
self.slots_slice().iter()
.max_by_key(|slot| slot.slot)
.map_or(0, |slot| slot.slot + 1)
}
#[inline]
pub fn slot(&self, index: seL4_Word) -> CDL_CapSlot {
#[allow(unaligned_references)]

1
apps/system/components/kata-os-common/src/model/Cargo.toml
View File

@@ -31,6 +31,7 @@ CONFIG_PRINTING = []
CONFIG_SMP_SUPPORT = []
CONFIG_VTX = []
# Enable inclusion of noisy logging in various areas
CONFIG_NOISY_UNTYPEDS = []
CONFIG_NOISY_CREATE_OBJECT = []
CONFIG_NOISY_INIT_CNODE = []
CONFIG_NOISY_INIT_VSPACE = []

37
apps/system/components/kata-os-common/src/model/feature/dynamic_alloc.rs
View File

@@ -5,7 +5,7 @@ use capdl::CDL_FrameFill_BootInfoEnum_t::*;
use capdl::CDL_FrameFillType_t::*;
use capdl::CDL_ObjectType::*;
use crate::KataOsModel;
use log::{debug, info, trace};
use log::{debug, trace};
use smallvec::SmallVec;
use sel4_sys::seL4_ASIDControl_MakePool;
@@ -72,12 +72,9 @@ impl<'a> KataOsModel<'a> {
{
let free_slot = self.free_slot_start + free_slot_index;
// trace!(
// "Creating object {} in slot {} from untyped {:#x}...",
// obj.name(),
// free_slot,
// self.state.get_untyped_cptr(ut_index)
// );
#[cfg(feature = "CONFIG_NOISY_CREATE_OBJECT")]
trace!("Creating object {} in slot {} from untyped {:#x}...",
obj.name(), free_slot, self.state.get_untyped_cptr(ut_index));
// NB: create_object may use free_slot + 1 and free_slot + 2
while let Err(e) =
@@ -112,18 +109,18 @@ impl<'a> KataOsModel<'a> {
// NB: can instantiate multiple frames but only one
// CNode can receive the untypeds since we must move
// 'em from the rootserver (since they are "derived").
// XXX maybe just complain & ignore
trace!("Found bootinfo Frame at {}", obj_id);
assert!(!is_objid_valid(bootinfo_frame));
assert!(!is_objid_valid(bootinfo_frame),
"Duplicate bootinfo Frame at {}, prev {}",
obj_id, bootinfo_frame);
bootinfo_frame = obj_id;
}
}
// Look for a CNode associated with any bootinfo frame.
CDL_CNode => {
if obj.cnode_has_untyped_memory() {
if is_objid_valid(untyped_cnode) {
info!("Duplicate bootinfo cnode at {}, prev {}", obj_id, untyped_cnode);
}
assert!(!is_objid_valid(untyped_cnode),
"Duplicate bootinfo cnode at {}, prev {}",
obj_id, untyped_cnode);
untyped_cnode = obj_id;
}
}
@@ -216,16 +213,18 @@ impl<'a> KataOsModel<'a> {
if !ut.is_device() {
let index = ut.size_bits();
// trace!("Untyped {:3} (cptr={:#x}) (addr={:#x}) is of size {:2}. Placing in slot {}...",
// untyped_index, untyped_start + untyped_index, ut.paddr, index, count[index]);
#[cfg(feature = "CONFIG_NOISY_UNTYPEDS")]
trace!("Untyped {:3} (cptr={:#x}) (addr={:#x}) is of size {:2}. Placing in slot {}...",
untyped_index, untyped_start + untyped_index, ut.paddr, index, count[index]);
self.state
.set_untyped_cptr(count[index], untyped_start + untyped_index);
count[index] += 1;
num_normal_untypes += 1;
} else {
// trace!("Untyped {:3} (cptr={:#x}) (addr={:#x}) is of size {:2}. Skipping as it is device",
// untyped_index, untyped_start + untyped_index, ut.paddr, ut.size_bits());
#[cfg(feature = "CONFIG_NOISY_UNTYPEDS")]
trace!("Untyped {:3} (cptr={:#x}) (addr={:#x}) is of size {:2}. Skipping as it is device",
untyped_index, untyped_start + untyped_index, ut.paddr, ut.size_bits());
}
}
num_normal_untypes
@@ -292,7 +291,7 @@ impl<'a> KataOsModel<'a> {
obj_size_bits: usize,
ut: &seL4_UntypedDesc,
) -> bool {
ut.paddr <= obj_addr && obj_addr + obj_size_bits <= ut.paddr + BIT(ut.size_bits())
ut.paddr <= obj_addr && obj_addr + BIT(obj_size_bits) <= ut.paddr + BIT(ut.size_bits())
}
fn get_address(ut_slot: seL4_CPtr) -> Result<seL4_Page_GetAddress, seL4_Error> {
// Create a temporary frame to get the address. We load this at slot + 2
@@ -316,7 +315,7 @@ impl<'a> KataOsModel<'a> {
}
}
if is_obj_inside_untyped(paddr, BIT(obj_size_bits), &untypedList[i]) {
if is_obj_inside_untyped(paddr, obj_size_bits, &untypedList[i]) {
// See above, loop looking for a Frame in the untyped object
// that matches our object's address. If we run out of space
// in the untyped the kernel will return seL4_NotEnoughMemory

69
apps/system/components/kata-os-common/src/model/mod.rs
View File

@@ -229,7 +229,7 @@ impl<'a> KataOsModel<'a> {
// as part of the work done by init_cspsace.
if is_objid_valid(self.untyped_cnode) {
self.handoff_untypeds(self.untyped_cnode)?;
self.handoff_untypeds()?;
}
Ok(())
}
@@ -885,15 +885,16 @@ impl<'a> KataOsModel<'a> {
Ok(())
}
fn handoff_untypeds(&mut self, cnode_obj_id: CDL_ObjID) -> seL4_Result {
let num_untypeds = self.bootinfo.untyped.end - self.bootinfo.untyped.start;
pub fn handoff_untypeds(&mut self) -> seL4_Result {
assert!(is_objid_valid(self.untyped_cnode), "No handoff CNode found");
// NB: UntypedMemory caps are appended to the CAmkES-generated slots
let dest_start = self.spec.obj_slice()[cnode_obj_id]
.slots_slice()
.iter()
.max_by_key(|slot| slot.slot)
.map_or(0, |slot| slot.slot + 1);
// UntypedMemory caps are appended to the CAmkES-generated slots
// in the CNode identified for handoff. CAmkES is assumed to have
// sized the CNode to handle moving the untyped memory slabs.
let cnode = self.get_object(self.untyped_cnode);
let dest_root = self.get_orig_cap(self.untyped_cnode);
let dest_start = cnode.next_free_slot();
let num_untypeds = self.bootinfo.untyped.end - self.bootinfo.untyped.start;
trace!("Hand-off {} untypeds from {} to {}",
num_untypeds,
@@ -901,26 +902,27 @@ impl<'a> KataOsModel<'a> {
dest_start);
// NB: we let kernel tell us if the CNode is too small.
for ut in 0..num_untypeds {
self.handoff_cap(cnode_obj_id,
self.handoff_cap(self.untyped_cnode,
/*src_index=*/ self.bootinfo.untyped.start + ut,
/*dest_root=*/ dest_root,
/*dest_index=*/ dest_start + ut)?;
}
Ok(())
}
fn handoff_cap(
&mut self,
&self,
cnode_obj_id: CDL_ObjID,
src_index: seL4_CPtr,
dest_root: seL4_CPtr,
dest_index: seL4_CPtr
) -> seL4_Result {
let cnode = &self.spec.obj_slice()[cnode_obj_id];
let cnode = self.get_object(cnode_obj_id);
assert_eq!(cnode.r#type(), CDL_CNode);
let src_root = seL4_CapInitThreadCNode;
let src_depth = seL4_WordBits as u8;
let dest_root = self.get_orig_cap(cnode_obj_id);
let dest_depth: u8 = cnode.size_bits.try_into().unwrap();
unsafe {
@@ -991,11 +993,11 @@ impl<'a> KataOsModel<'a> {
CDL_SchedControlCap => (false, self.get_sched_ctrl_cap(target_cap_obj)),
CDL_DomainCap => {
// there's only one cap
(false, seL4_CapDomain as seL4_CPtr)
(false, seL4_CapDomain)
}
CDL_ASIDControlCap => {
// there's only one cap
(false, seL4_CapASIDControl as seL4_CPtr)
(false, seL4_CapASIDControl)
}
_ => (false, self.get_orig_cap(target_cap_obj)),
};
@@ -1004,22 +1006,22 @@ impl<'a> KataOsModel<'a> {
if mode == InitCnodeCmode::MOVE && move_cap {
if is_ep_cap || is_irq_handler_cap {
#[cfg(feature = "CONFIG_NOISY_INIT_CNODE")]
debug!(" Populate {:?} slot {} by moving {}:{}:{} -> {}:{}:{}",
debug!(" Populate {:?} slot {} by moving {:?} -> {:?}",
target_cap_type, cnode_slot.slot,
src_root, src_index, src_depth,
dest_root, dest_index, dest_depth,
(src_root, src_index, src_depth),
(dest_root, dest_index, dest_depth),
);
unsafe {
seL4_CNode_Move(
dest_root, dest_index, dest_depth, src_root, src_index, src_depth,
)
}?
}?;
} else {
#[cfg(feature = "CONFIG_NOISY_INIT_CNODE")]
debug!(" Populate {:?} slot {} by mutating {}:{}:{} -> {}:{}:{}",
debug!(" Populate {:?} slot {} by mutating {:?} -> {:?}",
target_cap_type, cnode_slot.slot,
src_root, src_index, src_depth,
dest_root, dest_index, dest_depth,
(src_root, src_index, src_depth),
(dest_root, dest_index, dest_depth),
);
unsafe {
seL4_CNode_Mutate(
@@ -1052,10 +1054,10 @@ impl<'a> KataOsModel<'a> {
// NB: the mapped frame cap is stored in the dup table.
let mapped_frame_cap = self.get_dup_cap(frame_cap.obj_id);
#[cfg(feature = "CONFIG_NOISY_INIT_CNODE")]
debug!(" Map {:?} slot {} by moving {}:{}:{} -> {}:{}:{}",
debug!(" Map {:?} slot {} by moving {:?} -> {:?}",
target_cap_type, cnode_slot.slot,
src_root, mapped_frame_cap, src_depth,
dest_root, dest_index, dest_depth,
(src_root, mapped_frame_cap, src_depth),
(dest_root, dest_index, dest_depth),
);
// Move the cap to the frame used for the mapping into the
// destination slot.
@@ -1071,10 +1073,10 @@ impl<'a> KataOsModel<'a> {
}?;
} else {
#[cfg(feature = "CONFIG_NOISY_INIT_CNODE")]
debug!(" Populate {:?} slot {} by minting {}:{}:{} -> {}:{}:{} {:?} data {:#x}",
debug!(" Populate {:?} slot {} by minting {:?} -> {:?} {:?} data {:#x}",
target_cap_type, cnode_slot.slot,
src_root, src_index, src_depth,
dest_root, dest_index, dest_depth,
(src_root, src_index, src_depth),
(dest_root, dest_index, dest_depth),
target_cap_rights, target_cap_data,
);
unsafe {
@@ -1095,13 +1097,10 @@ impl<'a> KataOsModel<'a> {
}
fn get_object(&self, object_id: CDL_ObjID) -> &'a CDL_Object {
&(unsafe { core::slice::from_raw_parts(self.spec.objects, self.spec.num) }[object_id])
&self.spec.obj_slice()[object_id]
}
fn get_asid(&self, asid_num: usize) -> Option<CDL_ObjID> {
Some(
unsafe { core::slice::from_raw_parts(self.spec.asid_slots, self.spec.num_asid_slots) }
[asid_num],
)
Some(self.spec.asid_slot_slice()[asid_num])
}
// Top-level CSpace management: a one-level CSpace impl for now
@@ -1146,7 +1145,7 @@ impl<'a> KataOsModel<'a> {
// interrupt notifications and fault endpoints when MCS is enabled.
fn mint_cap(
&mut self,
object_id: CDL_ObjID,
obj_id: CDL_ObjID,
badge: seL4_Word,
) -> Result<seL4_CPtr, seL4_Error> {
let seL4_AllRights = seL4_CapRights::new(
@@ -1159,7 +1158,7 @@ impl<'a> KataOsModel<'a> {
/*dest_index=*/ free_slot,
/*dest_depth*/ seL4_WordBits as u8,
/*src_root=*/ seL4_CapInitThreadCNode,
/*src_index=*/ self.get_orig_cap(object_id),
/*src_index=*/ self.get_orig_cap(obj_id),
/*src_depth=*/ seL4_WordBits as u8,
seL4_AllRights,
badge,