Skip to content

template-pd: introduce 'template' attribute in sdf - #1

Open
ZGwtao wants to merge 3 commits into
mainfrom
template-pd
Open

template-pd: introduce 'template' attribute in sdf#1
ZGwtao wants to merge 3 commits into
mainfrom
template-pd

Conversation

@ZGwtao

@ZGwtao ZGwtao commented Jul 29, 2026

Copy link
Copy Markdown

This commmit allows users to create a type of PD that has no 'program_image'. Such a mechanism is helpful for loading application payloads into a microkit PD dynamically.

The requirements of using a template PD are:

  • template PD should be a child PD of a PD who has no parent
  • template PD should not have children, VMs, program images
  • template PD should always be active (or their parents need to perform SchedContext unbound operations)

Something needs discussing is the PD information generated by microkit (e.g., pd_name, ppc bitmaps), which are not provided to the template PDs, as the template PDs have no program image to patch with.

This issue may affect the payloads that use libmicrokit as their runtime, which checks channel ids using the generated channel bitmaps.

A solution is adding a region to the image of the parent PD, which can and should record the microkit-generated PD information of the template PDs. We can provide an object file that contains a region, and put it in libmicrokit.a. PDs that use the region can conditionally link with the object file when building with libmicrokit. The parent PD can pass the microkit-generated info to the template PDs by patching the payload during late-loading.

Ref:

Redirected from: seL4#582

Comment thread example/empty/loader.c Outdated
Comment thread example/empty/loader.c Outdated
Comment thread example/empty/loader.c Outdated
Comment thread example/empty/loader.c Outdated
Comment thread tool/microkit/src/sdf/pd_vm.rs Outdated
Comment thread tool/microkit/src/sdf/pd_vm.rs Outdated
Comment thread tool/microkit/src/sdf/pd_vm.rs
Comment thread docs/manual.md
Comment thread example/empty/loader.c Outdated
Comment thread example/empty/loader.c Outdated
continue;
}
void *src = (char *)ehdr + phdr[i].p_offset;
void *dest = (void *)(dest_vaddr + phdr[i].p_vaddr - ehdr->e_entry);

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Unless this is a PIE exe you should only be loading an ELF at it's desired virtual address; this also seems to implicitly assume that the entry point is at the start of a PD's address space.

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

bump?

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

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

So instead of forcing the clients to use PIE, I set up a region within the vspace of the template PD. The loadable segements (i.e., segs with PT_LOAD) of a payload should live within the given region. The payload is also required to begins at somewhere within the given region.

@ZGwtao
ZGwtao force-pushed the template-pd branch 2 times, most recently from ee785d1 to f03c1dd Compare July 30, 2026 03:27
@ZGwtao
ZGwtao requested a review from midnightveil July 30, 2026 03:29
Comment thread docs/manual.md
Comment thread docs/manual.md

It also has the same attributes as protection domains but not:

* `setvar_id`: This attribute is valid only when a program image is given.

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

is setvar_id an attribute on the child(?)

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

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

Oh I think I have mistaken the usage of setvar_id, I will fix this

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

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

Now it seems all setvars are disabled for templates. Tests are also provided.

Comment thread tool/microkit/src/sdf/pd_vm.rs
Comment thread example/empty/loader.c Outdated
continue;
}
void *src = (char *)ehdr + phdr[i].p_offset;
void *dest = (void *)(dest_vaddr + phdr[i].p_vaddr - ehdr->e_entry);

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

bump?

ZGwtao added 3 commits July 31, 2026 14:42
This commmit allows users to create a type of PD that has no
'program_image'. Such a mechanism is helpful for loading application
payloads into a microkit PD dynamically.

The requirements of using a template PD are:
- template PD should be a child PD of a PD who has no parent
- template PD should not have children, VMs, program images
- template PD should always be active (or their parents need to perform
  SchedContext unbound operations)

Ref:
- Ch.4., Evolving seL4CP Into a Dynamic OS, Leslie and Heiser, 2022
- https://trustworthy.systems/projects/microkit/2203-report-dynamic.pdf

Signed-off-by: Guangtao Zhu <guangtaozhu@outlook.com>
Signed-off-by: Guangtao Zhu <guangtaozhu@outlook.com>
Setvar and setvars on elements within a template are
all disabled, as they rely on a given program image, which
is not provided when using a template PD.

Signed-off-by: Guangtao Zhu <guangtaozhu@outlook.com>

@midnightveil midnightveil left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Good enough for me :) There's some grammatical issues in some of the text but that's less important. Feel free to merge when desired.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants