Skip to content

Fix approach used for making PDs passive #535

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
dreamliner787-9 wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Fix approach used for making PDs passive #535

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a6e34f9
tool/elf: decouple program headers from segments
dreamliner787-9 Jun 19, 2026
0c8df63
tool/elf: refactored program headers table mgmt
dreamliner787-9 Jun 19, 2026
c7abd5a
tool/elf: + segment with multiple program headers
dreamliner787-9 Jun 19, 2026
d9b1e0a
Switch rust-sel4 to mainline commit
dreamliner787-9 Jun 22, 2026
a1e7268
Make passive PD in initialiser rather than monitor
dreamliner787-9 Jun 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
93 changes: 62 additions & 31 deletions Cargo.lock
View file
Open in desktop

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

4 changes: 2 additions & 2 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,11 @@ members = [

[workspace.dependencies.sel4-capdl-initializer]
git = "https://github.com/au-ts/rust-sel4"
rev = "33cb132571121a8d846ad3be9066617087ee5c32"
rev = "d20b04cc16f4e5f1018213a3d3e9a45e0352724b"

[workspace.dependencies.sel4-capdl-initializer-types]
git = "https://github.com/au-ts/rust-sel4"
rev = "33cb132571121a8d846ad3be9066617087ee5c32"
rev = "d20b04cc16f4e5f1018213a3d3e9a45e0352724b"

[profile.release.package.microkit-tool]
strip = true
2 changes: 1 addition & 1 deletion libmicrokit/include/microkit.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ typedef unsigned int microkit_child;
typedef unsigned int microkit_ioport;
typedef seL4_MessageInfo_t microkit_msginfo;

#define MONITOR_EP 5
/* Index 5 is unused */

@midnightveil midnightveil Jun 22, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is probably unnecessary given all the other indices that are unused.

@dreamliner787-9 dreamliner787-9 Jun 22, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added that to signal to anyone looking at the code later that the index is free to re-use, since previously it was occupied. But I can remove it

/* Only valid in the 'benchmark' configuration */
#define TCB_CAP 6
/* Only valid when the PD has been configured to make SMC calls */
Expand Down
13 changes: 0 additions & 13 deletions libmicrokit/src/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,18 +200,5 @@ void main(void)
{
run_init_funcs();
init();

/*
* If we are passive, now our initialisation is complete we can
* signal the monitor to unbind our scheduling context and bind
* it to our notification object.
* We delay this signal so we are ready waiting on a recv() syscall
*/
if (microkit_passive) {
microkit_have_signal = seL4_True;
microkit_signal_msg = seL4_MessageInfo_new(0, 0, 0, 0);
microkit_signal_cap = MONITOR_EP;
}

handler_loop();
}
16 changes: 0 additions & 16 deletions monitor/src/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,6 @@
#define REPLY_CAP 2
#define BASE_PD_TCB_CAP 10
#define BASE_VM_TCB_CAP 74
#define BASE_SCHED_CONTEXT_CAP 138
#define BASE_NOTIFICATION_CAP 202

extern seL4_IPCBuffer __sel4_ipc_buffer_obj;
seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj;
Expand Down Expand Up @@ -731,20 +729,6 @@ static void monitor(void)
seL4_Word pd_id = badge - 1;
seL4_Word tcb_cap = BASE_PD_TCB_CAP + pd_id;

if (label == seL4_Fault_NullFault && pd_id < MAX_PDS) {
/* This is a request from our PD to become passive */
err = seL4_SchedContext_Bind(BASE_SCHED_CONTEXT_CAP + pd_id, BASE_NOTIFICATION_CAP + pd_id);
if (err != seL4_NoError) {
puts("MON|ERROR: could not bind scheduling context to notification object\n");
} else {
puts("MON|INFO: PD '");
puts(pd_names[pd_id]);
puts("' is now passive!\n");
}

continue;
}

puts("MON|ERROR: received message ");
puthex32(label);
puts(" badge: ");
Expand Down
Loading
Loading