Untyped Capability Size

seL4 kernel
1

Hi, I’m new to seL4 (and OS development in general) and have been going through the tutorial.

In the second tutorial, untyped, the goal is to retype some initially untyped capabilities. I’m confused about the size of the untyped capabilities and how retyping works.

The tutorial starts off like this:

// list of general seL4 objects
seL4_Word objects[] = {seL4_TCBObject, seL4_EndpointObject,
                         seL4_NotificationObject};
// list of general seL4 object size_bits
seL4_Word sizes[] = {seL4_TCBBits, seL4_EndpointBits, seL4_NotificationBits};

// TODO work out what size object we need to create to be able to create all
// of the objects listed above
seL4_Word untyped_size_bits = 0;

I would expect:
untyped_size_bits = seL4_TCBBits + seL4_EndpointBits + seL4_NotificationBits;

However, the solution suggests:
untyped_size_bits = seL4_TCBBits + 1;

seL4_TCBBits is the largest, which I think is important, but I’m not sure why the solution is correct.

The tutorial then follows:

seL4_CPtr parent_untyped = 0;
seL4_CPtr child_untyped = info->empty.start;

// First, find an untyped big enough to fit all of our objects
for (int i = 0; i < (info->untyped.end - info->untyped.start); i++) {
  if (info->untypedList[i].sizeBits >= untyped_size_bits &&
      !info->untypedList[i].isDevice) {
    parent_untyped = info->untyped.start + i;
    break;
  }
}
// create an untyped big enough to retype all of the above objects from

error =
    seL4_Untyped_Retype(parent_untyped, // the untyped capability to retype
                        seL4_UntypedObject,      // type
                        untyped_size_bits,       // size
                        seL4_CapInitThreadCNode, // root
                        0,                       // node_index
                        0,                       // node_depth
                        child_untyped,           // node_offset
                        1                        // num_caps
    );

I’m trying not to copy-paste the entire tutorial but also provide enough context to convey the problem.

If I understand correctly, this code breaks off a chunk of bytes (size untyped_size_bits) and creates a new untyped capability from it at the child_untyped location.

The next part of the tutorial tasks you with creating child TCB, Endpoint, and Notification objects.
The solution is as follows (without the test cases):

seL4_CPtr child_tcb = child_untyped + 1;
seL4_Untyped_Retype(child_untyped, seL4_TCBObject, 0, seL4_CapInitThreadCNode,
                    0, 0, child_tcb, 1);

seL4_CPtr child_ep = child_tcb + 1;
seL4_Untyped_Retype(child_untyped, seL4_EndpointObject, 0,
                    seL4_CapInitThreadCNode, 0, 0, child_ep, 1);

seL4_CPtr child_ntfn = child_ep + 1;
seL4_Untyped_Retype(child_untyped, seL4_NotificationObject, 0,
                    seL4_CapInitThreadCNode, 0, 0, child_ntfn, 1);

What I don’t understand about this is that it seems to be writing past child_untyped, and so its length seems irrelevant. Does child_tcb = child_untyped + 1 mean that child_tcb is pointing to the capability slot after child_untyped?

I think I am confusing capabilities with the actual memory that the child_untyped capability is referring to.

While writing this, I feel like I’ve completely missed the point of the tutorial. I have a basic understanding of memory and threads, but I’m still in high school and feel like I am in way over my head. Would you suggest that I learn more about OS development and try out seL4 with more experience and some formal CS education?

2

Hello @tsoutsman, welcome! :smiley:

When you call seL4_Untyped_Retype and ask seL4 to create a new untyped, it will calculate the size in bytes like this: 2size_bits.

In other words, untyped_size_bits is the log2 of the size in bytes.

The constants defined in libsel4 for the object sizes are in log2 form. Let’s look at them and calculate what their size is in bytes on the x86_64 platform.

They’re defined here:

Constant Value Size in Bytes (2Value)
seL4_TCBBits 12 4096
seL4_EndpointBits 4 16
seL4_NotificationBits 6 64

If we add up the size in bytes we need, we get 4176 bytes.

So we need our child untyped to be at least 4176 bytes, but we can’t ask for that size, we can only ask for sizes in powers of 2. The closest size we can ask for is 8192 bytes, which is 213, which is equal to 2seL4_TCBBits + 1.

That’s a lot of unused space!

Also, note that when seL4 retypes an object from an untyped it guarantees that the new object is naturally aligned. This means that the location of the new object in memory is divisible by the size of the object.

seL4 will take however many additional bytes is needed to naturally align the new object from the untyped, so if you don’t include that in your size calculation you could wind up short. It doesn’t matter in this case though since there’s so much extra space available.

Yes, exactly.

I think the tutorial does kind of confuse this.

An untyped object is a chunk of physical memory.

When you call seL4_Untyped_Retyped you transform the next available chunk of unused memory inside that Untyped object into a new object (not a capability). In this case, a TCB, Endpoint, and Notification.

In addition to creating the new object, seL4_Untyped_Retype also creates a capability to the new object and puts that in the slot you give it. The new capability isn’t created from untyped memory, it requires that you tell it about an empty slot in an existing CNode.

So, child_tcb, child_ep, and child_ntfn are CPtrs to empty slots in the initial thread’s CNode that will contain the capabilities to the new objects that were created from the untyped.

You end up with a new object and a new capability to that object.

3 Likes
4

That’s a very clear explanation, I think I understand it now. Thank you for taking the time to explain it!

5

You’re very welcome! :smiley:

I’m long out of high school and I still feel like I’m in way over my head, don’t let that stop you!

I don’t have any specific recommendations for learning general OS stuff. You might find the community at forum.osdev.org and wiki.osdev.org useful.

For seL4-specific training, you might be interested in Gernot Heiser’s advanced operating systems course. It has some free information on the website plus some free video lectures on youtube.

If you’d like to learn more about designing operating systems using object capabilities, there are some old audio lectures available for free from an advanced operating systems course by Jonathan Shapiro (Updated link). These were from when he was working on coyotos and focuses on its design.

2 Likes