Skip to content

Commit

Permalink
Change how channels described
Browse files Browse the repository at this point in the history 
Before this patch, being able to PPC to a channel depends on whether
or not the receiver of the PPC has 'pp="true"' in the SDF for its
protection domain.

This was finicky and easy to make mistakes with. In addition, it was
not granular enough to allow for actually checking an important
restriction Microkit places on the system architecture which is that
PPC is only allowed to PDs that have a strictly higher priority than
the invoker.

This allows for unidirectional channels as well.

Signed-off-by: julia <[email protected]>
Signed-off-by: Ivan-Velickovic <[email protected]>
  • Loading branch information
@midnightveil @Ivan-Velickovic
midnightveil authored and Ivan-Velickovic committed Oct 22, 2024
1 parent f03340a commit 6952a46
Show file tree
Hide file tree
Showing 9 changed files with 293 additions and 172 deletions.
3 changes: 3 additions & 0 deletions docs/manual.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -732,6 +732,9 @@ The `end` element has the following attributes:

* `pd`: Name of the protection domain for this end.
* `id`: Channel identifier in the context of the named protection domain. Must be at least 0 and less than 63.
* `pp`: (optional) Indicates that the protection domain for this end can perform a protected procedure call to the other end; defaults to false.
Protected procedure calls can only be to PDs of strictly higher priority.
* `notify`: (optional) Indicates that the protection domain for this end can send a notification to the other end; defaults to true.

