Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

vm_arm: add priority in vm config struct #69

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

vm_arm: add priority in vm config struct #69

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion components/VM_Arm/configurations/vm.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@
emits HaveNotification notification_ready_connector; \
maybe uses VMDTBPassthrough dtb_self; \
provides VMDTBPassthrough dtb; \
attribute int base_prio; \
attribute int base_prio = 100; \
attribute int num_vcpus = 1; \
attribute int num_extra_frame_caps; \
attribute int extra_frame_map_address; \
Expand Down
11 changes: 2 additions & 9 deletions components/VM_Arm/src/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,10 +77,8 @@ seL4_CPtr camkes_alloc(seL4_ObjectType type, size_t size, unsigned flags);
extern void *fs_buf;
int start_extra_frame_caps;

int VM_PRIO = 100;
int NUM_VCPUS = 1;

#define IRQSERVER_PRIO (VM_PRIO + 1)
#define IRQ_MESSAGE_LABEL 0xCAFE

#define DMA_VSTART 0x40000000
Expand Down Expand Up @@ -558,7 +556,7 @@ static int vmm_init(const vm_config_t *vm_config)
assert(!err);

/* Create an IRQ server */
_irq_server = irq_server_new(vspace, vka, IRQSERVER_PRIO,
_irq_server = irq_server_new(vspace, vka, vm_config->priority.irqserver,
simple, simple_get_cnode(simple), fault_ep_obj.cptr,
IRQ_MESSAGE_LABEL, 256, &_io_ops.malloc_ops);
assert(_irq_server);
Expand Down Expand Up @@ -1259,7 +1257,7 @@ static int main_continued(void)

/* Create CPUs and DTB node */
for (int i = 0; i < NUM_VCPUS; i++) {
vm_vcpu_t *new_vcpu = create_vmm_plat_vcpu(&vm, VM_PRIO - 1);
vm_vcpu_t *new_vcpu = create_vmm_plat_vcpu(&vm, vm_config.priority.vcpu);
assert(new_vcpu);
}
if (vm_config.generate_dtb) {
Expand Down Expand Up @@ -1317,15 +1315,10 @@ static int main_continued(void)
}

/* base_prio and num_vcpus are optional attributes of the VM component. */
extern const int __attribute__((weak)) base_prio;
extern const int __attribute__((weak)) num_vcpus;

int run(void)
{
/* if the base_prio attribute is set, use it */
if (&base_prio != NULL) {
VM_PRIO = base_prio;
}
/* if the num_vcpus attribute is set, try to use it */
if (&num_vcpus != NULL) {
if (num_vcpus > CONFIG_MAX_NUM_NODES) {
Expand Down
4 changes: 1 addition & 3 deletions components/VM_Arm/vm_common.camkes
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,7 @@ assembly {
vm.cnode_size_bits = 23;
vm.simple_untyped24_pool = 12;

vm.base_prio = 100;

vm._priority = 101;
Copy link
Member

@kent-mcleod kent-mcleod Apr 10, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

_priority has a special meaning as the priority for the thread that calls run

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, worth to add this in a comment. But shouldn't this be 100 then?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the VMM threads aren't a higher priority than the vm thread, the vm won't be preempted when there's work to be done in the VMM which affects things like IRQ latency.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But the "VM Thread" is the vCPU thread, right? This is supposed to run at "basePrio - 1".

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Check for vcpu_prio < base_prio && vcpu_prio < irqserver_prio is missing in that Jinja template. Probably that's what @kent-mcleod meant?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess it could still be up to someone to choose to configure the vmm and vcpu threads with the same priority if they wanted to delay things like IRQ injection until the vcpu thread was preempted or yielded, but in general, it's probably most straight forward if the irq server threads have equal or higher prio to vmm thread, which has higher prio to vcpu threads.

vm._priority = 101; /* priority of VM component's main thread */
vm.sem_value = 0;

}
Expand Down
31 changes: 31 additions & 0 deletions templates/seL4VMParameters.template.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,37 @@

const vm_config_t vm_config = {

.priority = {
/*#
* The CAmkES attribute '_priority' define the control thread's
* priority, which is the thread that does the VMM setup and executes
* the VMM even loop eventually.
* The VMM attribute 'base_prio' defines the priorities to be used
* - interrupt server thread: base_prio + 1
* - vmm thread: base_prio
* - vcpu thread(s): base_prio - 1
* but these can never exceed the component priority. Furthermore these
* constrains apply:
* - the vcpu thread can't have a higher priority than the VMM's event
* loop, otherwise it can't be preempted when an even arrives. It may
* have equal priority, in this case events like IRQ injection get
* delayed until the vcpu thread was preempted or yielded.
* - the VMM thread can have a higher priority than the interrupt
* server thread. They may have equal priority, but this also
* increases e.g. interrupt latency.
#*/
/*- set comp_prio = config.get('_priority') -*/
/*- set base_prio = config.get('base_prio') -*/
/*- set irqserver_prio = min(comp_prio, base_prio + 1) -*/
/*- set vcpu_prio = min(comp_prio, base_prio - 1) -*/
/*- if ((vcpu_prio > base_prio) or (base_prio > irqserver_prio)) -*/
/*? raise(Exception('Invalid priority configuration: vcpu/'+str(vcpu_prio)+' > base/'+str(base_prio)+' > irqserver/'+str(irqserver_prio))) ?*/
/*- endif -*/
.irqserver = /*? irqserver_prio ?*/,
.vmm = /*? base_prio ?*/,
.vcpu = /*? vcpu_prio ?*/,
},

/*- if vm_address_config -*/

.ram = {
Expand Down
6 changes: 6 additions & 0 deletions templates/seL4VMParameters.template.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,12 @@

typedef struct {

struct {
uint8_t vmm;
uint8_t irqserver;
uint8_t vcpu;
} priority;

struct {
uintptr_t phys_base;
uintptr_t base;
Expand Down