Can CSpaces Replace Resource Tracking?

[p-linh]

As I'm implementing threads, where we make separate CSpaces for them and copy over caps to the new thread, I'm starting to realize that in CellulOS, all PDs (aside from special ones, like the test PD and RT) only hold endpoints caps (representing resources) in their CSpaces.

If we copy caps to the new CSpace, we're essentially just sharing all resources from one PD to the other, so we don't need to explicitly share a resource through our separate data structure, which also just does the same thing (e.g. mint a new badge, copy the EP to the new CSpace).

In our current resource tracking, we keep track of fields that are already baked into the endpoint badge. Does it seem possible to extract a PD's resources by just walking its CSpace, and reading its badge value (we could make a syscall or something that does this)? Then, we don't need to be redundantly tracking resources separately as well.

[sid-agrawal]

I am open to adding a new syscall to get the endpoint's badge value.

However, before we do this, we need to get answers to the following questions:

1. Ask the sel4 mailing list about the implications of adding this syscall, and can we still call our uKernel seL4 after we do this? They are very particular in making changes to the uKernel and still calling it seL4. Given that we will be making security guarantees weaker, it is a fair thing to ask.

2. Will we still need to track information in the rootTask as we do, or can all of that be pushed to the badge? If the answer to this is we still need to track cap info for the root-task, then this might not be worth doing.

[p-linh]

Moved to a TODO beyond thesis