Clarity on the CPU resource

[p-linh]

These are some properties that we seemed to have agreed on previously:

1. The physical CPU core is the physical resource
2. The virtual CPU is a timeslice of the scheduler that allows a PD to execute something on a certain core
3. holding a CPU resource means we're allowed to execute on a certain core

For (2), in the VM case in seL4, there is also the concept of a vCPU object, which is the virtualized CPU. I thinking holding a CPU here means we're only allowed to execute on a timeslice that's dependent on the hypervisor PD, and not the kernel PD. How do we want to express this in the model? Something like the VM PD's virtual CPU resource maps back to the hypervisor PD's CPU resource?

For (3), does holding a CPU resource means we'll always be allowed to run on a certain core (as long as we hold it)? Since we seem to generally agree that holding a resource means we can give it away, if we give away a CPU resource, this means we're giving a different PD the ability to always run on that CPU core and, similarly, we are no longer allowed to execute on it?

Side note: we always talked about the TCB when discussing CPU objects, but I'm starting to think they're separate from each other. TCB seems more like an execution context resource we brought up several times.

[sid-agrawal]

VM below is for Virtual Machine and not Virtual Memory.

Thank you for raising these here. We do not have clear answers, yet I will jot down some thoughts and draw parallels with virtual memory wherever possible.

To begin with, let's talk about a regular scenario with our VM.

	Memory	CPU	What should we call it?
Physical Resource	Page of DRAM	Physical CPU	physical CPU
Virtual Resource	Page of Virtual Mem.	Entry in the Scheduler	virtual CPU
Mapping	VA --> PA (in the PTE)	vCPU --> pCPU (load TCB to CPU regs) uKernel does this	NA

Now, let's discuss a regular scenario with VM. The point of view is the VM's PD, which is the only thing CellulOS controls. What happens inside the guest VM is up to the guest kernel.

	Memory	CPU	What should we call it?
Physical Resource	Page of DRAM	Physical CPU	physical CPU
Virtual Resource	Page of Virtual Mem.	Entry in the Scheduler	virtual CPU
Mapping	VA --> PA (in the PTE)	vCPU --> pCPU (load TCB to CPU regs) uKernel does this	NA

The only difference between the second and first scenarios is the TCB's link with the vCPU capability in seL4's terminology. The word vCPU is unfortunate terminology, and I suggest we refrain from using it. The following quote from the seL4-manual is relevant

Hardware virtualization allows a thread to perform instructions and operations
as if running at a higher privilege level. Higher privilege levels typically
have access to additional machine registers and other pieces of state, and a VCPU object is
introduced to act as storage for this state.

So, I would call this seL4's vCPU capability a necessary resource for the PD to run a VM. We can call it a Privileged CPU resource; it is not really about physical CPU or virtual CPU (scheduler entry) but about the ability to access the privileged register state. This should answer one of your questions.

Regarding hold edges, in the case of both a standard process PD and a VM PD, the PD only has a hold edge for a Virtual CPU resource. So, it only can execute; it is up to the scheduler which physical CPU it will map to when it gets scheduled. It is similar to virtual memory; you have a hold edge to a virtual resource with no control over what physical resource it maps to at runtime.

I think that delegation could mean one or more of the following things

• CPU Time: If I am allowed to run a specific time period, I could transfer that to another PD (like Scheduling Context in seL4)
• Execution Control: A PD can give another PD the ability to stop/start its execution (like TCB Start/Stop in seL4)

The fact that there are separate cap types in seL4 makes me feel that these need to be separate resource types in CellulOS, too.

I agree that the TCB is different from the CPU resource. When dividing the CPU resource into time and EC, the TCB is certainly more like EC.

When starting a new PD, we could say something like

• the new PD gets a new EC
• But it shares the CPU time resource.

[p-linh]

Ignoring seL4's vCPU terminology for a moment, in the VM case, I was thinking about a virtualized CPU, where the hypervisor is responsible for scheduling which guest is allowed to run at what time. However, the hypervisor PD itself is also given an entry in the scheduler for the real, physical CPU, and it would only be able to schedule VMs from its own virtual CPU "timeslice".

For instance, I was thinking that if the hypervisor PD is only allowed to run on physical core 1, with low priority, then each guest VM managed by the hypervisor PD can also only run on core 1, and with low priority in the host. However, a certain guest may be configured within the hypervisor's scheduler to run at high priority (w.r.t. to other guests), but in the overall system, it can only still run at low priority.

This is why I thought that there might be one more hop between virtual and physical CPU for the VM case (e.g. guest virt CPU --> hypervisor virt CPU --> physical CPU).

[sid-agrawal]

I think I am a little confused by the terminology.

What is the hypervisor PD in the text above?
Is that the VMM-PD?
Or the seL4 kernel?

[p-linh]

Sorry, I should've been more clear. The VMM-PD that's user-level, not the seL4 kernel.

[sid-agrawal]

Thanks! This will be a good discussion for later today. A few points that comes to mind.

1. The VMM-PD is not doing any scheduling in this case (I think, but I would appreciate it if you could correct me). The sel4 kernel schedules all the TCBs it knows of.
2. It is possible that the VMM-PD runs its own TCB with a lower priority and the VM's TCB at a higher priority, right? (not sure if this is possible).

From a model point of view I agree that there is :

flowchart TD
    vGuest{ vCPU-guest inside the guest OS} -->|managed by guest scheduler| pGuest{Physical CPU inside the guest OS i.e. vCPU/TCB on the host}
    pGuest -->|manaegd by sel4 scheduler| pHost{Actual Phys CPU}

Loading

[p-linh]

1. Yes, the VMM-PD we're using doesn't do any scheduling, but I was wondering whether, in general, VMM's have a separate scheduler for the VMs it manages.

2. It depends on how we've set up the TCB. If we configure the VM TCB off of the VMM-PD's TCB, then it can only run at a priority less than or equal to the VMM-PD. From the manual:

   When a thread modifies a another threads priority (including itself) it must provide a thread capability from which to use the MCP from. Threads can only set priorities and MCPs to be less than or equal to the provided thread’s MCP.

   It would be possible for the VM to run at a priority higher than the VMM if we gave the VMM access to a TCB with higher priority than it (e.g. like the RT's TCB), but do we want to do this?

[p-linh]

From our verbal discussion:

• The difference in configuration between a Process-PD and a VM-PD is the extra privileges in which the VM-PD's virtualized CPU has.
  • We will currently bake this difference into the configuration, however, from the high-level view of the model, we don't express this.
• We currently don't express scheduling priority or time quotas in the model. This has parallels to virtual memory and enforcing a memory quota on certain PDs. Once we figure that out, we can then resolve this.