At the moment, the Microkit has two limitations which we will run into at some point:
-
There is a maximum number of PDs
|
// Note that these values are used in the monitor so should also be changed there |
|
// if any of these were to change. |
|
pub const MAX_PDS: usize = 63; |
|
pub const MAX_VMS: usize = 63; |
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:
-
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.
-
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.
At the moment, the Microkit has two limitations which we will run into at some point:
There is a maximum number of PDs
microkit/tool/microkit/src/lib.rs
Lines 26 to 29 in 16f3f58
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:
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.
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.