axel-h · axel-h · Jul 3, 2024 · Jul 5, 2024 · Jul 5, 2024 · Jul 8, 2024
diff --git a/CAVEATS.md b/CAVEATS.md
@@ -17,7 +17,7 @@ architectures is on the roadmap and expected in 2025.
   - Platforms (non-hyp): `sabre` (no FPU), `imx8mm-evk` (with FPU)
   - Platforms (hyp, no FPU): `tk1`, `exynos5`
 - AArch64: Armv8-a with hypervisor extensions only, no SMMU, with fast path
-  - Platforms: `tx2`
+  - Platforms: `tx2`, `zynqmp`, `bcm2711` (rpi4)
 - RISC-V: 64-bit only, no fast path
   - Platforms: `hifive`
 - x64: without VT-x and VT-d, no fast path

diff --git a/CHANGES.md b/CHANGES.md
@@ -25,8 +25,10 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
 
 ### Changes
 
+* Added `zynqmp` and `rpi4` to the set of verified AArch64 configs.
 
 ### Upgrade Notes
+
 ---
 
 ## 13.0.0 2024-07-01: BREAKING

diff --git a/config.cmake b/config.cmake
@@ -437,13 +437,28 @@ else()
     config_set(KernelEnableBenchmarks ENABLE_BENCHMARKS OFF)
 endif()
 
-# Reflect the existence of kernel Log buffer
+if(KernelBenchmarksTrackKernelEntries OR KernelBenchmarksTrackUtilisation OR KernelDebugBuild)
+    config_set(KernelTrackKernelEntries TRACE_KERNEL_ENTRIES ON)
+else()
+    config_set(KernelTrackKernelEntries TRACE_KERNEL_ENTRIES OFF)
+endif()
+
+# CONFIG_ENABLE_KERNEL_LOG_BUFFER is set automatically if a feature is used that
+# needs the kernel log buffer.
 if(KernelBenchmarksTrackKernelEntries OR KernelBenchmarksTracepoints)
-    config_set(KernelLogBuffer KERNEL_LOG_BUFFER ON)
+    config_set(KernelLogBuffer ENABLE_KERNEL_LOG_BUFFER ON)
 else()
-    config_set(KernelLogBuffer KERNEL_LOG_BUFFER OFF)
+    config_set(KernelLogBuffer ENABLE_KERNEL_LOG_BUFFER OFF)
 endif()
 
