I'm not sure what "PD" means, I'm assuming from context that you mean "process".
PD just means Protection Domain. So, in the context of seL4 - a cspace.
1.
Is there a way for a PD to look up the badge value of badged EP? I
think
the answer is no, but I thought I would still ask.
By design, there is no way to ask the kernel what the badge value is for a capability.
The creator of the endpoint is assured that this badge value can never be seen or modified by anyone who receives a badged cap to the endpoint. In this way, the creator of the endpoint can use the badge to store secrets, such as permission bits or object type.
2.
Is my idea of using the badge to keep track of the underlying object
on
the right track? Is there a better way of going about doing it?
Yes.
This mechanism allows you to use a single endpoint for multiple purposes, so a server only needs to use one. This is convenient since seL4 does not have a "select" mechanism to wait on multiple endpoints.
You might consider storing an array index instead of a pointer to get more room for other bits you may want to store here. Alternatively, you might use any unused low bits of the pointer (due to object size and alignment) to store the object type.
Agreed.
3.
As a potential solution, I can extend my server to add a new
function,
say GETID, which returns the badge value of a given object(i.e.,
EP). Since
I know that the server always badges the EP with the virtual address
of the
struct, it is a trivial call to implement. But I somehow feel like
this is
not a neat idea, not quite sure why.
I also don't think this is a good idea.
I think this friction may be an indication that a different design might work better.
Can you expand on what motivated you to use multiple threads in a single process to wait on multiple endpoints, instead of just using a single endpoint?
In my setup, the root task implements multiple servers(memory allocator, vspace manager, CPU allocator). Each server is run in a separate thread. So, all the servers share the address space.
Each server thread(which implements only one server) waits on only 1 endpoint. Multiple clients have been handed a separate badged copies of this endpoint during some previous handshake. I wanted to keep 1 EP per service for 2 reasons: - Future-proofing: At some point, I might move servers to separate processes. - To restrict clients. For instance, if I want a client to talk to only the CPU server but not others, it has only the CPU server EP. I realize that this can still be multiplexed with this EP on the server side and the server type can be encoded in the badge too. So this in itself is not a great reason.
-JB _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems