Skip to content

Commit

Permalink
Remove dependence on setvar patch for Microkit
Browse files Browse the repository at this point in the history
Signed-off-by: Nick Spinale <[email protected]>
  • Loading branch information
nspin committed Oct 31, 2023
1 parent c55256d commit 78a2a98
Show file tree
Hide file tree
Showing 10 changed files with 107 additions and 53 deletions.
9 changes: 0 additions & 9 deletions crates/examples/microkit/http-server/http-server.system
Original file line number Diff line number Diff line change
Expand Up @@ -27,15 +27,13 @@
<program_image path="microkit-http-server-example-server.elf" />

<map mr="virtio_net_client_dma" vaddr="0x1_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_client_dma_vaddr" />
<setvar symbol="virtio_net_client_dma_size" vaddr="0x200_000" />

<map mr="virtio_net_rx_free" vaddr="0x2_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_rx_free" />
<map mr="virtio_net_rx_used" vaddr="0x2_001_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_rx_used" />
<map mr="virtio_net_tx_free" vaddr="0x2_002_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_tx_free" />
<map mr="virtio_net_tx_used" vaddr="0x2_003_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_tx_used" />

<map mr="virtio_blk_client_dma" vaddr="0x3_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_blk_client_dma_vaddr" />
<setvar symbol="virtio_blk_client_dma_size" vaddr="0x200_000" />

<map mr="virtio_blk_free" vaddr="0x4_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_blk_free" />
<map mr="virtio_blk_used" vaddr="0x4_001_000_000" perms="rw" cached="true" setvar_vaddr="virtio_blk_used" />
Expand All @@ -45,21 +43,17 @@
<program_image path="microkit-http-server-example-sp804-driver.elf" />
<map mr="sp804_mmio" vaddr="0x5_000_000_000" perms="rw" cached="false" setvar_vaddr="sp804_mmio_vaddr" />
<irq irq="43" id="0" />
<setvar symbol="freq" vaddr="1_000_000" />
</protection_domain>

<protection_domain name="virtio_net_driver" pp="true" priority="253">
<program_image path="microkit-http-server-example-virtio-net-driver.elf" />

<map mr="virtio_mmio" vaddr="0x6_000_000_000" perms="rw" cached="false" setvar_vaddr="virtio_net_mmio_vaddr" />
<setvar symbol="virtio_net_mmio_offset" vaddr="0xe00" />

<map mr="virtio_net_driver_dma" vaddr="0x7_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_driver_dma_vaddr" />
<setvar symbol="virtio_net_driver_dma_size" vaddr="0x200_000" />
<setvar symbol="virtio_net_driver_dma_paddr" region_paddr="virtio_net_driver_dma" />

<map mr="virtio_net_client_dma" vaddr="0x1_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_client_dma_vaddr" />
<setvar symbol="virtio_net_client_dma_size" vaddr="0x200_000" />

<map mr="virtio_net_rx_free" vaddr="0x2_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_rx_free" />
<map mr="virtio_net_rx_used" vaddr="0x2_001_000_000" perms="rw" cached="true" setvar_vaddr="virtio_net_rx_used" />
Expand All @@ -73,14 +67,11 @@
<program_image path="microkit-http-server-example-virtio-blk-driver.elf" />

<map mr="virtio_mmio" vaddr="0x6_000_000_000" perms="rw" cached="false" setvar_vaddr="virtio_blk_mmio_vaddr" />
<setvar symbol="virtio_blk_mmio_offset" vaddr="0xc00" />

<map mr="virtio_blk_driver_dma" vaddr="0x8_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_blk_driver_dma_vaddr" />
<setvar symbol="virtio_blk_driver_dma_size" vaddr="0x200_000" />
<setvar symbol="virtio_blk_driver_dma_paddr" region_paddr="virtio_blk_driver_dma" />

<map mr="virtio_blk_client_dma" vaddr="0x3_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_blk_client_dma_vaddr" />
<setvar symbol="virtio_blk_client_dma_size" vaddr="0x200_000" />

<map mr="virtio_blk_free" vaddr="0x4_000_000_000" perms="rw" cached="true" setvar_vaddr="virtio_blk_free" />
<map mr="virtio_blk_used" vaddr="0x4_001_000_000" perms="rw" cached="true" setvar_vaddr="virtio_blk_used" />
Expand Down
16 changes: 16 additions & 0 deletions crates/examples/microkit/http-server/pds/server/src/config.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
//
// Copyright 2023, Colias Group, LLC
//
// SPDX-License-Identifier: BSD-2-Clause
//

pub mod channels {
use sel4_microkit::Channel;

pub const TIMER_DRIVER: Channel = Channel::new(0);
pub const NET_DRIVER: Channel = Channel::new(1);
pub const BLOCK_DRIVER: Channel = Channel::new(2);
}