+config_string(
+    KernelLogBufferSize KERNEL_LOG_BUFFER_SIZE
+    "Kernel Log Buffer Size."
+    DEFAULT 20
+    DEPENDS "KernelLogBuffer" DEFAULT_DISABLED 0
+    UNQUOTE
+)
+
 config_string(
     KernelMaxNumTracePoints MAX_NUM_TRACE_POINTS
     "Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data, \

diff --git a/configs/AARCH64_bcm2711_verified.cmake b/configs/AARCH64_bcm2711_verified.cmake
@@ -0,0 +1,26 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2022, Proofcraft Pty Ltd
+# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+# If this file is executed then build the kernel.elf and kernel_all_pp.c file
+include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
+cmake_script_build_kernel()
+
+set(KernelPlatform "bcm2711" CACHE STRING "")
+set(KernelSel4Arch "aarch64" CACHE STRING "")
+set(KernelArmHypervisorSupport ON CACHE BOOL "")
+set(KernelVerificationBuild ON CACHE BOOL "")
+set(KernelMaxNumNodes "1" CACHE STRING "")
+set(KernelOptimisation "-O2" CACHE STRING "")
+set(KernelRetypeFanOutLimit "256" CACHE STRING "")
+set(KernelBenchmarks "none" CACHE STRING "")
+set(KernelDangerousCodeInjection OFF CACHE BOOL "")
+set(KernelFastpath ON CACHE BOOL "")
+set(KernelPrinting OFF CACHE BOOL "")
+set(KernelNumDomains 16 CACHE STRING "")
+set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
+set(KernelArmSMMU OFF CACHE BOOL "")
diff --git a/configs/AARCH64_zynqmp_verified.cmake b/configs/AARCH64_zynqmp_verified.cmake
@@ -0,0 +1,26 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2022, Proofcraft Pty Ltd
+# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+# If this file is executed then build the kernel.elf and kernel_all_pp.c file
+include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
+cmake_script_build_kernel()
+
+set(KernelPlatform "zynqmp" CACHE STRING "")
+set(KernelSel4Arch "aarch64" CACHE STRING "")
+set(KernelArmHypervisorSupport ON CACHE BOOL "")
+set(KernelVerificationBuild ON CACHE BOOL "")
+set(KernelMaxNumNodes "1" CACHE STRING "")
+set(KernelOptimisation "-O2" CACHE STRING "")
+set(KernelRetypeFanOutLimit "256" CACHE STRING "")
+set(KernelBenchmarks "none" CACHE STRING "")
+set(KernelDangerousCodeInjection OFF CACHE BOOL "")
+set(KernelFastpath ON CACHE BOOL "")
+set(KernelPrinting OFF CACHE BOOL "")
+set(KernelNumDomains 16 CACHE STRING "")
+set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
+set(KernelArmSMMU OFF CACHE BOOL "")
diff --git a/include/api/debug.h b/include/api/debug.h
@@ -9,11 +9,11 @@
 #ifdef CONFIG_DEBUG_BUILD
 #pragma once
 
-#include <benchmark/benchmark_track.h>
 #include <arch/api/syscall.h>
 #include <arch/kernel/vspace.h>
 #include <model/statedata.h>
 #include <kernel/thread.h>
+#include <benchmark/benchmark.h>
 
 #ifdef CONFIG_PRINTING
 

diff --git a/include/arch/arm/arch/32/mode/hardware.h b/include/arch/arm/arch/32/mode/hardware.h
@@ -61,7 +61,7 @@
 #define PPTR_BASE seL4_UserTop
 
 /* Calculate virtual address space reserved for dynamic log buffer mapping */
-#ifdef CONFIG_KERNEL_LOG_BUFFER
+#ifdef CONFIG_ENABLE_KERNEL_LOG_BUFFER
 #define PPTR_TOP UL_CONST(0xffe00000)
 #define KS_LOG_PPTR PPTR_TOP
 #else

diff --git a/include/arch/arm/arch/32/mode/model/statedata.h b/include/arch/arm/arch/32/mode/model/statedata.h
@@ -20,9 +20,9 @@ extern hw_asid_t armKSNextASID VISIBLE;
 extern pde_t armKSGlobalPD[BIT(PD_INDEX_BITS)] VISIBLE;
 extern pte_t armKSGlobalPT[BIT(PT_INDEX_BITS)] VISIBLE;
 
-#ifdef CONFIG_KERNEL_LOG_BUFFER
+#ifdef CONFIG_ENABLE_KERNEL_LOG_BUFFER
 extern pte_t armKSGlobalLogPT[BIT(PT_INDEX_BITS)] VISIBLE;
-#endif /* CONFIG_KERNEL_LOG_BUFFER */
+#endif /* CONFIG_ENABLE_KERNEL_LOG_BUFFER */
 
 #else
 extern pdeS1_t armHSGlobalPGD[BIT(PGD_INDEX_BITS)] VISIBLE;

diff --git a/include/arch/arm/arch/64/mode/model/statedata.h b/include/arch/arm/arch/64/mode/model/statedata.h
@@ -38,11 +38,6 @@ extern asid_t armKSHWASIDTable[BIT(hwASIDBits)] VISIBLE;
 extern hw_asid_t armKSNextASID VISIBLE;
 #endif
 
-#ifdef CONFIG_KERNEL_LOG_BUFFER
-extern pte_t *armKSGlobalLogPTE;
-#endif
-
-
 #ifdef CONFIG_ARM_SMMU
 extern bool_t smmuStateSIDTable[SMMU_MAX_SID];
 extern cte_t smmuStateSIDNode[BIT(SMMU_SID_CNODE_SLOT_BITS)];

diff --git a/include/arch/arm/arch/benchmark.h b/include/arch/arm/arch/benchmark.h
@@ -7,8 +7,10 @@
 #pragma once
 
 #include <config.h>
+
 #ifdef CONFIG_ENABLE_BENCHMARKS
 
+#include <types.h>
 #include <armv/benchmark.h>
 #include <mode/machine.h>
 #include <model/statedata.h>
@@ -43,11 +45,13 @@ static inline void handleOverflowIRQ(void)
 }
 #endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
 
