[patch-axel-37] remove redundant inizialization

include/kernel/boot.h

@@ -98,6 +98,7 @@ create_initial_thread(
 );
 
 void init_core_state(tcb_t *scheduler_action);
+void arch_init_core_state(void);
 
 /* state tracking the memory allocated for root server objects */
 typedef struct {
@@ -138,13 +139,21 @@ static inline BOOT_CODE pptr_t it_alloc_paging(void)
 /* return the amount of paging structures required to cover v_reg */
 word_t arch_get_n_paging(v_region_t it_veg);
 
-#if defined(CONFIG_DEBUG_BUILD) && defined(ENABLE_SMP_SUPPORT) && defined(CONFIG_KERNEL_MCS) && !defined(CONFIG_PLAT_QEMU_ARM_VIRT)
+#if defined(CONFIG_DEBUG_BUILD) && defined(ENABLE_SMP_SUPPORT) && defined(CONFIG_KERNEL_MCS)
 /* Test whether clocks are synchronised across nodes */
 #define ENABLE_SMP_CLOCK_SYNC_TEST_ON_BOOT
 #endif
 
 #ifdef ENABLE_SMP_CLOCK_SYNC_TEST_ON_BOOT
-BOOT_CODE void clock_sync_test(void);
+/* Test whether clocks are synchronised across nodes */
+void clock_sync_test(void);
+void clock_sync_test_evaluation(void);
+#define SMP_CLOCK_SYNC_TEST_UPDATE_TIME() \
+    do { \
+        NODE_STATE(ksCurTime) = getCurrentTime(); \
+        __atomic_thread_fence(__ATOMIC_RELEASE); \
+    } while(0)
 #else
 #define clock_sync_test()
+#define SMP_CLOCK_SYNC_TEST_UPDATE_TIME()   ((void)0)
 #endif

include/model/smp.h

@@ -21,7 +21,16 @@ typedef struct smpStatedata {
 
 extern smpStatedata_t ksSMP[CONFIG_MAX_NUM_NODES];
 
+static bool_t is_valid_core(word_t core) {
+    /* Currently the affinity value in both userland and kernel is a linear core
+     * IDs. The actual mapping is architecture and platform specific. We check
+     * against ksNumCPUs, because this is the number of cores that booted
+     * successfully. This is supposed to be equal to CONFIG_MAX_NUM_NODES, which
+     * is the number of cores the kernel tries to boot.
+     */
+    return (core < ksNumCPUs);
+}
+
 void migrateTCB(tcb_t *tcb, word_t new_core);
 
 #endif /* ENABLE_SMP_SUPPORT */
-

include/model/statedata.h

@@ -92,7 +92,7 @@ NODE_STATE_DECLARE(timestamp_t, benchmark_kernel_number_schedules);
 
 NODE_STATE_END(nodeState);
 
-extern word_t ksNumCPUs;
+extern volatile word_t ksNumCPUs;
 
 #if defined ENABLE_SMP_SUPPORT && defined CONFIG_ARCH_ARM
 #define INT_STATE_ARRAY_SIZE ((CONFIG_MAX_NUM_NODES - 1) * NUM_PPI + maxIRQ + 1)

src/arch/arm/kernel/boot.c

@@ -115,6 +115,11 @@ BOOT_CODE static bool_t arch_init_freemem(p_region_t ui_p_reg,
                         it_v_reg, extra_bi_size_bits);
 }
 
+/* This is called from init_core_state() */
+BOOT_CODE void arch_init_core_state()
+{
+    /* Nothing to be done */
+}
 
 BOOT_CODE static void init_irqs(cap_t root_cnode_cap)
 {
@@ -292,6 +297,8 @@ BOOT_CODE static bool_t try_init_kernel_secondary_core(void)
 
 BOOT_CODE static void release_secondary_cpus(void)
 {
+    SMP_CLOCK_SYNC_TEST_UPDATE_TIME();
+
     /* release the cpus at the same time */
     assert(0 == node_boot_lock); /* Sanity check for a proper lock state. */
     node_boot_lock = 1;
@@ -315,12 +322,14 @@ BOOT_CODE static void release_secondary_cpus(void)
 
     /* Wait until all the secondary cores are done initialising */
     while (ksNumCPUs != CONFIG_MAX_NUM_NODES) {
+        SMP_CLOCK_SYNC_TEST_UPDATE_TIME();
+        /* perform a memory acquire to get new values of ksNumCPUs */
+        __atomic_thread_fence(__ATOMIC_ACQUIRE);
+    }
+
 #ifdef ENABLE_SMP_CLOCK_SYNC_TEST_ON_BOOT
-        NODE_STATE(ksCurTime) = getCurrentTime();
+    clock_sync_test_evaluation();
 #endif
-        /* perform a memory acquire to get new values of ksNumCPUs, release for ksCurTime */
-        __atomic_thread_fence(__ATOMIC_ACQ_REL);
-    }
 }
 #endif /* ENABLE_SMP_SUPPORT */
 

src/arch/riscv/kernel/boot.c

@@ -93,6 +93,12 @@ BOOT_CODE static bool_t arch_init_freemem(region_t ui_reg,
                         it_v_reg, extra_bi_size_bits);
 }
 
