Implement Rust MLCore driver and remove C driver.

This change adds the kata-ml-core crate. vc_top is generated
programatically, with the script going to be reviewed next if the format here
looks good. The library replaces the VectorCoreDriver c-code.

Change-Id: Id3f083e2498ea29481db49af5e87d47fe8414a71
GitOrigin-RevId: 40d43b0288e995d215997fc8973e18a41a4d5844
This commit is contained in:
Adam Jesionowski 2021-12-02 21:41:27 +00:00 committed by Sam Leffler
parent a9bdb64616
commit acdd562e40
14 changed files with 415 additions and 188 deletions

View File

@ -2,6 +2,8 @@
members = [ members = [
"kata-ml-coordinator", "kata-ml-coordinator",
"kata-ml-interface",
"kata-ml-core"
] ]
[profile.dev] [profile.dev]

View File

@ -4,13 +4,17 @@ import <SecurityCoordinatorInterface.camkes>;
component MlCoordinator { component MlCoordinator {
provides MlCoordinatorInterface mlcoord; provides MlCoordinatorInterface mlcoord;
provides VectorCoreReturnInterface vctop_return;
consumes Interrupt host_req;
consumes Interrupt finish;
consumes Interrupt instruction_fault;
consumes Interrupt data_fault;
dataport Buf csr;
dataport Buf(0x300000) elf_file; dataport Buf(0x300000) elf_file;
dataport Buf(0x40000) itcm; dataport Buf(0x40000) itcm;
dataport Buf(0x1000000) dtcm; dataport Buf(0x1000000) dtcm;
uses LoggerInterface logger; uses LoggerInterface logger;
uses SecurityCoordinatorInterface security; uses SecurityCoordinatorInterface security;
uses VectorCoreInterface vctop;
} }

View File

@ -8,6 +8,7 @@ edition = "2018"
kata-logger = { path = "../../DebugConsole/kata-logger" } kata-logger = { path = "../../DebugConsole/kata-logger" }
kata-panic = { path = "../../DebugConsole/kata-panic" } kata-panic = { path = "../../DebugConsole/kata-panic" }
kata-ml-interface = { path = "../kata-ml-interface" } kata-ml-interface = { path = "../kata-ml-interface" }
kata-ml-core = { path = "../kata-ml-core" }
log = "0.4" log = "0.4"
xmas-elf = "0.8.0" xmas-elf = "0.8.0"

View File

@ -1,82 +0,0 @@
use core::assert;
use core::slice;
use xmas_elf::program::{SegmentData, Type};
use xmas_elf::ElfFile;
// TODO(jesionowski): Move these constants to an auto-generated file.
const ELF_SIZE: usize = 0x300000;
const ITCM_SIZE: usize = 0x40000;
const ITCM_PADDR: usize = 0x30000000;
const DTCM_SIZE: usize = 0x1000000;
const DTCM_PADDR: usize = 0x34000000;
extern "C" {
static elf_file: *const u32;
}
extern "C" {
static itcm: *mut u32;
}
extern "C" {
static dtcm: *mut u32;
}
pub fn loadelf() -> Result<(), &'static str> {
let elf_slice = unsafe { slice::from_raw_parts(elf_file as *const u8, ELF_SIZE) };
let itcm_slice = unsafe { slice::from_raw_parts_mut(itcm as *mut u8, ITCM_SIZE) };
let dtcm_slice = unsafe { slice::from_raw_parts_mut(dtcm as *mut u8, DTCM_SIZE) };
let elf = ElfFile::new(&elf_slice)?;
for seg in elf.program_iter() {
if seg.get_type()? == Type::Load {
let fsize = seg.file_size() as usize;
let msize = seg.mem_size() as usize;
// TODO(jesionowski): I'm assuming that there will be two segments, each beginning at
// the respective PADDRs. Is that assumption safe or does there need to be more
// complex handling?
if seg.virtual_addr() as usize == ITCM_PADDR {
assert!(
fsize <= ITCM_SIZE,
"Elf's ITCM section is larger than than ITCM_SIZE"
);
// Due to being Load types we are guarunteed SegmentData::Undefined as the
// data type.
if let SegmentData::Undefined(bytes) = seg.get_data(&elf)? {
itcm_slice[..fsize].copy_from_slice(&bytes);
}
} else if seg.virtual_addr() as usize == DTCM_PADDR {
assert!(
msize <= DTCM_SIZE,
"Elf's DTCM section is larger than than DTCM_SIZE"
);
if let SegmentData::Undefined(bytes) = seg.get_data(&elf)? {
dtcm_slice[..fsize].copy_from_slice(&bytes);
}
// Clear NOBITS sections.
dtcm_slice[fsize..msize].fill(0x00);
} else {
assert!(false, "Elf contains LOAD section outside TCM");
}
}
}
Ok(())
}
fn get_dtcm_slice() -> &'static mut [u32] {
unsafe { slice::from_raw_parts_mut(dtcm, DTCM_SIZE / 4) }
}
// TODO(jesionowski): Read these from CSRs when available.
pub fn get_return_code() -> u32 {
const RC_OFFSET: usize = 0x3FFFEE;
get_dtcm_slice()[RC_OFFSET]
}
pub fn get_fault_register() -> u32 {
const FAULT_OFFSET: usize = 0x3FFFEF;
get_dtcm_slice()[FAULT_OFFSET]
}

