Skip to content

Commit

Permalink
tool: specify ppcalls on a per-channel basis
Browse files Browse the repository at this point in the history 
Previously, this was done on a per-protection domain basis, which
meant that protection domains were given more rights than was strictly
necessary. This also allows for authors to remove rights for sending
notifications on either end of the channel, and so allows for having
unidirectional notification channels.

This removes the previous `pp="true"` attribute on PDs (the one you
would PPC *into*), replacing it with `pp="true/false" and
`notify="true/false"` on each channel end.

So the following:
```
<protection_domain name="sender" [...] />
<protection_domain name="receiver" pp="true" [...] />
<channel>
  <end id="0" pd="sender"   />
  <end id="0" pd="receiver" />
</channel>
```

Becomes instead:
```
<protection_domain name="sender" [...] />
<protection_domain name="receiver" [...] />
<channel>
  <end id="0" pd="sender" pp="true"  />
  <end id="0" pd="receiver"          />
</channel>
```

Signed-off-by: julia <[email protected]>
  • Loading branch information
@midnightveil
midnightveil committed Sep 5, 2024
1 parent a9f6537 commit 2edb5c3
Show file tree
Hide file tree
Showing 10 changed files with 319 additions and 172 deletions.
4 changes: 3 additions & 1 deletion docs/manual.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -638,7 +638,6 @@ The `protection_domain` element describes a protection domain.
It supports the following attributes:

* `name`: A unique name for the protection domain
* `pp`: (optional) Indicates that the protection domain has a protected procedure; defaults to false.
* `priority`: The priority of the protection domain (integer 0 to 254).
* `budget`: (optional) The PD's budget in microseconds; defaults to 1,000.
* `period`: (optional) The PD's period in microseconds; must not be smaller than the budget; defaults to the budget.
Expand Down Expand Up @@ -732,6 +731,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
134 changes: 51 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,55 @@ 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 send_cnode_obj = cnode_objs_by_pd[send_pd];
let recv_notification_obj = &notification_objs[recv.pd];

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,
},
));
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;

// 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);
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,
},
));
}

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,
},
));
}
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;

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);
let recv_endpoint_obj =
pd_endpoint_objs[recv.pd].expect("endpoint object to exist");

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 2edb5c3

Please sign in to comment.