+/* This is called from init_core_state() */
+BOOT_CODE void arch_init_core_state()
+{
+    /* Nothing to be done */
+}
+
 BOOT_CODE static void init_irqs(cap_t root_cnode_cap)
 {
     irq_t i;
@@ -169,6 +175,8 @@ BOOT_CODE static bool_t try_init_kernel_secondary_core(word_t hart_id, word_t co
 
 BOOT_CODE static void release_secondary_cores(void)
 {
+    SMP_CLOCK_SYNC_TEST_UPDATE_TIME();
+
     assert(0 == node_boot_lock); /* Sanity check for a proper lock state. */
     node_boot_lock = 1;
     /* At this point in time the primary core (executing this code) already uses
@@ -180,11 +188,14 @@ BOOT_CODE static void release_secondary_cores(void)
     fence_rw_rw();
 
     while (ksNumCPUs != CONFIG_MAX_NUM_NODES) {
+        SMP_CLOCK_SYNC_TEST_UPDATE_TIME();
+        /* perform a memory acquire to get new values of ksNumCPUs */
+        __atomic_thread_fence(__ATOMIC_ACQUIRE);
+    }
+
 #ifdef ENABLE_SMP_CLOCK_SYNC_TEST_ON_BOOT
-        NODE_STATE(ksCurTime) = getCurrentTime();
+    clock_sync_test_evaluation();
 #endif
-        __atomic_thread_fence(__ATOMIC_ACQ_REL);
-    }
 }
 #endif /* ENABLE_SMP_SUPPORT */
 

src/arch/x86/kernel/boot.c

@@ -67,6 +67,13 @@ BOOT_CODE static void init_irqs(cap_t root_cnode_cap)
     write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
 }
 
