draft: loader MMU changes, map RAM (and only RAM)

docs/manual.md

@@ -1817,6 +1817,7 @@ At build-time, the Microkit tool embeds the capDL specification that describe
 all kernel objects that needs to be created. Then for each kernel object, the spec
 describe what state they need to be in and what capabilities exist to that object
 (i.e. who has access to this kernel object). For example, the spec would specify the:
+
 - starting Instruction Pointer (IP), Stack Pointer (SP) and IPC buffer pointer of a Thread Control Block (TCB),
 - page table structure and mapping attributes of an address space (VSpace),
 - interrupts (IRQ),
@@ -1868,7 +1869,7 @@ In order to do this however, the Microkit tool needs to emulate how the seL4 ker
 to obtain the list of free untyped objects that the kernel would give to the initial task.
 
 While this is non-trivial to do, it comes with the useful property that if the tool
-produces a valid image, there should be no errors upon initialising the system
+produces a valid image, there should be no errors upon initialising the system.
 If there are any errors with configuring the system (e.g running out of memory),
 they will be caught at build-time. This can only reasonably be done due to the
 static-architecture of Microkit systems.

loader/src/aarch64/mmu.c

@@ -12,18 +12,13 @@
 #include "../cutil.h"
 #include "../uart.h"
 
-void el1_mmu_enable(void);
-void el2_mmu_enable(void);
+void el1_mmu_enable(uint64_t aarch64_pt_ttbr0_el1, uint64_t aarch64_pt_ttbr1_el1);
+void el2_mmu_enable(uint64_t aarch64_pt_ttbr0_el2);
 
-/* Paging structures for kernel mapping */
-uint64_t boot_lvl0_upper[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl1_upper[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl2_upper[1 << 9] ALIGN(1 << 12);
-
-/* Paging structures for identity mapping */
-uint64_t boot_lvl0_lower[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl1_lower[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl2_lower[1 << 9] ALIGN(1 << 12);
+/* Pointers to the top-level paging structures */
+uint64_t aarch64_pt_ttbr0_el1;
+uint64_t aarch64_pt_ttbr1_el1;
+uint64_t aarch64_pt_ttbr0_el2;
 
 int arch_mmu_enable(int logical_cpu)
 {
@@ -37,9 +32,9 @@ int arch_mmu_enable(int logical_cpu)
     LDR_PRINT("INFO", logical_cpu, "enabling MMU\n");
     el = current_el();
     if (el == EL1) {
-        el1_mmu_enable();
+        el1_mmu_enable(aarch64_pt_ttbr0_el1, aarch64_pt_ttbr1_el1);
     } else if (el == EL2) {
-        el2_mmu_enable();
+        el2_mmu_enable(aarch64_pt_ttbr0_el2);
     } else {
         LDR_PRINT("ERROR", logical_cpu, "unknown EL for MMU enable\n");
     }

loader/src/aarch64/util64.S

@@ -308,7 +308,6 @@ END_FUNC(el1_mmu_disable)
 
 BEGIN_FUNC(el2_mmu_disable)
     stp     x29, x30, [sp, #-16]!
-    stp     x27, x28, [sp, #-16]!
     mov     x29, sp
 
     /* Disable caches */
@@ -323,14 +322,18 @@ BEGIN_FUNC(el2_mmu_disable)
      */
     bl      invalidate_icache
 
-    ldp     x27, x28, [sp], #16
     ldp     x29, x30, [sp], #16
     ret
 END_FUNC(el2_mmu_disable)
 
+/*
+ * Enables the MMU for EL2.
+ * Takes two arguments the physical address for TTBR0_EL1 (x0) and TTBR1_EL1 (x1).
+ */
 BEGIN_FUNC(el1_mmu_enable)
     stp     x29, x30, [sp, #-16]!
     stp     x27, x28, [sp, #-16]!
+    /* move caller-saved to callee-saved registers */
     mov     x29, sp
     mov     x27, x0
     mov     x28, x1
@@ -358,10 +361,8 @@ BEGIN_FUNC(el1_mmu_enable)
     msr     tcr_el1, x10
 
     /* Setup page tables */
-    adrp    x8, boot_lvl0_lower
-    msr     ttbr0_el1, x8
-    adrp    x8, boot_lvl0_upper
-    msr     ttbr1_el1, x8
+    msr     ttbr0_el1, x27  /* argument 0 */
+    msr     ttbr1_el1, x28  /* argument 1 */
     isb
 
     /* invalidate all TLB entries for EL1 */
@@ -374,12 +375,18 @@ BEGIN_FUNC(el1_mmu_enable)
     ldp     x27, x28, [sp], #16
     ldp     x29, x30, [sp], #16
     ret
-
 END_FUNC(el1_mmu_enable)
 
+/*
+ * Enables the MMU for EL2.
+ * Takes one argument, the physical address for TTBR0_EL2 (x0).
+ */
 BEGIN_FUNC(el2_mmu_enable)
     stp     x29, x30, [sp, #-16]!
+    stp     x27, x28, [sp, #-16]!
+    /* move caller-saved to callee-saved registers */
     mov     x29, sp
+    mov     x28, x0
 
     /* Disable the MMU */
     bl      el2_mmu_disable
@@ -403,8 +410,7 @@ BEGIN_FUNC(el2_mmu_enable)
     isb
 
     /* Setup page tables */
-    adrp    x8, boot_lvl0_lower
-    msr     ttbr0_el2, x8
+    msr     ttbr0_el2, x28  /* argument 0 */
     isb
 
     /* invalidate all TLB entries for EL2 */
@@ -423,9 +429,9 @@ BEGIN_FUNC(el2_mmu_enable)
     dsb     ish
     isb
 
+    ldp     x27, x28, [sp], #16
     ldp     x29, x30, [sp], #16
     ret
-
 END_FUNC(el2_mmu_enable)
 
 .extern arm_secondary_cpu_c_entry

loader/src/riscv/mmu.c

@@ -8,15 +8,9 @@
 #include <stdint.h>
 
 #include "../arch.h"
-#include "../cutil.h"
-
-/* Paging structures for kernel mapping */
-uint64_t boot_lvl1_pt[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl2_pt[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl3_pt[1 << 9] ALIGN(1 << 12);
-/* Paging structures for identity mapping */
-uint64_t boot_lvl2_pt_loader[1 << 9] ALIGN(1 << 12);
 
+/* Pointers to the top-level paging structures */
+uintptr_t riscv64_boot_lvl1_pt;
 
 /*
  * This is the encoding for the MODE field of the satp register when
@@ -36,7 +30,7 @@ int arch_mmu_enable(int logical_cpu)
     asm volatile(
         "csrw satp, %0\n"
         :
-        : "r"(VM_MODE | (uintptr_t)boot_lvl1_pt >> RISCV_PGSHIFT)
+        : "r"(VM_MODE | riscv64_boot_lvl1_pt >> RISCV_PGSHIFT)
         :
     );
     asm volatile("fence.i" ::: "memory");