pub const VIRTIO_NET_CLIENT_DMA_SIZE: usize = 0x200_000;
pub const VIRTIO_BLK_CLIENT_DMA_SIZE: usize = 0x200_000;
28 changes: 13 additions & 15 deletions crates/examples/microkit/http-server/pds/server/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,19 +29,21 @@ use sel4_async_block_io::{
use sel4_bounce_buffer_allocator::{Basic, BounceBufferAllocator};
use sel4_externally_shared::{ExternallySharedRef, ExternallySharedRefExt};
use sel4_logging::{LevelFilter, Logger, LoggerBuilder};
use sel4_microkit::{memory_region_symbol, protection_domain, var, Channel, Handler};
use sel4_microkit::{memory_region_symbol, protection_domain, Handler};
use sel4_shared_ring_buffer::RingBuffers;
use sel4_shared_ring_buffer_block_io::SharedRingBufferBlockIO;
use sel4_shared_ring_buffer_smoltcp::DeviceImpl;

use microkit_http_server_example_server_core::run_server;

mod block_client;
mod config;
mod handler;
mod net_client;
mod timer_client;

use block_client::BlockClient;
use config::channels;
use handler::HandlerImpl;
use net_client::NetClient;
use timer_client::TimerClient;
Expand All @@ -66,10 +68,6 @@ static LOGGER: Logger = LoggerBuilder::const_default()
.write(|s| sel4::debug_print!("{}", s))
.build();

const TIMER_DRIVER: Channel = Channel::new(0);
const NET_DRIVER: Channel = Channel::new(1);
const BLOCK_DRIVER: Channel = Channel::new(2);

#[protection_domain(
heap_size = 16 * 1024 * 1024,
)]
Expand All @@ -78,17 +76,17 @@ fn init() -> impl Handler {

setup_newlib();

let timer_client = TimerClient::new(TIMER_DRIVER);
let net_client = NetClient::new(NET_DRIVER);
let block_client = BlockClient::new(BLOCK_DRIVER);
let timer_client = TimerClient::new(channels::TIMER_DRIVER);
let net_client = NetClient::new(channels::NET_DRIVER);
let block_client = BlockClient::new(channels::BLOCK_DRIVER);

let notify_net: fn() = || NET_DRIVER.notify();
let notify_block: fn() = || BLOCK_DRIVER.notify();
let notify_net: fn() = || channels::NET_DRIVER.notify();
let notify_block: fn() = || channels::BLOCK_DRIVER.notify();

let net_device = {
let dma_region = unsafe {
ExternallySharedRef::<'static, _>::new(
memory_region_symbol!(virtio_net_client_dma_vaddr: *mut [u8], n = *var!(virtio_net_client_dma_size: usize = 0)),
memory_region_symbol!(virtio_net_client_dma_vaddr: *mut [u8], n = config::VIRTIO_NET_CLIENT_DMA_SIZE),
)
};

Expand Down Expand Up @@ -137,7 +135,7 @@ fn init() -> impl Handler {
let shared_block_io = {
let dma_region = unsafe {
ExternallySharedRef::<'static, _>::new(
memory_region_symbol!(virtio_blk_client_dma_vaddr: *mut [u8], n = *var!(virtio_blk_client_dma_size: usize = 0)),
memory_region_symbol!(virtio_blk_client_dma_vaddr: *mut [u8], n = config::VIRTIO_BLK_CLIENT_DMA_SIZE),
)
};

Expand All @@ -158,9 +156,9 @@ fn init() -> impl Handler {
};

HandlerImpl::new(
TIMER_DRIVER,
NET_DRIVER,
BLOCK_DRIVER,
channels::TIMER_DRIVER,
channels::NET_DRIVER,
channels::BLOCK_DRIVER,
timer_client,
net_device,
net_config,
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
//
// Copyright 2023, Colias Group, LLC
//
// SPDX-License-Identifier: BSD-2-Clause
//

pub mod channels {
use sel4_microkit::Channel;

pub const DEVICE: Channel = Channel::new(0);
pub const CLIENT: Channel = Channel::new(1);
}

pub const FREQ: u64 = 1_000_000;
Original file line number Diff line number Diff line change
Expand Up @@ -10,21 +10,22 @@

use core::time::Duration;

use sel4_microkit::{memory_region_symbol, protection_domain, var, Channel, Handler, MessageInfo};
use sel4_microkit::{memory_region_symbol, protection_domain, Channel, Handler, MessageInfo};
use sel4_microkit_message::MessageInfoExt as _;

use microkit_http_server_example_sp804_driver_core::Driver;
use microkit_http_server_example_sp804_driver_interface_types::*;

const DEVICE: Channel = Channel::new(0);
const CLIENT: Channel = Channel::new(1);
mod config;

use config::channels;

#[protection_domain]
fn init() -> HandlerImpl {
let driver = unsafe {
Driver::new(
memory_region_symbol!(sp804_mmio_vaddr: *mut ()).as_ptr(),
(*var!(freq: usize = 0)).try_into().unwrap(),
config::FREQ,
)
};
HandlerImpl { driver }
Expand All @@ -39,10 +40,10 @@ impl Handler for HandlerImpl {

fn notified(&mut self, channel: Channel) -> Result<(), Self::Error> {
match channel {
DEVICE => {
channels::DEVICE => {
self.driver.handle_interrupt();
DEVICE.irq_ack().unwrap();
CLIENT.notify();
channels::DEVICE.irq_ack().unwrap();
channels::CLIENT.notify();
}
_ => {
unreachable!()
Expand All @@ -57,7 +58,7 @@ impl Handler for HandlerImpl {
msg_info: MessageInfo,
) -> Result<MessageInfo, Self::Error> {
Ok(match channel {
CLIENT => match msg_info.recv_using_postcard::<Request>() {
channels::CLIENT => match msg_info.recv_using_postcard::<Request>() {
Ok(req) => match req {
Request::Now => {
let now = self.driver.now();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
//
// Copyright 2023, Colias Group, LLC
//
// SPDX-License-Identifier: BSD-2-Clause
//

pub mod channels {
use sel4_microkit::Channel;

pub const DEVICE: Channel = Channel::new(0);
pub const CLIENT: Channel = Channel::new(1);
}

pub const VIRTIO_BLK_MMIO_OFFSET: usize = 0xc00;
pub const VIRTIO_BLK_DRIVER_DMA_SIZE: usize = 0x200_000;
pub const VIRTIO_BLK_CLIENT_DMA_SIZE: usize = 0x200_000;
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,9 @@ use sel4_shared_ring_buffer_block_io_types::{
use microkit_http_server_example_virtio_blk_driver_interface_types::*;
use microkit_http_server_example_virtio_hal_impl::HalImpl;

const DEVICE: Channel = Channel::new(0);
const CLIENT: Channel = Channel::new(1);
mod config;

use config::channels;

// HACK hard-coded in virtio-drivers
const QUEUE_SIZE: usize = 4;
Expand All @@ -45,14 +46,14 @@ const QUEUE_SIZE: usize = 4;
)]
fn init() -> HandlerImpl {
HalImpl::init(
*var!(virtio_blk_driver_dma_size: usize = 0),
config::VIRTIO_BLK_DRIVER_DMA_SIZE,
*var!(virtio_blk_driver_dma_vaddr: usize = 0),
*var!(virtio_blk_driver_dma_paddr: usize = 0),
);

let mut dev = {
let header = NonNull::new(
(*var!(virtio_blk_mmio_vaddr: usize = 0) + *var!(virtio_blk_mmio_offset: usize = 0))
(*var!(virtio_blk_mmio_vaddr: usize = 0) + config::VIRTIO_BLK_MMIO_OFFSET)
as *mut VirtIOHeader,
)
.unwrap();
Expand All @@ -63,11 +64,11 @@ fn init() -> HandlerImpl {

let client_region = unsafe {
ExternallySharedRef::<'static, _>::new(
memory_region_symbol!(virtio_blk_client_dma_vaddr: *mut [u8], n = *var!(virtio_blk_client_dma_size: usize = 0)),
memory_region_symbol!(virtio_blk_client_dma_vaddr: *mut [u8], n = config::VIRTIO_BLK_CLIENT_DMA_SIZE),
)
};

let notify_client: fn() = || CLIENT.notify();
let notify_client: fn() = || channels::CLIENT.notify();

let ring_buffers =
RingBuffers::<'_, Use, fn(), BlockIORequest>::from_ptrs_using_default_initialization_strategy_for_role(
Expand All @@ -77,7 +78,7 @@ fn init() -> HandlerImpl {
);

dev.ack_interrupt();
DEVICE.irq_ack().unwrap();
channels::DEVICE.irq_ack().unwrap();

HandlerImpl {
dev,
Expand Down Expand Up @@ -105,7 +106,7 @@ impl Handler for HandlerImpl {

fn notified(&mut self, channel: Channel) -> Result<(), Self::Error> {
match channel {
DEVICE | CLIENT => {
channels::DEVICE | channels::CLIENT => {
let mut notify = false;

while self.dev.peek_used().is_some() {
Expand Down Expand Up @@ -191,7 +192,7 @@ impl Handler for HandlerImpl {
}

self.dev.ack_interrupt();
DEVICE.irq_ack().unwrap();
channels::DEVICE.irq_ack().unwrap();
}
_ => {
unreachable!()
Expand All @@ -206,7 +207,7 @@ impl Handler for HandlerImpl {
msg_info: MessageInfo,
) -> Result<MessageInfo, Self::Error> {
Ok(match channel {
CLIENT => match msg_info.recv_using_postcard::<Request>() {
channels::CLIENT => match msg_info.recv_using_postcard::<Request>() {
Ok(req) => match req {
Request::GetNumBlocks => {
let num_blocks = self.dev.capacity();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
//
// Copyright 2023, Colias Group, LLC
//
// SPDX-License-Identifier: BSD-2-Clause
//

pub mod channels {
use sel4_microkit::Channel;

pub const DEVICE: Channel = Channel::new(0);
pub const CLIENT: Channel = Channel::new(1);
}

pub const VIRTIO_NET_MMIO_OFFSET: usize = 0xe00;
pub const VIRTIO_NET_DRIVER_DMA_SIZE: usize = 0x200_000;
pub const VIRTIO_NET_CLIENT_DMA_SIZE: usize = 0x200_000;
Loading

0 comments on commit 78a2a98

Please sign in to comment.