+/* This is called from init_core_state() */
+BOOT_CODE void arch_init_core_state()
+{
+    ARCH_NODE_STATE(x86KScurInterrupt) = int_invalid;
+    ARCH_NODE_STATE(x86KSPendingInterrupt) = int_invalid;
+}
+
 BOOT_CODE static bool_t arch_init_freemem(p_region_t ui_p_reg,
                                           v_region_t it_v_reg,
                                           mem_p_regs_t *mem_p_regs,

src/arch/x86/kernel/boot_sys.c

@@ -48,13 +48,11 @@ extern char _start[1];
 
 #define HIGHMEM_PADDR 0x100000
 
-BOOT_BSS
-boot_state_t boot_state;
+BOOT_BSS boot_state_t boot_state;
 
 /* global variables (not covered by abstract specification) */
 
-BOOT_BSS
-cmdline_opt_t cmdline_opt;
+BOOT_BSS cmdline_opt_t cmdline_opt;
 
 /* functions not modeled in abstract specification */
 
@@ -704,27 +702,26 @@ BOOT_CODE VISIBLE void boot_sys(
     unsigned long multiboot_magic,
     void *mbi)
 {
-    bool_t result = false;
-
-    if (multiboot_magic == MULTIBOOT_MAGIC) {
-        result = try_boot_sys_mbi1(mbi);
-    } else if (multiboot_magic == MULTIBOOT2_MAGIC) {
-        result = try_boot_sys_mbi2(mbi);
-    } else {
+    switch(multiboot_magic) {
+    case MULTIBOOT_MAGIC:
+        if (!try_boot_sys_mbi1(mbi)) {
+            fail("try_boot_sys_mbi1 failed\n");
+        }
+        break;
+    case MULTIBOOT2_MAGIC:
+        if (!try_boot_sys_mbi2(mbi)) {
+            fail("try_boot_sys_mbi2 failed\n");
+        }
+        break;
+    default:
         printf("Boot loader is not multiboot 1 or 2 compliant %lx\n", multiboot_magic);
+        break;
     }
 
-    if (result) {
-        result = try_boot_sys();
-    }
-
-    if (!result) {
+    if (!try_boot_sys())
         fail("boot_sys failed for some reason :(\n");
     }
 
-    ARCH_NODE_STATE(x86KScurInterrupt) = int_invalid;
-    ARCH_NODE_STATE(x86KSPendingInterrupt) = int_invalid;
-
 #ifdef CONFIG_KERNEL_MCS
     NODE_STATE(ksCurTime) = getCurrentTime();
     NODE_STATE(ksConsumed) = 0;
@@ -733,4 +730,3 @@ BOOT_CODE VISIBLE void boot_sys(
     schedule();
     activateThread();
 }
-

src/arch/x86/kernel/smp_sys.c

@@ -13,24 +13,20 @@
 
 #ifdef ENABLE_SMP_SUPPORT
 
-/* Index of next AP to boot, BSP has index zero */
-BOOT_DATA VISIBLE
-volatile word_t smp_aps_index = 1;
-
 #ifdef CONFIG_USE_LOGICAL_IDS
 BOOT_CODE static void update_logical_id_mappings(void)
 {
-    cpu_mapping.index_to_logical_id[getCurrentCPUIndex()] = apic_get_logical_id();
+    cpu_id_t idx = getCurrentCPUIndex();
+    logical_id_t id = apic_get_logical_id();
 
-    for (int i = 0; i < smp_aps_index; i++) {
-        if (apic_get_cluster(cpu_mapping.index_to_logical_id[getCurrentCPUIndex()]) ==
-            apic_get_cluster(cpu_mapping.index_to_logical_id[i])) {
+    cpu_mapping.index_to_logical_id[idx] = id;
 
-            cpu_mapping.other_indexes_in_cluster[getCurrentCPUIndex()] |= BIT(i);
-            cpu_mapping.other_indexes_in_cluster[i] |= BIT(getCurrentCPUIndex());
+    for (int i = 0; i < ksNumCPUs; i++) {
+        if (id == apic_get_cluster(cpu_mapping.index_to_logical_id[i])) {
+            cpu_mapping.other_indexes_in_cluster[idx] |= BIT(i);
+            cpu_mapping.other_indexes_in_cluster[i] |= BIT(idx);
         }
-    }
-}
+    }}
 #endif /* CONFIG_USE_LOGICAL_IDS */
 
 BOOT_CODE static void start_cpu(cpu_id_t cpu_id, paddr_t boot_fun_paddr)
@@ -52,26 +48,30 @@ BOOT_CODE void start_boot_aps(void)
 #endif /* CONFIG_USE_LOGICAL_IDS */
 
     /* startup APs one at a time as we use shared kernel boot stack */
-    while (smp_aps_index < boot_state.num_cpus) {
-        word_t current_ap_index = smp_aps_index;
+    while (ksNumCPUs < boot_state.num_cpus) {
+        word_t current_ap_index = ksNumCPUs;
+        cpu_id_t id = boot_state.cpus[current_ap_index]
 
         printf("Starting node #%lu with APIC ID %lu \n",
-               current_ap_index, boot_state.cpus[current_ap_index]);
+               current_ap_index, id);
 
         /* update cpu mapping for APs, store APIC ID of the next booting AP
          * as APIC ID are not continoius e.g. 0,2,1,3 for 4 cores with hyperthreading
          * we need to store a mapping to translate the index to real APIC ID */
-        cpu_mapping.index_to_cpu_id[current_ap_index] = boot_state.cpus[current_ap_index];
-        start_cpu(boot_state.cpus[current_ap_index], BOOT_NODE_PADDR);
+        cpu_mapping.index_to_cpu_id[current_ap_index] = id;
+        SMP_CLOCK_SYNC_TEST_UPDATE_TIME();
+        start_cpu(id, BOOT_NODE_PADDR);
 
         /* wait for current AP to boot up */
         while (smp_aps_index == current_ap_index) {
-#ifdef ENABLE_SMP_CLOCK_SYNC_TEST_ON_BOOT
-            NODE_STATE(ksCurTime) = getCurrentTime();
-            __atomic_thread_fence(__ATOMIC_ACQ_REL);
-#endif
+            SMP_CLOCK_SYNC_TEST_UPDATE_TIME();
         }
     }
+
+#ifdef ENABLE_SMP_CLOCK_SYNC_TEST_ON_BOOT
+    clock_sync_test_evaluation();
+#endif
+
 }
 
 BOOT_CODE bool_t copy_boot_code_aps(uint32_t mem_lower)
@@ -105,7 +105,7 @@ static BOOT_CODE bool_t try_boot_node(void)
     setCurrentVSpaceRoot(kpptr_to_paddr(X86_KERNEL_VSPACE_ROOT), 0);
     /* Sync up the compilers view of the world here to force the PD to actually
      * be set *right now* instead of delayed */
-    asm volatile("" ::: "memory");
+    x86_mfence();
 
     /* initialise the CPU, make sure legacy interrupts are disabled */
     if (!init_cpu(1)) {
@@ -123,25 +123,21 @@ static BOOT_CODE bool_t try_boot_node(void)
  * node #0 to possibly reallocate this memory */
 VISIBLE void boot_node(void)
 {
-    bool_t result;
+    mode_init_tls(ksNumCPUs);
 
-    mode_init_tls(smp_aps_index);
-    result = try_boot_node();
-
-    if (!result) {
+    if (!try_boot_node()) {
         fail("boot_node failed for some reason :(\n");
     }
 
     clock_sync_test();
-    smp_aps_index++;
+
+    ksNumCPUs++;
+    __atomic_thread_fence(__ATOMIC_RELEASE);
 
     /* grab BKL before leaving the kernel */
     NODE_LOCK_SYS;
 
     init_core_state(SchedulerAction_ChooseNewThread);
-    ARCH_NODE_STATE(x86KScurInterrupt) = int_invalid;
-    ARCH_NODE_STATE(x86KSPendingInterrupt) = int_invalid;
-
     schedule();
     activateThread();
 }