Kent/n1

configs/seL4Config.cmake

@@ -147,6 +147,7 @@ foreach(
     KernelArmCortexA55
     KernelArmCortexA57
     KernelArmCortexA72
+    KernelArmNeoverseN1
     KernelArchArmV7a
     KernelArchArmV7ve
     KernelArchArmV8a
@@ -194,6 +195,7 @@ config_set(KernelArmCortexA53 ARM_CORTEX_A53 "${KernelArmCortexA53}")
 config_set(KernelArmCortexA55 ARM_CORTEX_A55 "${KernelArmCortexA55}")
 config_set(KernelArmCortexA57 ARM_CORTEX_A57 "${KernelArmCortexA57}")
 config_set(KernelArmCortexA72 ARM_CORTEX_A72 "${KernelArmCortexA72}")
+config_set(KernelArmNeoverseN1 ARM_NEOVERSE_N1 "${KernelArmNeoverseN1}")
 config_set(KernelArchArmV7a ARCH_ARM_V7A "${KernelArchArmV7a}")
 config_set(KernelArchArmV7ve ARCH_ARM_V7VE "${KernelArchArmV7ve}")
 config_set(KernelArchArmV8a ARCH_ARM_V8A "${KernelArchArmV8a}")
@@ -227,6 +229,8 @@ elseif(KernelArmCortexA57)
     set(KernelArmCPU "cortex-a57" CACHE INTERNAL "")
 elseif(KernelArmCortexA72)
     set(KernelArmCPU "cortex-a72" CACHE INTERNAL "")
+elseif(KernelArmNeoverseN1)
+    set(KernelArmCPU "neoverse-n1" CACHE INTERNAL "")
 endif()
 if(KernelArchARM)
     config_set(KernelArmMach ARM_MACH "${KernelArmMach}")

include/arch/arm/arch/64/mode/hardware.h

@@ -180,7 +180,11 @@
 
 /* Top of the physical memory window */
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+#ifdef CONFIG_ARM_KERNEL_WINDOW_1GIB_PAGES
+#define PPTR_TOP UL_CONST(0x0000ffffc0000000)
+#else
 #define PPTR_TOP UL_CONST(0x000000ffc0000000)
+#endif
 #else
 #define PPTR_TOP UL_CONST(0xffffffffc0000000)
 #endif
@@ -198,7 +202,11 @@
 /* This is a page table mapping at the end of the virtual address space
  * to map objects with 4KiB pages rather than 4MiB large pages. */
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+#ifdef CONFIG_ARM_KERNEL_WINDOW_1GIB_PAGES
+#define KERNEL_PT_BASE UL_CONST(0x0000ffffffe00000)
+#else
 #define KERNEL_PT_BASE UL_CONST(0x000000ffffe00000)
+#endif
 #else
 #define KERNEL_PT_BASE UL_CONST(0xffffffffffe00000)
 #endif

include/arch/arm/arch/64/mode/model/statedata.h

@@ -28,8 +28,13 @@ extern asid_pool_t *armKSASIDTable[BIT(asidHighBits)] VISIBLE;
 extern vspace_root_t armKSGlobalUserVSpace[BIT(seL4_VSpaceIndexBits)] VISIBLE;
 extern pte_t armKSGlobalKernelPGD[BIT(PT_INDEX_BITS)] VISIBLE;
 
+#ifdef CONFIG_ARM_KERNEL_WINDOW_1GIB_PAGES
+extern pte_t armKSGlobalKernelPUDs[BIT(PT_INDEX_BITS)-1][BIT(PT_INDEX_BITS)] VISIBLE;
+extern pte_t armKSGlobalKernelPD[BIT(PT_INDEX_BITS)] VISIBLE;
+#else
 extern pte_t armKSGlobalKernelPUD[BIT(PT_INDEX_BITS)] VISIBLE;
 extern pte_t armKSGlobalKernelPDs[BIT(PT_INDEX_BITS)][BIT(PT_INDEX_BITS)] VISIBLE;
+#endif
 extern pte_t armKSGlobalKernelPT[BIT(PT_INDEX_BITS)] VISIBLE;
 
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

include/arch/arm/arch/machine/gic_common.h

@@ -61,7 +61,7 @@ irq_t irqInvalid = (uint16_t) -1;
 /* Setters/getters helpers for hardware irqs */
 #define IRQ_REG(IRQ) ((IRQ) >> 5u)
 #define IRQ_BIT(IRQ) ((IRQ) & 0x1f)
-#define IS_IRQ_VALID(X) (((X) & IRQ_MASK) < SPECIAL_IRQ_START)
+#define IS_IRQ_VALID(X) (((X) & IRQ_MASK) != IRQ_NONE)
 
 /*
  * The only sane way to get an GIC IRQ number that can be properly

include/arch/arm/arch/machine/gic_v3.h

@@ -295,6 +295,10 @@ static inline bool_t isIRQPending(void)
 
 static inline void maskInterrupt(bool_t disable, irq_t irq)
 {
+    if (irq > 8192) {
+        // Cannot enable or disable LPI interrupts
+        return;
+    }
 #if defined ENABLE_SMP_SUPPORT
     assert(!(IRQ_IS_PPI(irq)) || (IRQT_TO_CORE(irq) == getCurrentCPUIndex()));
 #endif
@@ -307,6 +311,12 @@ static inline void maskInterrupt(bool_t disable, irq_t irq)
 }
 
 
+// From the spec: "PPIs, SGIs, and SPIs have an active state in the IRI and must be deactivated."
+// And: "A valid write to ICC_EOIR0_EL1 or ICC_EOIR1_EL1 to perform a priority drop is required for each
+// acknowledged interrupt, even for LPIs which do not have an active state."
+// We use Split EOIMode and perform a priority drop for all interrupts received in handleInterrupt.
+// deactivateInterrupt does not need to be called for LPIs.
+// This means userspace does not need to perform an ack invocation for LPI interrupts.
 static inline void deactivateInterrupt(irq_t irq)
 {
     word_t hw_irq = IRQT_TO_IRQ(irq);

include/arch/arm/armv/armv8-a/64/armv/vcpu.h

@@ -596,6 +596,10 @@ static inline void vcpu_init_vtcr(void)
     vtcr_el2 = VTCR_EL2_T0SZ(24);                            // 40-bit input IPA
     vtcr_el2 |= VTCR_EL2_PS(PS_1T);                          // 40-bit PA size
     vtcr_el2 |= VTCR_EL2_SL0(SL0_4K_L1);                     // 4KiB, start at level 1
+#elif defined(CONFIG_ARM_PA_SIZE_BITS_48)
+    vtcr_el2 = VTCR_EL2_T0SZ(16);                            // 48-bit input IPA
+    vtcr_el2 |= VTCR_EL2_PS(PS_256T);                        // 48-bit PA size
+    vtcr_el2 |= VTCR_EL2_SL0(SL0_4K_L0);                     // 4KiB, start at level 0
 #else
     vtcr_el2 = VTCR_EL2_T0SZ(20);                            // 44-bit input IPA
     vtcr_el2 |= VTCR_EL2_PS(PS_16T);                         // 44-bit PA size

include/object/structures_32.bf

@@ -99,12 +99,7 @@ block irq_control_cap {
 }
 
 block irq_handler_cap {
-#ifdef ENABLE_SMP_SUPPORT
     field capIRQ   32
-#else
-    padding 24
-    field capIRQ 8
-#endif
 
     padding       24
     field capType  8

include/object/structures_64.bf

@@ -147,12 +147,7 @@ block irq_control_cap {
 }
 
 block irq_handler_cap {
-#ifdef ENABLE_SMP_SUPPORT
     field capIRQ 64
-#else
-    padding 52
-    field capIRQ 12
-#endif
 
     field capType  5
     padding 59

libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h

@@ -247,6 +247,8 @@ SEL4_SIZE_SANITY(seL4_VSpaceEntryBits, seL4_VSpaceIndexBits, seL4_VSpaceBits);
 #define seL4_UserTop 0x00000fffffffffff
 #elif defined(CONFIG_ARM_PA_SIZE_BITS_40)
 #define seL4_UserTop 0x000000ffffffffff
+#elif defined(CONFIG_ARM_PA_SIZE_BITS_48)
+#define seL4_UserTop 0x0000ffffffffffff
 #else
 #error "Unknown physical address width"
 #endif

libsel4/sel4_plat_include/altra/sel4/plat/api/constants.h

@@ -0,0 +1,9 @@
+/*
+ * Copyright 2025, Kry10 Limited.
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+
+#include <sel4/config.h>

src/arch/arm/64/kernel/vspace.c

@@ -233,6 +233,55 @@ BOOT_CODE void map_kernel_frame(paddr_t paddr, pptr_t vaddr, vm_rights_t vm_righ
                                                                                             attr_index);
 }
 
+#ifdef CONFIG_ARM_KERNEL_WINDOW_1GIB_PAGES
+
+BOOT_CODE void map_kernel_window(void)
+{
+
+    paddr_t paddr;
+    word_t idx;
+
+    /* verify that the kernel window as at the second entry of the PGD */
+    assert(GET_KPT_INDEX(PPTR_BASE, KLVL_FRM_ARM_PT_LVL(0)) == 1);
+    assert(IS_ALIGNED(PPTR_BASE, seL4_HugePageBits));
+    /* verify that the kernel device window is 1gb aligned and 1gb in size */
+    assert(GET_KPT_INDEX(PPTR_TOP, KLVL_FRM_ARM_PT_LVL(1)) == BIT(PT_INDEX_BITS) - 1);
+    assert(IS_ALIGNED(PPTR_TOP, seL4_HugePageBits));
+
+    // First we map 511 PUDs into the PGD:
+    for (idx = 1; idx < 512; idx++) {
+        armKSGlobalKernelPGD[idx] = pte_pte_table_new(addrFromKPPtr(armKSGlobalKernelPUDs[(idx-1)]));
+    }
+
+    // Next we create a lot of 1GiB PTE mappings but leave the last 1GiB entry empty.
+    for (idx = 0; idx < ((512*511) - 1); idx++) {
+        // Mapping in 1GiB increments:
+        paddr = PADDR_BASE + (idx * (1 << 30));
+
+        armKSGlobalKernelPUDs[idx / 512][idx % 512] = pte_pte_page_new(
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+                                                    0, // XN
+#else
+                                                    1, // UXN
+#endif
+                                                    paddr,
+                                                    0,                        /* global */
+                                                    1,                        /* access flag */
+                                                    SMP_TERNARY(SMP_SHARE, 0),        /* Inner-shareable if SMP enabled, otherwise unshared */
+                                                    0,                        /* VMKernelOnly */
+                                                    NORMAL
+                                                );
+    }
+
+    // Now need to map the kernel device mappings into the last entry
+    armKSGlobalKernelPUDs[511 - 1][511] = pte_pte_table_new(addrFromKPPtr(armKSGlobalKernelPD));
+    armKSGlobalKernelPD[511] = pte_pte_table_new(addrFromKPPtr(armKSGlobalKernelPT));
+
+    map_kernel_devices();
+}
+
+#else /* CONFIG_ARM_KERNEL_WINDOW_1GIB_PAGES */
+
 BOOT_CODE void map_kernel_window(void)
 {
 
@@ -297,6 +346,8 @@ BOOT_CODE void map_kernel_window(void)
     map_kernel_devices();
 }
 
