Improvements to the 64 (62) client/PD/channel limit

Open
#526 3 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
5/5
Estimated time
Over a week
Newbie friendliness
30/100
Issue type
Feature
Clarity
Needs clarification
Activity status
Quiet
Tech stack
rust

Research direction

Start with tool/microkit/src/lib.rs at the cited PD limit and trace the monitor's PD-name and badge handling. Review the linked sDDF virtualiser pattern for shared notification IDs and client grouping. Done means the Microkit design and implementation support larger PD counts and more flexible client/server channel relationships.

Written by the indexing model from the issue text.

Description

needs-discussion

At the moment, the Microkit has two limitations which we will run into at some point:

  • There is a maximum number of PDs
    https://github.com/seL4/microkit/blob/16f3f5889460aad4e76a9d99708a8926f34fe69c/tool/microkit/src/lib.rs#L26-L29
    This is limited by the fact that the monitor is a default fault endpoint for all PDs.
    It is also limited by the size of the PD names array in the monitor (this can be easily solved).

  • There is a maximum number of channels to each PD
    This is "limited" by the number of bits in an seL4_Word: for asynchronous notifications, reporting the status of 64 channels requires more 64 bits of information: in fact we limit the number of channels to 62, using the badged mechanism to also report "fault" and "PPC" identifiers.

However, whilst this is all true, these limits are not absolute:

  1. A server can easily support more than 64 different PPCs/Faults (endpoints): in seL4, endpoints form a queue.
    Whilst the top 2 bits must be reserved to distinguish fault/PPC/signal, both faults and endpoints then have the remaining 62 bits left: which gives us 2^62 different unique client identifiers, which should be more than enough.
    Part of this would also be reworking so that the "channel" is not a unique namespace between notifications/PPCs.

  2. Currently, client:server notifications have 1:1 channel IDs. That is, one client notification will set one bit in the badge of the server's notification receive, and vice versa.
    This is however, unnecessary: like in real hardware IRQs, seL4 allows multiple notifications to have the same badge, i.e. have the same ID to the server, and be distinguished out of band.
    In the simplest case, this can be done using shared memory by the user, or as is the case for many of our virtualisers in the sDDF, we don't actually need to distinguish between different clients. Alternatively, one can partition clients into "priority" classes or other groupings.

    The server to notify a client will signal a capability: we can easily have more than 64 of one particular capability, we just need to layout the CSpace such that there is one cap.

    For example: consider our network virtualiser. On a notification from a client, we process all client queues. We don't care which client did so: as this gives us the most benefit from batching of packets. To respond to a particular client, we perform a singular notification on the appropriate notification capability, which has no limit.

These two changes would allow for systems with larger number of PDs to be created.

Dominant language
Rust
Stars
201
Forks
80
Avg merge
1d 4h
Merged PRs (30d)
7

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from seL4/microkit

All issues in seL4/microkit

Similar issues

More Rust issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.