Repository navigation
Feature request: worker threads in a Protection Domain #614
Description
I have a use case where a Protection Domain performs CPU-intensive data processing and needs to execute work in parallel on multiple CPU cores.
At the moment, the natural way to use multiple cores in Microkit is to split the application into multiple PDs. This works well when the components are logically separate, but is awkward when they are really execution contexts of the same application.
In my case, the processing application contains a scheduler and a fairly large object graph allocated on the heap. Processing objects have internal state and are connected through ordinary pointers. Splitting the workers into separate PDs would require moving most or all of the heap into explicitly shared memory and using a shared-memory-aware allocation scheme, even though there is no desired isolation boundary between the workers.
The seL4 model already naturally supports multiple TCBs sharing the same VSpace and CSpace, which seems like a much better fit for this use case.
I would therefore like to propose optional additional worker threads within a Microkit Protection Domain.
Possible SDF interface
For example:
<protection_domain name="audio_processor" cpu="0" priority="200" budget="1000" period="1000">
<program_image path="audio_processor.elf" />
<thread id="0" cpu="1" entry="worker_entry" stack_size="0x8000" />
<thread id="1" cpu="2" entry="worker_entry" stack_size="0x8000" />
</protection_domain>The exact syntax is of course only a suggestion.
Proposed semantics
The existing PD thread would remain the main thread and retain the current Microkit programming model:
- it runs the normal program/runtime initialisation;
- it executes
init; - it owns the Microkit event loop;
- only this thread executes
notified,protected, andfault.
Additional threads would be worker threads rather than additional Microkit event loops.
Each worker would have:
- its own TCB;
- its own Scheduling Context;
- its own stack;
- its own CPU affinity;
- the same VSpace as the main PD thread;
- the same CSpace as the main PD thread.
This means normal pointers, heap allocations, vtables/trait objects, shared static data, and capabilities can be used directly by all threads without constructing a separate shared-memory object model.
Scheduling parameters such as priority, budget and period could initially be inherited from the parent PD, with only cpu being specified per thread. Per-thread overrides could potentially be added later if useful.
Thread initialisation and startup
Worker threads must not enter the normal program startup path independently.
In particular, global/runtime initialisation and the PD's init function must only execute once on the main thread.
Worker TCBs could therefore be created by the system initializer in a suspended state. Their initial PC would point either to their configured entry point or to a small Microkit thread trampoline.
They should only become runnable after the main PD has completed its initialisation.
There are at least two possible APIs for this:
- automatically resume all worker threads after
initreturns; or - provide the PD with a small API such as:
microkit_thread_start(thread_id);so that the application can explicitly start workers near the end of its initialisation.
I personally prefer explicit startup, as it also permits applications to initialise shared scheduler state before workers become runnable.
A worker entry point could look conceptually like:
void worker_entry(microkit_thread_id id);and should probably be required not to return.
IPC buffers and initial scope
I do not think full IPC support is necessary for an initial implementation.
A useful first version could support worker threads intended primarily for computation and shared-memory synchronisation.
For example, workers could use Notifications to sleep while no work is available and to signal other components after producing output.
Therefore an initial implementation could potentially create worker TCBs without IPC buffers.
Full per-thread IPC could be added later by allocating a separate IPC buffer for each thread and providing appropriate TLS/runtime support.
This would keep the first implementation considerably simpler.
Synchronisation use case
A typical worker loop in my application is conceptually:
loop:
take executable work from shared scheduler
execute available work
if no work remains:
wait for a notification
seL4 Notifications are particularly suitable for this because a notification that arrives before the worker waits remains pending, avoiding the usual lost-wakeup race between checking the work queue and going to sleep.
The notification is only a wake-up hint; the shared scheduler/work queue remains the source of truth, so notification coalescing is not a problem.
Why not model the workers as separate PDs?
Separate PDs introduce an isolation boundary that is not desired for this use case.
To make several worker PDs operate on the same state, an application has to explicitly place essentially its entire mutable object graph/heap into shared memory.
For pointer-heavy or stateful processing applications this is significantly more intrusive than simply having several execution contexts within one address space.
Another possible workaround would be to create dummy PDs and later reconfigure their TCBs to use the CSpace and VSpace of a "master" PD. Apart from being a hack, this requires exposing capabilities that allow runtime CSpace/VSpace reconfiguration and no longer accurately reflects the static system structure described by the SDF. Recently, cap_cspace was removed from capability sharing for this reason.
Representing the threads explicitly in the system description avoids that problem; the authority graph remains static and all threads are explicitly part of the same protection domain.
Fault handling
It would also be useful for worker faults to identify the worker/thread ID.
For example, debug fault reporting could distinguish:
audio_processor (main)
audio_processor.thread[0]
audio_processor.thread[1]
even though all of them belong to the same PD.
Initial feature scope
A minimal version that would already cover my use case could therefore be:
- multiple TCBs belonging to one PD;
- shared CSpace and VSpace;
- separate stacks and Scheduling Contexts;
- per-thread CPU affinity;
- configurable entry point;
- workers initially suspended;
- explicit or automatic start after PD initialisation;
- no additional Microkit event loops;
- no
notified/protecteddispatch on workers; - no worker IPC buffers initially;
- Notification-based wakeup/signalling;
- worker ID available to the entry point and fault reporting.
More complete thread runtime support, TLS, per-thread IPC buffers, and more sophisticated scheduling parameters could be added separately.
Would this fit the intended Microkit model for the "multithreaded applications" case, or is there another preferred way to represent this?
Activity
midnightveil commentedon Sep 29, 2026
Related: #602 .
Microkit is (currently) not intended to run unmodified Linux programs, and the current expectations for this sort of implicit shared memory concurrency is that any memory is explicitly shared. However; you should be able to just add shared memory regions at the right virtual address containing .bss/.data and emulate this, but this is currently not an intended mechanism.
I will note however, that this has been asked a few times and internally we have run into situations where we could have used this feature. At this time we (Trustworthy Systems) do not have plans for this. (or funding!)
If you'd like to try to shepherd this, it might be worth writing up a formal RFC with a design and submitting it for further discussion. You may also wish to join a developer hangout.
I am somewhat undecided about whether this would be a good idea to add.
Indanz commentedon Sep 29, 2026
This is just asking for minimal multithreading support of some kind, not for Linux compatibility. This seems entirely reasonable to me.
If thread local storage is not required, then it's fairly easy to add, as noted the main thing missing is telling the loader that multiple tasks share the same VSpace. Whether to specify threads within an existing PD like proposed here, or let threads be PDs with a property that makes it a thread, I don't know.
For the former, all that's really needed is a config option on a PD to tell how many threads it has, and then let the user launch them manually with a function that takes an entry point and stack pointer + size as arguments. There is no strict requirement to make the endpoint badges different: The fault handler can infer which thread it is either via stack pointer or a thread-specific register. If CSpace is shared, IPC calls will use the same badged endpoint too. Main difficulty of this approach is doing PD operations on all threads instead of just one task, like restarting, suspending and resuming. So all in all my impression is that a more verbose way of specifying threads as special PDs might be easier to fit in the Microkit model.
But any kind of official support adds a long-term maintenance burden beyond the initial development, I'm not sure Microkit is mature and stable enough at this point to extend it with a feature like this. And simple initial support, once it's there, will lead to demand for more features, like TLS and more configuration, making things more complicated and increasing the burden.
joep commentedon Sep 30, 2026
I'm pretty sure this can be done using the same sort of hook mechanism we are already using for GDB support where the capDL spec is modified after it is constructed but before it is written.
In this case, for each worker thread, the hook would:
• add worker TCB and scheduling context
• connect it to the PD (audio_processor in this case)
• provide stack, IPC buffer, wakeup capabilities
The stack and IPC-buffer memory could be declared as ordinary .system memory regions. Microkit then creates their mappings normally, and the hook only needs to find the IPC frame and attach it to the TCB.
The worker's register/configuration fields could then be set (tcb_extra_info)
The main PD could then do something like:
I think some sort of formalized access to the capDL spec for modification should be available to those who want to use it. The maintenance burden for all these sorts of requests, including ours, is reduced to one common one. Developers who want to use it are then free to use it (and share their 'extensions'!)
garlinski commentedon Sep 30, 2026
@joep the extension/hook approach sounds very good to me, and I think it would solve my use case without requiring Microkit itself to commit to a multithreading model and all of the associated long-term semantics. Is the hook mechanism you mentioned for GDB support already available in a form that external users can use today, or would it need to be generalized/exposed first?
joep commentedon Sep 30, 2026
No, it's not. It's a modification/hack to Microkit we made specifically for our purposes. It's fragile and prone to problems because we needed to reverse engineer a lot of internal stuff that the tool does.
We have given some thought to an overall extension interface to Microkit. We think the best approach would be to extend the SDF with namespaces. Illustrative example with threads and gdb extensions:
The tool would process this in the following order:
The namespaces select which extension owns custom fields. The command declarations select the programs implementing them. Their order ensures GDB sees the threads added by the threading extension.
We are willing to do the formal RFP for it but we are pretty overwhelmed at the moment so it would be probably near the end of the year.
gernotheiser commentedon Sep 30, 2026
Some quick comments (and apologies if I overlooked something, given I only had time for a relatively shallow look).
I think there are two separate issues here:
I don't see why we need anything extra for (1), other than maybe better tool support for system configuration. A multicore task is simply a PD per core, all sharing a Vspace and Cspace. Obviously each PD has its own TCB and SC (the latter defining the core to which the PD is bound). Each PD has a channel to each other PD (really means they have a Notification to which the other PDs have send rights with different badges). The PDs should not need protected entry points (that's a server feature). They start up as normal (by the parent invoking init()). They can then coordinate via whatever protocol they like.
The protocol presumably requires that one PD (the leader) at the end of its initialisation sends a protocol-initialisation signal to all the other PDs and waits until they all signal back that they are ready.
For (2) I'm also not sure what else is needed. There is no reason why the init or notified functions in app code need to be short (unlike servers) or in fact ever terminate. So why can't the leader simply kick of the followers by sending a signal and then let them run?