View File

@ -1,27 +1,45 @@
#![no_std] #![no_std]
// ML Coordinator Design Doc: go/sparrow-ml-doc // ML Coordinator Design Doc: go/sparrow-ml-doc
extern crate kata_panic; extern crate kata_panic;
use core::slice;
use kata_logger::KataLogger; use kata_logger::KataLogger;
use kata_ml_core::MlCore;
use kata_ml_interface::MlCoordinatorInterface; use kata_ml_interface::MlCoordinatorInterface;
use kata_ml_interface::MlCoreInterface;
use log::{error, info, trace}; use log::{error, info, trace};
mod mlcore;
pub struct MLCoordinator { pub struct MLCoordinator {
pub is_loaded: bool, is_loaded: bool,
ml_core: MlCore,
} }
pub static mut ML_COORD: MLCoordinator = MLCoordinator { is_loaded: false }; extern "C" {
static elf_file: *const u8;
}
// TODO(jesionowski): Get the size programatically.
const ELF_SIZE: usize = 0x300000;
pub static mut ML_COORD: MLCoordinator = MLCoordinator {
is_loaded: false,
ml_core: MlCore {},
};
impl MLCoordinator { impl MLCoordinator {
fn init(&mut self) {
self.ml_core.enable_interrupts(true);
}
fn handle_return_interrupt(&self) { fn handle_return_interrupt(&self) {
extern "C" {
fn finish_acknowledge() -> u32;
}
// TODO(hcindyl): check the return code and fault registers, move the result // TODO(hcindyl): check the return code and fault registers, move the result
// from TCM to SRAM, update the input/model, and call mlcoord_execute again. // from TCM to SRAM, update the input/model, and call mlcoord_execute again.
let return_code = mlcore::get_return_code(); let return_code = MlCore::get_return_code();
let fault = mlcore::get_fault_register(); let fault = MlCore::get_fault_register();
if return_code != 0 { if return_code != 0 {
error!( error!(
@ -29,17 +47,18 @@ impl MLCoordinator {
return_code, fault return_code, fault
); );
} }
MlCore::clear_finish();
assert!(unsafe { finish_acknowledge() == 0 });
} }
} }
impl MlCoordinatorInterface for MLCoordinator { impl MlCoordinatorInterface for MLCoordinator {
fn execute(&mut self) { fn execute(&mut self) {
extern "C" {
fn vctop_set_ctrl(ctrl: u32);
}
if !self.is_loaded { if !self.is_loaded {
let res = mlcore::loadelf(); let res = self
.ml_core
.load_elf(unsafe { slice::from_raw_parts(elf_file, ELF_SIZE) });
if let Err(e) = res { if let Err(e) = res {
error!("Load error: {:?}", e); error!("Load error: {:?}", e);
} else { } else {
@ -50,9 +69,7 @@ impl MlCoordinatorInterface for MLCoordinator {
if self.is_loaded { if self.is_loaded {
// Unhalt, start at default PC. // Unhalt, start at default PC.
unsafe { self.ml_core.run();
vctop_set_ctrl(vctop_ctrl(0, 0, 0));
}
} }
} }
} }
@ -66,14 +83,10 @@ pub extern "C" fn pre_init() {
#[no_mangle] #[no_mangle]
pub extern "C" fn mlcoord__init() { pub extern "C" fn mlcoord__init() {
// TODO(sleffler): maybe not needed?
trace!("init"); trace!("init");
unsafe {
ML_COORD.init();
} }
// TODO: Move out of this file into separate (auto-generated?) file.
// TODO: Consider the modular_bitfield crate to represent bitfields.
fn vctop_ctrl(freeze: u32, vc_reset: u32, pc_start: u32) -> u32 {
(pc_start << 2) + ((vc_reset & 1) << 1) + (freeze & 1)
} }
// TODO: Once multiple model support is in start by name. // TODO: Once multiple model support is in start by name.
@ -85,8 +98,37 @@ pub extern "C" fn mlcoord_execute() {
} }
#[no_mangle] #[no_mangle]
pub extern "C" fn vctop_return_update_result() { pub extern "C" fn host_req_handle() {
extern "C" {
fn host_req_acknowledge() -> u32;
}
MlCore::clear_host_req();
assert!(unsafe { host_req_acknowledge() == 0 });
}
#[no_mangle]
pub extern "C" fn finish_handle() {
unsafe { unsafe {
ML_COORD.handle_return_interrupt(); ML_COORD.handle_return_interrupt();
} }
} }
#[no_mangle]
pub extern "C" fn instruction_fault_handle() {
extern "C" {
fn instruction_fault_acknowledge() -> u32;
}
error!("Instruction fault in Vector Core.");
MlCore::clear_instruction_fault();
assert!(unsafe { instruction_fault_acknowledge() == 0 });
}
#[no_mangle]
pub extern "C" fn data_fault_handle() {
extern "C" {
fn data_fault_acknowledge() -> u32;
}
error!("Data fault in Vector Core.");
MlCore::clear_data_fault();
assert!(unsafe { data_fault_acknowledge() == 0 });
}

View File

@ -0,0 +1,11 @@
[package]
name = "kata-ml-core"
version = "0.1.0"
edition = "2018"
[dependencies]
kata-logger = { path = "../../DebugConsole/kata-logger" }
kata-ml-interface = { path = "../kata-ml-interface" }
modular-bitfield = "0.11.2"
log = "0.4"
xmas-elf = "0.8.0"

View File

@ -0,0 +1,133 @@
#![no_std]
// kata-ml-core is the vector core driver. It is responsible for providing
// convenient methods for interacting with the hardware.
mod vc_top;
use core::assert;
use core::slice;
use kata_ml_interface::MlCoreInterface;
use xmas_elf::program::{SegmentData, Type};
use xmas_elf::ElfFile;
// TODO(jesionowski): Move these constants to an auto-generated file.
const ITCM_SIZE: usize = 0x40000;
const ITCM_PADDR: usize = 0x30000000;
const DTCM_SIZE: usize = 0x1000000;
const DTCM_PADDR: usize = 0x34000000;
// TODO(jesionowski): ITCM / DTCM will eventually be merged into a single memory.
extern "C" {
static itcm: *mut u32;
}
extern "C" {
static dtcm: *mut u32;
}
fn get_dtcm_slice() -> &'static mut [u32] {
unsafe { slice::from_raw_parts_mut(dtcm, DTCM_SIZE / 4) }
}
pub struct MlCore {}
impl MlCoreInterface for MlCore {
fn enable_interrupts(&mut self, enable: bool) {
let intr_enable = vc_top::IntrEnable::new()
.with_host_req(enable)
.with_finish(enable)
.with_instruction_fault(enable)
.with_data_fault(enable);
vc_top::set_intr_enable(intr_enable);
}
// TODO(jesionowski): Implement using hardware clear CSRs.
fn clear_tcm(&mut self, _start: *const u32, _len: usize) {}
fn run(&mut self) {
let ctrl = vc_top::Ctrl::new()
.with_freeze(false)
.with_vc_reset(false)
.with_pc_start(0);
vc_top::set_ctrl(ctrl);
}
fn load_elf(&mut self, elf_slice: &[u8]) -> Result<(), &'static str> {
let itcm_slice = unsafe { slice::from_raw_parts_mut(itcm as *mut u8, ITCM_SIZE) };
let dtcm_slice = unsafe { slice::from_raw_parts_mut(dtcm as *mut u8, DTCM_SIZE) };
let elf = ElfFile::new(elf_slice)?;
for seg in elf.program_iter() {
if seg.get_type()? == Type::Load {
let fsize = seg.file_size() as usize;
let msize = seg.mem_size() as usize;
if seg.virtual_addr() as usize == ITCM_PADDR {
assert!(
fsize <= ITCM_SIZE,
"Elf's ITCM section is larger than than ITCM_SIZE"
);
// Due to being Load types we are guarunteed SegmentData::Undefined as the
// data type.
if let SegmentData::Undefined(bytes) = seg.get_data(&elf)? {
itcm_slice[..fsize].copy_from_slice(&bytes);
}
} else if seg.virtual_addr() as usize == DTCM_PADDR {
assert!(
msize <= DTCM_SIZE,
"Elf's DTCM section is larger than than DTCM_SIZE"
);
if let SegmentData::Undefined(bytes) = seg.get_data(&elf)? {
dtcm_slice[..fsize].copy_from_slice(&bytes);
}
// TODO(jesionowski): Use clear_tcm instead.
// Clear NOBITS sections.
dtcm_slice[fsize..msize].fill(0x00);
} else {
assert!(false, "Elf contains LOAD section outside TCM");
}
}
}
Ok(())
}
// TODO(jesionowski): Read these from CSRs when available.
fn get_return_code() -> u32 {
const RC_OFFSET: usize = 0x3FFFEE;
get_dtcm_slice()[RC_OFFSET]
}
fn get_fault_register() -> u32 {
const FAULT_OFFSET: usize = 0x3FFFEF;
get_dtcm_slice()[FAULT_OFFSET]
}
// Interrupts are write 1 to clear.
fn clear_host_req() {
let mut intr_state = vc_top::get_intr_state();
intr_state.set_host_req(true);
vc_top::set_intr_state(intr_state);
}
fn clear_finish() {
let mut intr_state = vc_top::get_intr_state();
intr_state.set_finish(true);
vc_top::set_intr_state(intr_state);
}
fn clear_instruction_fault() {
let mut intr_state = vc_top::get_intr_state();
intr_state.set_instruction_fault(true);
vc_top::set_intr_state(intr_state);
}
fn clear_data_fault() {
let mut intr_state = vc_top::get_intr_state();
intr_state.set_data_fault(true);
vc_top::set_intr_state(intr_state);
}
}

View File

@ -0,0 +1,179 @@
// Auto-generated hardware structs from vc_top.hjson
#![allow(unused)]
use modular_bitfield::prelude::*;
#[bitfield]
pub struct IntrState {
pub host_req: bool,
pub finish: bool,
pub instruction_fault: bool,
pub data_fault: bool,
#[skip]
_unused: B28,
}
#[bitfield]
pub struct IntrEnable {
pub host_req: bool,
pub finish: bool,
pub instruction_fault: bool,
pub data_fault: bool,
#[skip]
_unused: B28,
}
#[bitfield]
pub struct IntrTest {
pub host_req: bool,
pub finish: bool,
pub instruction_fault: bool,
pub data_fault: bool,
#[skip]
_unused: B28,
}
#[bitfield]
pub struct Ctrl {
pub freeze: bool,
pub vc_reset: bool,
pub pc_start: B17,
#[skip]
pub _unused0: B13,
}
#[bitfield]
pub struct MemoryBankCtrl {
pub i_mem_enable: B4,
pub d_mem_enable: B8,
#[skip]
pub _unused0: B20,
}
#[bitfield]
pub struct ErrorStatus {
pub i_mem_out_of_range: bool,
pub d_mem_out_of_range: bool,
pub i_mem_disable_access: B4,
pub d_mem_disable_access: B8,
#[skip]
pub _unused0: B18,
}
#[bitfield]
pub struct InitStart {
pub address: B22,
pub imem_dmem_sel: bool,
#[skip]
pub _unused0: B9,
}
#[bitfield]
pub struct InitEnd {
pub address: B22,
pub valid: bool,
#[skip]
pub _unused0: B9,
}
#[bitfield]
pub struct InitStatus {
pub init_pending: bool,
pub init_done: bool,
#[skip]
pub _unused0: B30,
}
extern "C" {
static csr: *mut [u32; 9];
}
pub fn get_intr_state() -> IntrState {
unsafe { IntrState::from_bytes((*csr)[0].to_ne_bytes()) }
}
pub fn set_intr_state(intr_state: IntrState) {
unsafe {
(*csr)[0] = u32::from_ne_bytes(intr_state.into_bytes());
}
}
pub fn get_intr_enable() -> IntrEnable {
unsafe { IntrEnable::from_bytes((*csr)[1].to_ne_bytes()) }
}
pub fn set_intr_enable(intr_enable: IntrEnable) {
unsafe {
(*csr)[1] = u32::from_ne_bytes(intr_enable.into_bytes());
}
}
pub fn get_intr_test() -> IntrTest {
unsafe { IntrTest::from_bytes((*csr)[2].to_ne_bytes()) }
}
pub fn set_intr_test(intr_test: IntrTest) {
unsafe {
(*csr)[2] = u32::from_ne_bytes(intr_test.into_bytes());
}
}
pub fn get_ctrl() -> Ctrl {
unsafe { Ctrl::from_bytes((*csr)[3].to_ne_bytes()) }
}
pub fn set_ctrl(ctrl: Ctrl) {
unsafe {
(*csr)[3] = u32::from_ne_bytes(ctrl.into_bytes());
}
}
pub fn get_memory_bank_ctrl() -> MemoryBankCtrl {
unsafe { MemoryBankCtrl::from_bytes((*csr)[4].to_ne_bytes()) }
}
pub fn set_memory_bank_ctrl(memory_bank_ctrl: MemoryBankCtrl) {
unsafe {
(*csr)[4] = u32::from_ne_bytes(memory_bank_ctrl.into_bytes());
}
}
pub fn get_error_status() -> ErrorStatus {
unsafe { ErrorStatus::from_bytes((*csr)[5].to_ne_bytes()) }
}
pub fn set_error_status(error_status: ErrorStatus) {
unsafe {
(*csr)[5] = u32::from_ne_bytes(error_status.into_bytes());
}
}
pub fn get_init_start() -> InitStart {
unsafe { InitStart::from_bytes((*csr)[6].to_ne_bytes()) }
}
pub fn set_init_start(init_start: InitStart) {
unsafe {
(*csr)[6] = u32::from_ne_bytes(init_start.into_bytes());
}
}
pub fn get_init_end() -> InitEnd {
unsafe { InitEnd::from_bytes((*csr)[7].to_ne_bytes()) }
}
pub fn set_init_end(init_end: InitEnd) {
unsafe {
(*csr)[7] = u32::from_ne_bytes(init_end.into_bytes());
}
}
pub fn get_init_status() -> InitStatus {
unsafe { InitStatus::from_bytes((*csr)[8].to_ne_bytes()) }
}
pub fn set_init_status(init_status: InitStatus) {
unsafe {
(*csr)[8] = u32::from_ne_bytes(init_status.into_bytes());
}
}

View File

@ -3,3 +3,16 @@
pub trait MlCoordinatorInterface { pub trait MlCoordinatorInterface {
fn execute(&mut self); fn execute(&mut self);
} }
pub trait MlCoreInterface {
fn enable_interrupts(&mut self, enabled: bool);
fn clear_tcm(&mut self, start: *const u32, len: usize);
fn run(&mut self);
fn load_elf(&mut self, elf_slice: &[u8]) -> Result<(), &'static str>;
fn get_return_code() -> u32;
fn get_fault_register() -> u32;
fn clear_host_req();
fn clear_finish();
fn clear_instruction_fault();
fn clear_data_fault();
}

View File

@ -1,11 +0,0 @@
component VectorCoreDriver {
dataport Buf csr;
consumes Interrupt host_req;
consumes Interrupt finish;
consumes Interrupt instruction_fault;
consumes Interrupt data_fault;
provides VectorCoreInterface vctop;
uses VectorCoreReturnInterface vctop_return;
}

View File

@ -1,51 +0,0 @@
#include <camkes.h>
#include <stdint.h>
#include "vc_top/vc_top.h"
#define CSR_OFFSET (void *)csr
#define VCTOP_REG(name) \
*((volatile uint32_t *)(CSR_OFFSET + VC_TOP_##name##_REG_OFFSET))
// CAmkES initialization hook.
//
// Enables Interrupts.
//
void pre_init() {
// Enables interrupts.
VCTOP_REG(INTR_ENABLE) = (BIT(VC_TOP_INTR_COMMON_HOST_REQ_BIT) |
BIT(VC_TOP_INTR_ENABLE_FINISH_BIT) |
BIT(VC_TOP_INTR_COMMON_INSTRUCTION_FAULT_BIT) |
BIT(VC_TOP_INTR_COMMON_DATA_FAULT_BIT));
}
void vctop_set_ctrl(uint32_t ctrl) {
VCTOP_REG(CTRL) = ctrl;
}
void host_req_handle(void) {
// Also need to clear the INTR_STATE (write-1-to-clear).
VCTOP_REG(INTR_STATE) = BIT(VC_TOP_INTR_STATE_HOST_REQ_BIT);
seL4_Assert(host_req_acknowledge() == 0);
}
void finish_handle(void) {
// Read main() return code and machine exception PC.
vctop_return_update_result();
// Also need to clear the INTR_STATE (write-1-to-clear).
VCTOP_REG(INTR_STATE) = BIT(VC_TOP_INTR_STATE_FINISH_BIT);
seL4_Assert(finish_acknowledge() == 0);
}
void instruction_fault_handle(void) {
// Also need to clear the INTR_STATE (write-1-to-clear).
VCTOP_REG(INTR_STATE) = BIT(VC_TOP_INTR_STATE_INSTRUCTION_FAULT_BIT);
seL4_Assert(instruction_fault_acknowledge() == 0);
}
void data_fault_handle(void) {
// Also need to clear the INTR_STATE (write-1-to-clear).
VCTOP_REG(INTR_STATE) = BIT(VC_TOP_INTR_STATE_DATA_FAULT_BIT);
seL4_Assert(data_fault_acknowledge() == 0);
}

View File

@ -1,3 +0,0 @@
procedure VectorCoreInterface {
void set_ctrl(in uint32_t ctrl);
};

View File

@ -1,3 +0,0 @@
procedure VectorCoreReturnInterface {
void update_result();
};

View File

@ -13,15 +13,12 @@
import <std_connector.camkes>; import <std_connector.camkes>;
import <global-connectors.camkes>; import <global-connectors.camkes>;
import "interfaces/VectorCoreInterface.camkes";
import "interfaces/VectorCoreReturnInterface.camkes";
import "components/OpenTitanUARTDriver/OpenTitanUARTDriver.camkes"; import "components/OpenTitanUARTDriver/OpenTitanUARTDriver.camkes";
import "components/DebugConsole/DebugConsole.camkes"; import "components/DebugConsole/DebugConsole.camkes";
import "components/ProcessManager/ProcessManager.camkes"; import "components/ProcessManager/ProcessManager.camkes";
import "components/MlCoordinator/MlCoordinator.camkes"; import "components/MlCoordinator/MlCoordinator.camkes";
import "components/StorageManager/StorageManager.camkes"; import "components/StorageManager/StorageManager.camkes";
import "components/SecurityCoordinator/SecurityCoordinator.camkes"; import "components/SecurityCoordinator/SecurityCoordinator.camkes";
import "components/VectorCoreDriver/VectorCoreDriver.camkes";
component OpenTitanUART { component OpenTitanUART {
hardware; hardware;
@ -52,7 +49,6 @@ component VectorPayload {
assembly { assembly {
composition { composition {
component VectorCoreHw vctop; component VectorCoreHw vctop;
component VectorCoreDriver vc_drv;
component VectorPayload vc_payload; component VectorPayload vc_payload;
component OpenTitanUART uart; component OpenTitanUART uart;
@ -75,19 +71,15 @@ assembly {
to uart_driver.tx_empty); to uart_driver.tx_empty);
// VectorCoreDriver // VectorCoreDriver
connection seL4HardwareMMIO vc_csr(from vc_drv.csr, to vctop.csr); connection seL4HardwareMMIO vc_csr(from ml_coordinator.csr, to vctop.csr);
connection seL4RPCCall ml_coord_to_driver(from ml_coordinator.vctop,
to vc_drv.vctop);
connection seL4RPCCall vc_driver_to_ml_coord(from vc_drv.vctop_return,
to ml_coordinator.vctop_return);
connection seL4HardwareInterrupt vctop_host_req(from vctop.host_req, connection seL4HardwareInterrupt vctop_host_req(from vctop.host_req,
to vc_drv.host_req); to ml_coordinator.host_req);
connection seL4HardwareInterrupt vctop_finish(from vctop.finish, connection seL4HardwareInterrupt vctop_finish(from vctop.finish,
to vc_drv.finish); to ml_coordinator.finish);
connection seL4HardwareInterrupt vctop_instruction_fault(from vctop.instruction_fault, connection seL4HardwareInterrupt vctop_instruction_fault(from vctop.instruction_fault,
to vc_drv.instruction_fault); to ml_coordinator.instruction_fault);
connection seL4HardwareInterrupt vctop_data_fault(from vctop.data_fault, connection seL4HardwareInterrupt vctop_data_fault(from vctop.data_fault,
to vc_drv.data_fault); to ml_coordinator.data_fault);
connection seL4HardwareMMIO vc_itcm(from ml_coordinator.itcm, connection seL4HardwareMMIO vc_itcm(from ml_coordinator.itcm,
to vctop.itcm); to vctop.itcm);
connection seL4HardwareMMIO vc_dtcm(from ml_coordinator.dtcm, connection seL4HardwareMMIO vc_dtcm(from ml_coordinator.dtcm,