+#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 static inline void benchmark_arch_utilisation_reset(void)
 {
 #ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
     ARCH_NODE_STATE(ccnt_num_overflows) = 0;
 #endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
 }
-#endif /* CONFIG_ENABLE_BENCHMARKS */
+#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
 
+#endif /* CONFIG_ENABLE_BENCHMARKS */
diff --git a/include/arch/arm/arch/fastpath/fastpath.h b/include/arch/arm/arch/fastpath/fastpath.h
@@ -8,7 +8,6 @@
 
 #include <linker.h>
 #include <mode/fastpath/fastpath.h>
-#include <benchmark/benchmark_track.h>
 #include <arch/machine/debug.h>
 
 void slowpath(syscall_t syscall)

diff --git a/include/arch/arm/arch/machine.h b/include/arch/arm/arch/machine.h
@@ -42,22 +42,6 @@ void cleanInvalidate_L1D(void);
 void cleanCaches_PoU(void);
 void cleanInvalidateL1Caches(void);
 
-/* Cleaning memory before user-level access */
-static inline void clearMemory(word_t *ptr, word_t bits)
-{
-    memzero(ptr, BIT(bits));
-    cleanCacheRange_RAM((word_t)ptr, (word_t)ptr + BIT(bits) - 1,
-                        addrFromPPtr(ptr));
-}
-
-/* Cleaning memory before page table walker access */
-static inline void clearMemory_PT(word_t *ptr, word_t bits)
-{
-    memzero(ptr, BIT(bits));
-    cleanCacheRange_PoU((word_t)ptr, (word_t)ptr + BIT(bits) - 1,
-                        addrFromPPtr(ptr));
-}
-
 #ifdef ENABLE_SMP_SUPPORT
 static inline void arch_pause(void)
 {

diff --git a/include/arch/arm/armv/armv7-a/armv/benchmark.h b/include/arch/arm/armv/armv7-a/armv/benchmark.h
@@ -6,9 +6,10 @@
 
 #pragma once
 
-#ifdef CONFIG_ENABLE_BENCHMARKS
 #include <config.h>
 
+#ifdef CONFIG_ENABLE_BENCHMARKS
+
 #define PMCR "p15, 0, %0, c9, c12, 0"
 #define PMCNTENSET "p15, 0, %0, c9, c12, 1"
 #define PMOVSR "p15, 0, %0, c9, c12, 3"
@@ -30,4 +31,3 @@ static inline void armv_handleOverflowIRQ(void)
     MCR(PMOVSR, val);
 }
 #endif /* CONFIG_ENABLE_BENCHMARKS */
-
diff --git a/include/arch/arm/armv/armv8-a/64/armv/benchmark.h b/include/arch/arm/armv/armv8-a/64/armv/benchmark.h
@@ -7,6 +7,7 @@
 #pragma once
 
 #include <config.h>
+
 #ifdef CONFIG_ENABLE_BENCHMARKS
 
 #define CCNT "PMCCNTR_EL0"
@@ -31,4 +32,3 @@ static inline void armv_handleOverflowIRQ(void)
 }
 
 #endif /* CONFIG_ENABLE_BENCHMARKS */
-
diff --git a/include/arch/riscv/arch/32/mode/hardware.h b/include/arch/riscv/arch/32/mode/hardware.h
@@ -38,7 +38,7 @@
 #define PPTR_BASE seL4_UserTop
 
 /* Top of the physical memory window */
-#ifdef CONFIG_KERNEL_LOG_BUFFER
+#ifdef CONFIG_ENABLE_KERNEL_LOG_BUFFER
 #define PPTR_TOP UL_CONST(0xFF400000)
 /* Place the kernel log buffer after the PPTR region */
 #define KS_LOG_PPTR PPTR_TOP

diff --git a/include/arch/riscv/arch/benchmark.h b/include/arch/riscv/arch/benchmark.h
@@ -8,19 +8,23 @@
 #pragma once
 
 #include <config.h>
+
+#ifdef CONFIG_ENABLE_BENCHMARKS
+
+#include <types.h>
 #include <arch/object/structures.h>
 #include <mode/hardware.h>
 
-#ifdef CONFIG_ENABLE_BENCHMARKS
 static inline timestamp_t timestamp(void)
 {
     return riscv_read_cycle();
 }
 
