diff --git a/crates/sel4-capdl-initializer/src/initialize.rs b/crates/sel4-capdl-initializer/src/initialize.rs index da2f0a7c0..1c7585a64 100644 --- a/crates/sel4-capdl-initializer/src/initialize.rs +++ b/crates/sel4-capdl-initializer/src/initialize.rs @@ -1053,6 +1053,82 @@ impl<'a> Initializer<'a> { Ok(()) } + #[sel4::sel4_cfg(KERNEL_MCS)] + fn us_to_ticks(&self, duration_us: u64) -> Result { + sel4::sel4_cfg_if! { + if #[sel4_cfg(any(ARCH_ARM, ARCH_RISCV))] { + const US_IN_SECOND: u64 = 1000 * 1000; + + // On 32-bit platforms, Word is 32-bits, but on 64-bit platforms + // it is also a u64 and deemed "unnecessary". + #[allow(clippy::useless_conversion)] + let f: u64 = sel4::sel4_cfg_word!(TIMER_FREQUENCY).into(); + + // TODO: Formal correctness of this implementation + // https://github.com/seL4/capdl/issues/98 + // See also the corresponding implementation in capDL. + + if (duration_us / US_IN_SECOND) >= (1u64 << 56) / f { + panic!( + "Input us {duration_us} would overflow 64-bits of \ + exceed 56-bit output tick maximum @ freq {f} Hz" + ); + } + + let s: u64 = duration_us / US_IN_SECOND; + let us: u64 = duration_us % US_IN_SECOND; + + // The '+ US_IN_S / 2' implements round-to-nearest behaviour + let ticks = s * f + ((us * f + US_IN_SECOND / 2) / US_IN_SECOND); + + Ok(ticks) + } else if #[sel4_cfg(any(ARCH_X86, ARCH_X86_64))] { + let tsc_freq_bi = self + .bootinfo + .extra() + .find(|bi| bi.id == sel4::BootInfoExtraId::X86TscFreq) + .expect("Unable to determine timer frequency as \ + no TSC frequency provided in bootinfo"); + + // For x86 platforms, the timer frequency is provided in MHz by the bootinfo + let tsc_freq_mhz = u32::from_le_bytes(tsc_freq_bi.content().try_into().unwrap()); + + let ticks = duration_us + .checked_mul(tsc_freq_mhz.into()) + .expect(format!( + "Output would overflow when computing ticks for duration \ + {duration_us} us @ freq {tsc_freq_mhz} MHz")); + + Ok(ticks) + } else { + compile_error!("unsupported architecture"); + } + } + } + + #[sel4::sel4_cfg(not(KERNEL_MCS))] + fn us_to_ticks(&self, duration_us: u64) -> Result { + // On non-MCS, 1 tick is equivalent to 1 TIMER_TICK_MS, or an integer multiple + // of 1 millisecond. + + // On 32-bit platforms, Word is 32-bits, but on 64-bit platforms it is + // also a u64 and deemed "unnecessary". + #[allow(clippy::unnecessary_cast)] + const TIMER_TICK_MS: u64 = sel4::sel4_cfg_word!(TIMER_TICK_MS) as u64; + let period_us: u64 = 1000 * TIMER_TICK_MS; + let ticks: u64 = duration_us / period_us; + let remainder: u64 = duration_us % period_us; + + if remainder != 0 { + panic!( + "domain schedule duration {duration_us} is not an \ + integer multiple of TIMER_TICK_MS ({TIMER_TICK_MS} ms)" + ); + } + + Ok(ticks) + } + fn init_domain_schedule(&self) -> Result<()> { if let ArchivedOption::Some(domain_schedule) = &self.spec.domain_schedule { debug!("Initializing domain schedule"); @@ -1066,11 +1142,17 @@ impl<'a> Initializer<'a> { // sched_index is used as a shift, and not an invariant for the loop. #[allow(clippy::explicit_counter_loop)] - for ArchivedDomainSchedEntry { id, time } in domain_schedule.iter() { - let domain_time = *time; + for ArchivedDomainSchedEntry { domain, duration } in domain_schedule.iter() { + let duration_ticks: u64 = match *duration { + ArchivedDomainSchedDuration::Ticks(ticks) => ticks.get(), + ArchivedDomainSchedDuration::Us(us) => self.us_to_ticks(us.get())?, + ArchivedDomainSchedDuration::EndMarker => 0, + }; + init_thread::slot::DOMAIN_SET .cap() - .domain_set_schedule_configure(sched_index, *id, domain_time.to_native())?; + .domain_set_schedule_configure(sched_index, *domain, duration_ticks)?; + sched_index += 1; } } @@ -1078,25 +1160,30 @@ impl<'a> Initializer<'a> { } fn start_domain_schedule(&self) -> Result<()> { - if self.spec.domain_schedule.is_some() { - debug!("Starting domain schedule"); + if self.spec.domain_schedule.is_none() { + return Ok(()); + } - // The start index also needs to be shifted. This makes the shift - // an offset into the schedule rather than an absolute index. - let shift = self - .spec - .domain_idx_shift - .as_ref() - .map(ArchivedWord::to_sel4) - .unwrap_or(0); + // Only call set start if we have been given a start index + let ArchivedOption::Some(start) = self.spec.domain_set_start else { + return Ok(()); + }; + + debug!("Starting domain schedule"); + + // The start index also needs to be shifted. This makes the shift + // an offset into the schedule rather than an absolute index. + let shift = self + .spec + .domain_idx_shift + .as_ref() + .map(ArchivedWord::to_sel4) + .unwrap_or(0); + + init_thread::slot::DOMAIN_SET + .cap() + .domain_set_schedule_set_start(start.to_sel4() + shift)?; - // Only call set start if we have been given a start index - if let ArchivedOption::Some(start) = self.spec.domain_set_start { - init_thread::slot::DOMAIN_SET - .cap() - .domain_set_schedule_set_start(start.to_sel4() + shift)?; - } - } Ok(()) } diff --git a/crates/sel4-capdl-initializer/types/src/spec.rs b/crates/sel4-capdl-initializer/types/src/spec.rs index 4126b9621..5524c9058 100644 --- a/crates/sel4-capdl-initializer/types/src/spec.rs +++ b/crates/sel4-capdl-initializer/types/src/spec.rs @@ -7,6 +7,7 @@ use alloc::boxed::Box; use alloc::string::String; use alloc::vec::Vec; +use core::num::NonZero; use core::ops::Range; use rkyv::Archive; @@ -143,12 +144,21 @@ pub struct IrqEntry { pub handler: ObjectId, } +#[derive(Debug, Clone, Copy, Eq, PartialEq)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[derive(rkyv::Archive, rkyv::Serialize)] +pub enum DomainSchedDuration { + Ticks(NonZero), + Us(NonZero), + EndMarker, +} + #[derive(Debug, Clone, Copy, Eq, PartialEq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] #[derive(rkyv::Archive, rkyv::Serialize)] pub struct DomainSchedEntry { - pub id: u8, - pub time: u64, + pub domain: u8, + pub duration: DomainSchedDuration, } pub type AsidSlotEntry = ObjectId; diff --git a/crates/sel4/src/invocations.rs b/crates/sel4/src/invocations.rs index d880ffc82..a682e1711 100644 --- a/crates/sel4/src/invocations.rs +++ b/crates/sel4/src/invocations.rs @@ -19,7 +19,6 @@ use crate::{ use crate::Badge; /// Corresponds to `seL4_Time`. -#[sel4_cfg(KERNEL_MCS)] pub type Time = u64; impl Untyped { @@ -413,7 +412,7 @@ impl DomainSet { self, index: Word, domain: u8, - duration: u64, + duration: Time, ) -> Result<()> { Error::wrap(self.invoke(|cptr, ipc_buffer| { ipc_buffer.inner_mut().seL4_DomainSet_ScheduleConfigure( diff --git a/crates/sel4/src/lib.rs b/crates/sel4/src/lib.rs index 5eb789f11..f5adb235e 100644 --- a/crates/sel4/src/lib.rs +++ b/crates/sel4/src/lib.rs @@ -125,7 +125,7 @@ pub use cptr::{ pub use error::{Error, Result}; pub use fault::*; pub use invocation_context::{InvocationContext, NoExplicitInvocationContext, NoInvocationContext}; -pub use invocations::TcbFlagsBuilder; +pub use invocations::{TcbFlagsBuilder, Time}; pub use ipc_buffer::IpcBuffer; pub use message_info::{MessageInfo, MessageInfoBuilder}; pub use object::{ @@ -139,14 +139,10 @@ pub use vspace::{ vspace_levels, }; -sel4_cfg_if! { - if #[sel4_cfg(KERNEL_MCS)] { - pub use invocations::Time; - } else { - pub use syscalls::reply; - pub use reply_authority::ImplicitReplyAuthority; - } -} +#[sel4_cfg(not(KERNEL_MCS))] +pub use reply_authority::ImplicitReplyAuthority; +#[sel4_cfg(not(KERNEL_MCS))] +pub use syscalls::reply; #[sel4_cfg(SET_TLS_BASE_SELF)] pub use syscalls::set_tls_base;