From 99fb5ce23753bd126cd8543375652cdac51cc8fb Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Mon, 20 Mar 2023 17:01:43 +0100 Subject: [PATCH] vm_arm: add priority in vm config struct - Cleanup the definitions. - Set a default base value for the attribute. - Derive the other priorities in the config params template. - Do sanity check during template processing. Signed-off-by: Axel Heider --- components/VM_Arm/configurations/vm.h | 2 +- components/VM_Arm/src/main.c | 11 ++-------- components/VM_Arm/vm_common.camkes | 4 +--- templates/seL4VMParameters.template.c | 31 +++++++++++++++++++++++++++ templates/seL4VMParameters.template.h | 6 ++++++ 5 files changed, 41 insertions(+), 13 deletions(-) diff --git a/components/VM_Arm/configurations/vm.h b/components/VM_Arm/configurations/vm.h index 8e15dec2..1c503945 100644 --- a/components/VM_Arm/configurations/vm.h +++ b/components/VM_Arm/configurations/vm.h @@ -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; \ diff --git a/components/VM_Arm/src/main.c b/components/VM_Arm/src/main.c index cf591e4d..3a35c65b 100644 --- a/components/VM_Arm/src/main.c +++ b/components/VM_Arm/src/main.c @@ -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 @@ -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); @@ -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) { @@ -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) { diff --git a/components/VM_Arm/vm_common.camkes b/components/VM_Arm/vm_common.camkes index 38c102c2..a9580f08 100644 --- a/components/VM_Arm/vm_common.camkes +++ b/components/VM_Arm/vm_common.camkes @@ -30,9 +30,7 @@ assembly { vm.cnode_size_bits = 23; vm.simple_untyped24_pool = 12; - vm.base_prio = 100; - - vm._priority = 101; + vm._priority = 101; /* priority of VM component's main thread */ vm.sem_value = 0; } diff --git a/templates/seL4VMParameters.template.c b/templates/seL4VMParameters.template.c index 7b7ce070..c7087b97 100644 --- a/templates/seL4VMParameters.template.c +++ b/templates/seL4VMParameters.template.c @@ -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 = { diff --git a/templates/seL4VMParameters.template.h b/templates/seL4VMParameters.template.h index ab30b5e6..42411f1b 100644 --- a/templates/seL4VMParameters.template.h +++ b/templates/seL4VMParameters.template.h @@ -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;