+#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 static inline void benchmark_arch_utilisation_reset(void)
 {
     /* nothing here */
 }
+#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
 
 #endif /* CONFIG_ENABLE_BENCHMARK */
-
diff --git a/include/arch/riscv/arch/machine.h b/include/arch/riscv/arch/machine.h
@@ -146,12 +146,6 @@ static inline void hwASIDFlush(asid_t asid)
 word_t PURE getRestartPC(tcb_t *thread);
 void setNextPC(tcb_t *thread, word_t v);
 
-/* Cleaning memory before user-level access */
-static inline void clearMemory(void *ptr, unsigned int bits)
-{
-    memzero(ptr, BIT(bits));
-}
-
 static inline void write_satp(word_t value)
 {
     asm volatile("csrw satp, %0" :: "rK"(value));

diff --git a/include/arch/riscv/arch/model/statedata.h b/include/arch/riscv/arch/model/statedata.h
@@ -32,7 +32,7 @@ extern pte_t kernel_root_pageTable[BIT(PT_INDEX_BITS)] VISIBLE;
 #if __riscv_xlen != 32
 extern pte_t kernel_image_level2_pt[BIT(PT_INDEX_BITS)];
 extern pte_t kernel_image_level2_dev_pt[BIT(PT_INDEX_BITS)];
-#elif defined(CONFIG_KERNEL_LOG_BUFFER)
+#elif defined(CONFIG_ENABLE_KERNEL_LOG_BUFFER)
 extern pte_t kernel_image_level2_log_buffer_pt[BIT(PT_INDEX_BITS)];
 #endif
 
diff --git a/include/arch/x86/arch/32/mode/fastpath/fastpath.h b/include/arch/x86/arch/32/mode/fastpath/fastpath.h
@@ -12,7 +12,7 @@
 #include <arch/machine/debug.h>
 #include <api/types.h>
 #include <api/syscall.h>
-#include <benchmark/benchmark_track.h>
+#include <benchmark/benchmark.h>
 #include <mode/stack.h>
 #include <arch/kernel/tlb_bitmap.h>
 

diff --git a/include/arch/x86/arch/32/mode/model/statedata.h b/include/arch/x86/arch/32/mode/model/statedata.h
@@ -15,9 +15,9 @@
 extern pde_t ia32KSGlobalPD[BIT(PD_INDEX_BITS)];
 extern pte_t ia32KSGlobalPT[BIT(PT_INDEX_BITS)];
 
-#ifdef CONFIG_KERNEL_LOG_BUFFER
+#ifdef CONFIG_ENABLE_KERNEL_LOG_BUFFER
 extern pte_t ia32KSGlobalLogPT[BIT(PT_INDEX_BITS)];
-#endif /* CONFIG_KERNEL_LOG_BUFFER */
+#endif /* CONFIG_ENABLE_KERNEL_LOG_BUFFER */
 
 NODE_STATE_BEGIN(modeNodeState)
 /* Current active page directory. This is really just a shadow of CR3 */

diff --git a/include/arch/x86/arch/benchmark.h b/include/arch/x86/arch/benchmark.h
@@ -7,8 +7,11 @@
 #pragma once
 
 #include <config.h>
+
 #ifdef CONFIG_ENABLE_BENCHMARKS
 
+#include <types.h>
+
 static inline uint64_t timestamp(void)
 {
     uint32_t low, high;
@@ -31,9 +34,11 @@ static inline uint64_t timestamp(void)
     return ((uint64_t) high) << 32llu | (uint64_t) low;
 }
 
+#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 static inline void benchmark_arch_utilisation_reset(void)
 {
+    /* nothing here */
 }
+#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
 
 #endif /* CONFIG_ENABLE_BENCHMARKS */
-
diff --git a/include/arch/x86/arch/machine.h b/include/arch/x86/arch/machine.h
@@ -339,13 +339,6 @@ static inline void x86_load_fsgs_base(tcb_t *thread, cpu_id_t cpu)
     x86_write_gs_base(gs_base, cpu);
 }
 
-/* Cleaning memory before user-level access */
-static inline void clearMemory(void *ptr, unsigned int bits)
-{
-    memzero(ptr, BIT(bits));
-    /* no cleaning of caches necessary on IA-32 */
-}
-
 /* Initialises MSRs required to setup sysenter and sysexit */
 void init_sysenter_msrs(void);