Skip to content

Commit

Permalink
crates/sel4-microkit: Factor out runtime
Browse files Browse the repository at this point in the history
Signed-off-by: Nick Spinale <[email protected]>
  • Loading branch information
nspin committed Feb 28, 2024
1 parent 2f8fad9 commit 25e7f8d
Show file tree
Hide file tree
Showing 23 changed files with 470 additions and 404 deletions.
13 changes: 10 additions & 3 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,7 @@ members = [
"crates/sel4-kernel-loader/payload-types",
"crates/sel4-logging",
"crates/sel4-microkit",
"crates/sel4-microkit/base",
"crates/sel4-microkit/macros",
"crates/sel4-microkit/message",
"crates/sel4-microkit/message/types",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ impl Handler for HandlerImpl {
type Error = Infallible;

fn notified(&mut self, _channel: Channel) -> Result<(), Self::Error> {
self.deferred_action.defer(CLIENT.defer_notify()).unwrap();
self.deferred_action.defer_notify(CLIENT).unwrap();
Ok(())
}

Expand Down
7 changes: 3 additions & 4 deletions crates/sel4-microkit/Cargo.nix
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,13 @@ mk {
dependencies = {
inherit (versions) cfg-if;
inherit (localCrates)
sel4-panicking
sel4-panicking-env
sel4-immediate-sync-once-cell
sel4-immutable-cell
sel4-panicking-env
sel4-panicking
sel4-dlmalloc
sel4-sync
sel4-microkit-base
sel4-microkit-macros
sel4-externally-shared
;
sel4-runtime-common = localCrates.sel4-runtime-common // { features = [ "tls" "unwinding" "start" ]; };
sel4 = localCrates.sel4 // { features = [ "single-threaded" ]; };
Expand Down
3 changes: 1 addition & 2 deletions crates/sel4-microkit/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,8 @@ unwinding = ["sel4-panicking/unwinding"]
cfg-if = "1.0.0"
sel4 = { path = "../sel4", features = ["single-threaded"] }
sel4-dlmalloc = { path = "../sel4-dlmalloc" }
sel4-externally-shared = { path = "../sel4-externally-shared" }
sel4-immediate-sync-once-cell = { path = "../sel4-immediate-sync-once-cell" }
sel4-immutable-cell = { path = "../sel4-immutable-cell" }
sel4-microkit-base = { path = "base" }
sel4-microkit-macros = { path = "macros" }
sel4-panicking = { path = "../sel4-panicking" }
sel4-panicking-env = { path = "../sel4-panicking/env" }
Expand Down
20 changes: 20 additions & 0 deletions crates/sel4-microkit/base/Cargo.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
#
# Copyright 2023, Colias Group, LLC
#
# SPDX-License-Identifier: BSD-2-Clause
#

{ mk, localCrates }:

mk {
package.name = "sel4-microkit-base";
dependencies = {
inherit (localCrates)
sel4-immutable-cell
sel4
;
};
features = {
extern-symbols = [];
};
}
24 changes: 24 additions & 0 deletions crates/sel4-microkit/base/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
#
# Copyright 2023, Colias Group, LLC
#
# SPDX-License-Identifier: BSD-2-Clause
#
#
# This file is generated from './Cargo.nix'. You can edit this file directly
# if you are not using this project's Cargo manifest management tools.
# See 'hacking/cargo-manifest-management/README.md' for more information.
#

[package]
name = "sel4-microkit-base"
version = "0.1.0"
authors = ["Nick Spinale <[email protected]>"]
edition = "2021"
license = "BSD-2-Clause"

[features]
extern-symbols = []

[dependencies]
sel4 = { path = "../../sel4" }
sel4-immutable-cell = { path = "../../sel4-immutable-cell" }
81 changes: 81 additions & 0 deletions crates/sel4-microkit/base/src/channel.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
//
// Copyright 2023, Colias Group, LLC
//
// SPDX-License-Identifier: BSD-2-Clause
//

use core::fmt;

use crate::MessageInfo;

const BASE_OUTPUT_NOTIFICATION_SLOT: usize = 10;
const BASE_ENDPOINT_SLOT: usize = BASE_OUTPUT_NOTIFICATION_SLOT + 64;
const BASE_IRQ_SLOT: usize = BASE_ENDPOINT_SLOT + 64;

const MAX_CHANNELS: usize = 63;

/// A channel between this protection domain and another, identified by a channel index.
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
pub struct Channel {
index: usize,
}

impl Channel {
pub const fn new(index: usize) -> Self {
assert!(index < MAX_CHANNELS);
Self { index }
}

fn cap<T: sel4::CapType>(&self, base_slot: usize) -> sel4::Cap<T> {
sel4::Cap::from_bits((base_slot + self.index) as sel4::CPtrBits)
}

#[doc(hidden)]
pub fn notification(&self) -> sel4::Notification {
self.cap::<sel4::cap_type::Notification>(BASE_OUTPUT_NOTIFICATION_SLOT)
}

#[doc(hidden)]
pub fn irq_handler(&self) -> sel4::IrqHandler {
self.cap::<sel4::cap_type::IrqHandler>(BASE_IRQ_SLOT)
}

#[doc(hidden)]
pub fn endpoint(&self) -> sel4::Endpoint {
self.cap::<sel4::cap_type::Endpoint>(BASE_ENDPOINT_SLOT)
}

pub fn notify(&self) {
self.notification().signal()
}

pub fn irq_ack(&self) -> Result<(), IrqAckError> {
self.irq_handler()
.irq_handler_ack()
.map_err(IrqAckError::from_inner)
}

pub fn pp_call(&self, msg_info: MessageInfo) -> MessageInfo {
MessageInfo::from_inner(self.endpoint().call(msg_info.into_inner()))
}
}

/// Error type returned by [`Channel::irq_ack`].
#[derive(Debug, PartialEq, Eq)]
pub struct IrqAckError(sel4::Error);

impl IrqAckError {
fn from_inner(inner: sel4::Error) -> Self {
Self(inner)
}

fn inner(&self) -> &sel4::Error {
&self.0
}
}

impl fmt::Display for IrqAckError {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "irq ack error: {:?}", self.inner())
}
}
25 changes: 25 additions & 0 deletions crates/sel4-microkit/base/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
//
// Copyright 2024, Colias Group, LLC
//
// SPDX-License-Identifier: BSD-2-Clause
//

#![no_std]
#![feature(used_with_arg)]

mod channel;
mod message;
mod symbols;

pub use channel::{Channel, IrqAckError};
pub use message::{
get_mr, set_mr, with_msg_bytes, with_msg_bytes_mut, with_msg_regs, with_msg_regs_mut,
MessageInfo, MessageLabel, MessageRegisterValue,
};
pub use symbols::{ipc_buffer_ptr, pd_is_passive, pd_name};

// For macros
#[doc(hidden)]
pub mod _private {
pub use sel4_immutable_cell::ImmutableCell;
}
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@
// SPDX-License-Identifier: BSD-2-Clause
//

//! Utilities for handling IPC messages for protected procedure calls.

pub type MessageLabel = sel4::Word;
pub type MessageRegisterValue = sel4::Word;

Expand All @@ -15,16 +13,18 @@ pub struct MessageInfo {
}

impl MessageInfo {
pub(crate) fn from_sel4(inner: sel4::MessageInfo) -> Self {
#[doc(hidden)]
pub fn from_inner(inner: sel4::MessageInfo) -> Self {
Self { inner }
}

pub(crate) fn into_sel4(self) -> sel4::MessageInfo {
#[doc(hidden)]
pub fn into_inner(self) -> sel4::MessageInfo {
self.inner
}

pub fn new(label: MessageLabel, count: usize) -> Self {
Self::from_sel4(sel4::MessageInfo::new(label, 0, 0, count))
Self::from_inner(sel4::MessageInfo::new(label, 0, 0, count))
}

pub fn label(&self) -> MessageLabel {
Expand Down
Loading

0 comments on commit 25e7f8d

Please sign in to comment.