The `id` is passed to the PD in the `notified` and `protected` entry points.
The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functions.
Expand Down
141 changes: 58 additions & 83 deletions tool/microkit/src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1569,8 +1569,9 @@ fn build_system(
let pd_endpoint_names: Vec<String> = system
.protection_domains
.iter()
.filter(|pd| pd.needs_ep())
.map(|pd| format!("EP: PD={}", pd.name))
.enumerate()
.filter(|(idx, pd)| pd.needs_ep(*idx, &system.channels))
.map(|(_, pd)| format!("EP: PD={}", pd.name))
.collect();
let endpoint_names = [vec![format!("EP: Monitor Fault")], pd_endpoint_names].concat();
// Reply objects
Expand All @@ -1593,8 +1594,9 @@ fn build_system(
system
.protection_domains
.iter()
.map(|pd| {
if pd.needs_ep() {
.enumerate()
.map(|(idx, pd)| {
if pd.needs_ep(idx, &system.channels) {
let obj = &endpoint_objs[1..][i];
i += 1;
Some(obj)
Expand Down Expand Up @@ -2157,7 +2159,7 @@ fn build_system(

// Minting in the address space
for (idx, pd) in system.protection_domains.iter().enumerate() {
let obj = if pd.needs_ep() {
let obj = if pd.needs_ep(idx, &system.channels) {
pd_endpoint_objs[idx].unwrap()
} else {
&notification_objs[idx]
Expand Down Expand Up @@ -2344,89 +2346,62 @@ fn build_system(
}

for cc in &system.channels {
let pd_a = &system.protection_domains[cc.pd_a];
let pd_b = &system.protection_domains[cc.pd_b];
let pd_a_cnode_obj = cnode_objs_by_pd[pd_a];
let pd_b_cnode_obj = cnode_objs_by_pd[pd_b];
let pd_a_notification_obj = &notification_objs[cc.pd_a];
let pd_b_notification_obj = &notification_objs[cc.pd_b];

// Set up the notification caps
let pd_a_cap_idx = BASE_OUTPUT_NOTIFICATION_CAP + cc.id_a;
let pd_a_badge = 1 << cc.id_b;
assert!(pd_a_cap_idx < PD_CAP_SIZE);
system_invocations.push(Invocation::new(
config,
InvocationArgs::CnodeMint {
cnode: pd_a_cnode_obj.cap_addr,
dest_index: pd_a_cap_idx,
dest_depth: PD_CAP_BITS,
src_root: root_cnode_cap,
src_obj: pd_b_notification_obj.cap_addr,
src_depth: config.cap_address_bits,
rights: Rights::All as u64, // FIXME: Check rights
badge: pd_a_badge,
},
));
for (send, recv) in [(&cc.end_a, &cc.end_b), (&cc.end_b, &cc.end_a)] {
let send_pd = &system.protection_domains[send.pd];
let recv_pd = &system.protection_domains[recv.pd];
let send_cnode_obj = cnode_objs_by_pd[send_pd];
let recv_notification_obj = &notification_objs[recv.pd];

if send.can_notify_other {
let send_cap_idx = BASE_OUTPUT_NOTIFICATION_CAP + send.id;
assert!(send_cap_idx < PD_CAP_SIZE);
// receiver sees the sender's badge.
let send_badge = 1 << recv.id;

let pd_b_cap_idx = BASE_OUTPUT_NOTIFICATION_CAP + cc.id_b;
let pd_b_badge = 1 << cc.id_a;
assert!(pd_b_cap_idx < PD_CAP_SIZE);
system_invocations.push(Invocation::new(
config,
InvocationArgs::CnodeMint {
cnode: pd_b_cnode_obj.cap_addr,
dest_index: pd_b_cap_idx,
dest_depth: PD_CAP_BITS,
src_root: root_cnode_cap,
src_obj: pd_a_notification_obj.cap_addr,
src_depth: config.cap_address_bits,
rights: Rights::All as u64, // FIXME: Check rights
badge: pd_b_badge,
},
));
system_invocations.push(Invocation::new(
config,
InvocationArgs::CnodeMint {
cnode: send_cnode_obj.cap_addr,
dest_index: send_cap_idx,
dest_depth: PD_CAP_BITS,
src_root: root_cnode_cap,
src_obj: recv_notification_obj.cap_addr,
src_depth: config.cap_address_bits,
rights: Rights::All as u64, // FIXME: Check rights
badge: send_badge,
},
));
}

// Set up the endpoint caps
if pd_b.pp {
let pd_a_cap_idx = BASE_OUTPUT_ENDPOINT_CAP + cc.id_a;
let pd_a_badge = PPC_BADGE | cc.id_b;
let pd_b_endpoint_obj = pd_endpoint_objs[cc.pd_b].unwrap();
assert!(pd_a_cap_idx < PD_CAP_SIZE);
if send.can_ppcall_other {
let send_cap_idx = BASE_OUTPUT_ENDPOINT_CAP + send.id;
assert!(send_cap_idx < PD_CAP_SIZE);
// receiver sees the sender's badge.
let send_badge = PPC_BADGE | recv.id;

system_invocations.push(Invocation::new(
config,
InvocationArgs::CnodeMint {
cnode: pd_a_cnode_obj.cap_addr,
dest_index: pd_a_cap_idx,
dest_depth: PD_CAP_BITS,
src_root: root_cnode_cap,
src_obj: pd_b_endpoint_obj.cap_addr,
src_depth: config.cap_address_bits,
rights: Rights::All as u64, // FIXME: Check rights
badge: pd_a_badge,
},
));
}
let recv_endpoint_obj =
pd_endpoint_objs[recv.pd].expect("endpoint object to exist");

if pd_a.pp {
let pd_b_cap_idx = BASE_OUTPUT_ENDPOINT_CAP + cc.id_b;
let pd_b_badge = PPC_BADGE | cc.id_a;
let pd_a_endpoint_obj = pd_endpoint_objs[cc.pd_a].unwrap();
assert!(pd_b_cap_idx < PD_CAP_SIZE);
assert!(
send_pd.priority < recv_pd.priority,
"ppcalls must be to a higher priority PD; you specified from pd {} (priority: {}) to pd {} (priority {})",
send_pd.name, send_pd.priority, recv_pd.name, recv_pd.priority,
);

system_invocations.push(Invocation::new(
config,
InvocationArgs::CnodeMint {
cnode: pd_b_cnode_obj.cap_addr,
dest_index: pd_b_cap_idx,
dest_depth: PD_CAP_BITS,
src_root: root_cnode_cap,
src_obj: pd_a_endpoint_obj.cap_addr,
src_depth: config.cap_address_bits,
rights: Rights::All as u64, // FIXME: Check rights
badge: pd_b_badge,
},
));
system_invocations.push(Invocation::new(
config,
InvocationArgs::CnodeMint {
cnode: send_cnode_obj.cap_addr,
dest_index: send_cap_idx,
dest_depth: PD_CAP_BITS,
src_root: root_cnode_cap,
src_obj: recv_endpoint_obj.cap_addr,
src_depth: config.cap_address_bits,
rights: Rights::All as u64, // FIXME: Check rights
badge: send_badge,
},
));
}
}
}

Expand Down
Loading

0 comments on commit 6952a46

Please sign in to comment.