vm_arm: add pcpu list for core pinning

Add a pcpu list to the VM_Arm component to allow pinning of vcpus to specific physical cpus within a CAmkES configuration. Co-authored-by: Alex Pavey <[email protected]> Signed-off-by: Axel Heider <[email protected]>
seL4 · Jan 29, 2024 · e41635f · e41635f
1 parent 8139a5f
commit e41635f
Show file tree

Hide file tree

Showing 4 changed files with 28 additions and 1 deletion.
diff --git a/components/VM_Arm/configurations/vm.h b/components/VM_Arm/configurations/vm.h
@@ -65,6 +65,7 @@
     provides VMDTBPassthrough dtb; \
     attribute int base_prio; \
     attribute int num_vcpus = 1; \
+    attribute int pcpus[] = []; \
     attribute int num_extra_frame_caps; \
     attribute int extra_frame_map_address; \
     attribute { \

diff --git a/components/VM_Arm/src/main.c b/components/VM_Arm/src/main.c
@@ -1314,9 +1314,14 @@ static int main_continued(void)
 #endif
 
     /* Create CPUs and DTB node */
+    int pcpu_list_size = get_instance_size_pcpus_list();
     for (int i = 0; i < vm_config.num_vcpus; i++) {
         vm_vcpu_t *new_vcpu = create_vmm_plat_vcpu(&vm, VM_PRIO - 1);
         assert(new_vcpu);
+        if (i < pcpu_list_size) {
+            /* Assign VCPU to explicit physical CPU */
+            new_vcpu->target_cpu = pcpus[i];
+        }
     }
     if (vm_config.generate_dtb) {
         err = fdt_generate_plat_vcpu_node(&vm, gen_dtb_buf);
@@ -1332,8 +1337,12 @@ static int main_continued(void)
         return -1;
     }
 
-    err = vm_assign_vcpu_target(vcpu_boot, 0);
+    /* Use affinity as boot core if pcpus are not specified */
+    err = vm_assign_vcpu_target(vcpu_boot,
+                                (0 == pcpu_list_size) ? get_instance_affinity()
+                                : vm_vcpu->target_cpu);
     if (err) {
+        ZF_LOGE("Error: Failed to assign boot vcpu");
         return -1;
     }
 

diff --git a/templates/seL4VMParameters.template.c b/templates/seL4VMParameters.template.c
@@ -131,3 +131,18 @@ const vm_config_t vm_config = {
 /*- endif -*/
 
 };
+
+/*- set pcpu_cnt = 0 -*/
+/*- if 'pcpus' in config.keys() -*/
+    /*- set pcpus = config.get('pcpus') -*/
+    /*- set pcpu_cnt = len(pcpus) -*/
+    /*- for pcpu in pcpus -*/
+#if(/*? pcpu ?*/  >= CONFIG_MAX_NUM_NODES)
+#error "Invalid CPU number /*? pcpu ?*/ in PCPU list"
+#endif
+    /*- endfor -*/
+/*- endif -*/
+
+int get_instance_size_pcpus_list(void) {
+    return /*? pcpu_cnt ?*/;
+}
diff --git a/templates/seL4VMParameters.template.h b/templates/seL4VMParameters.template.h
@@ -47,3 +47,5 @@ typedef struct {
 } vm_config_t;
 
 extern const vm_config_t vm_config;
+
+int get_instance_size_pcpus_list(void);
Original file line number	Diff line number	Diff line change
Expand Up		@@ -47,3 +47,5 @@ typedef struct {
		} vm_config_t;

		extern const vm_config_t vm_config;

		int get_instance_size_pcpus_list(void);