+#endif
+
 /* When the hypervisor support is enabled, the stage-2 translation table format
  * is used for applications.
  * The global bit is always 0.

src/arch/arm/64/model/statedata.c

@@ -85,8 +85,13 @@ asid_pool_t *armKSASIDTable[BIT(asidHighBits)];
 vspace_root_t armKSGlobalUserVSpace[BIT(seL4_VSpaceIndexBits)] ALIGN_BSS(BIT(seL4_VSpaceBits));
 pte_t armKSGlobalKernelPGD[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
 
+#ifdef CONFIG_ARM_KERNEL_WINDOW_1GIB_PAGES
+pte_t armKSGlobalKernelPUDs[BIT(PT_INDEX_BITS)-1][BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
+pte_t armKSGlobalKernelPD[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
+#else
 pte_t armKSGlobalKernelPUD[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
 pte_t armKSGlobalKernelPDs[BIT(PT_INDEX_BITS)][BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
+#endif
 pte_t armKSGlobalKernelPT[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
 
 #ifdef CONFIG_KERNEL_LOG_BUFFER

src/arch/arm/config.cmake

@@ -12,6 +12,7 @@ endif()
 
 set(KernelArmPASizeBits40 OFF)
 set(KernelArmPASizeBits44 OFF)
+set(KernelArmPASizeBits48 OFF)
 if(KernelArmCortexA35)
     set(KernelArmICacheVIPT ON)
     set(KernelArmPASizeBits40 ON)
@@ -32,9 +33,17 @@ elseif(KernelArmCortexA72)
     # (https://developer.arm.com/documentation/100095/0001/memory-management-unit/about-the-mmu)
     set(KernelArmPASizeBits44 ON)
     math(EXPR KernelPaddrUserTop "(1 << 44)")
+elseif(KernelArmNeoverseN1)
+    # For Neoverse N1 in AArch64 state, the physical address range is 48 bits
+    set(KernelArmPASizeBits48 ON)
+    # The max physical address for kernel untypeds is still capped at 1 << 47
+    # because the kernel window isn't the full 48 bits.
+    math(EXPR KernelPaddrUserTop "(1 << 47)")
 endif()
+
 config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
 config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
+config_set(KernelArmPASizeBits48 ARM_PA_SIZE_BITS_48 "${KernelArmPASizeBits48}")
 config_set(KernelArmICacheVIPT ARM_ICACHE_VIPT "${KernelArmICacheVIPT}")
 
 if(KernelSel4ArchAarch32)
@@ -86,7 +95,7 @@ config_option(
     "Build as Hypervisor. Utilise ARM virtualisation extensions to build the kernel as a hypervisor"
     DEFAULT ${KernelSel4ArchArmHyp}
     DEPENDS
-        "KernelArmCortexA15 OR KernelArmCortexA35 OR KernelArmCortexA57 OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA72"
+        "KernelArmCortexA15 OR KernelArmCortexA35 OR KernelArmCortexA57 OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA72 OR KernelArmNeoverseN1"
 )
 
 config_option(KernelArmGicV3 ARM_GIC_V3_SUPPORT "Build support for GICv3" DEFAULT OFF)
@@ -229,6 +238,17 @@ config_choice(
     "tpidruro;KernelArmTLSRegTPIDRURO;ARM_TLS_REG_TPIDRURO;KernelArchARM"
 )
 
+config_option(
+    KernelArmKernelWindow1GiBPages
+    ARM_KERNEL_WINDOW_1GIB_PAGES
+    "Use 1 GiB pages for mapping the bulk of the kernel window. On machines that \
+    have large gaps between low and high mappings of DRAM, a 2MiB mapped kernel window \
+    that covers 512GiB of address space may not be large enough. A 1GiB mapped kernel \
+    window can cover > 255TiB of address space (511 entries in the top level)."
+    DEFAULT OFF
+    DEPENDS "KernelSel4ArchAarch64;KernelArmHypervisorSupport"
+)
+
 if(KernelArmTLSRegTPIDRURO)
     set(KernelSetTLSBaseSelf ON)
 endif()
@@ -246,6 +266,7 @@ if(
     OR KernelArmCortexA55
     OR KernelArmCortexA57
     OR KernelArmCortexA72
+    OR KernelArmNeoverseN1
 )
     # According to https://developer.arm.com/documentation/100095/0001/functional-description/about-the-cortex-a72-processor-functions/components-of-the-processor
     # the L1 instruction on the Cortex-A72 cache has a 64-byte cache line.

src/arch/arm/object/vcpu.c

@@ -424,7 +424,11 @@ exception_t decodeVCPUInjectIRQ(cap_t cap, word_t length, word_t *buffer)
 #endif
 
     /* Check IRQ parameters */
