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 <[email protected]>

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; \

components/VM_Arm/src/main.c

@@ -76,10 +76,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
@@ -552,7 +550,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);
@@ -1236,7 +1234,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) {
@@ -1294,15 +1292,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) {

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;
 
     }

templates/seL4VMParameters.template.c

@@ -20,6 +20,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 = {

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;