+#if defined(CONFIG_ARM_GIC_V3_SUPPORT) && defined(CONFIG_ARCH_AARCH64)
+    if (vid > (1U << 16) - 1) {
+#else
     if (vid > (1U << 10) - 1) {
+#endif
         current_syscall_error.type = seL4_RangeError;
         current_syscall_error.rangeErrorMin = 0;
         current_syscall_error.rangeErrorMax = (1U << 10) - 1;

src/plat/altra/config.cmake

@@ -0,0 +1,32 @@
+#
+# Copyright 2025, Kry10 Limited.
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+declare_platform(altra KernelPlatformAltra PLAT_ALTRA KernelArchARM)
+
+if(KernelPlatformAltra)
+    declare_seL4_arch(aarch64)
+    # TODO update this to neoverse when needed
+    set(KernelArmNeoverseN1 ON)
+    set(KernelArchArmV8a ON)
+    set(KernelArmGicV3 ON)
+    config_set(KernelARMPlatform ARM_PLAT ${KernelPlatform})
+    list(APPEND KernelDTSList "tools/dts/${KernelPlatform}.dts")
+    list(APPEND KernelDTSList "src/plat/altra/overlay-${KernelPlatform}.dts")
+    declare_default_headers(
+        TIMER_FREQUENCY 25000000
+        TIMER drivers/timer/arm_generic.h
+        TIMER_OVERHEAD_TICKS 1
+        NUM_PPI 32
+        MAX_IRQ 16383
+        INTERRUPT_CONTROLLER arch/machine/gic_v3.h
+        KERNEL_WCET 10u
+    )
+endif()
+
+add_sources(
+    DEP "KernelPlatformAltra"
+    CFILES src/arch/arm/machine/gic_v3.c src/arch/arm/machine/l2c_nop.c
+)

src/plat/altra/overlay-altra.dts

@@ -0,0 +1,18 @@
+/*
+ * Copyright 2025, Kry10 Limited.
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ */
+
+/ {
+	chosen {
+		seL4,elfloader-devices =
+			&{/timer};
+
+		seL4,kernel-devices =
+			&{/armpl011@100002600000},
+			&{/intc@gic},
+			&{/timer};
+	};
+
+};