Improve page mapping benchmarks

Extended page mapping benchmarks to work on AARCH64,
changed CMake to make it clearer which architectures
are supported, and fixed a bug in the implementation.

Signed-off-by: Alwin Joshy <[email protected]>

apps/page_mapping/CMakeLists.txt

@@ -16,7 +16,7 @@ config_option(
     DEFAULT
     ON
     DEPENDS
-    "DefaultBenchDeps"
+    "DefaultBenchDeps; KernelSel4ArchAarch64 OR KernelArchX86"
 )
 add_config_library(sel4benchpagemapping "${configure_string}")
 

apps/page_mapping/src/main.c

@@ -18,9 +18,11 @@
 
 #if defined(CONFIG_ARCH_X86_64)
 #define DEFAULT_DEPTH 64
+#elif defined(CONFIG_ARCH_AARCH64)
+#define DEFAULT_DEPTH 64
 #else
 #define DEFAULT_DEPTH 32
-#endif /* defined(CONFIG_ARCH_X86_64) */
+#endif
 
 #define PAGE_PER_TABLE BIT(seL4_PageTableBits - seL4_WordSizeBits)
 #define untyped_retype_root(a,b,c,e)\
@@ -50,7 +52,6 @@ static void inline prepare_page_table(seL4_Word addr, int npage, seL4_CPtr untyp
 
         err = seL4_ARCH_PageTable_Map(pt, SEL4UTILS_PD_SLOT, addr,
                                       seL4_ARCH_Default_VMAttributes);
-
 #if defined(CONFIG_ARCH_X86_64)
         if (err) {
             seL4_CPtr pd = *free_slot;
@@ -77,8 +78,23 @@ static void inline prepare_page_table(seL4_Word addr, int npage, seL4_CPtr untyp
                                           seL4_ARCH_Default_VMAttributes);
         }
 
-#endif /* CONFIG_ARCH_X86_64 */
         assert(err == 0);
+#elif defined(CONFIG_ARCH_AARCH64)
+        while (err != seL4_DeleteFirst) {
+            pt = *free_slot;
+            err = untyped_retype_root(untyped, seL4_ARCH_PageTableObject,
+                                  seL4_PageTableBits, pt);
+            assert(err == 0);
+            (*free_slot)++;
+
+            err = seL4_ARCH_PageTable_Map(pt, SEL4UTILS_PD_SLOT, addr,
+                              seL4_ARCH_Default_VMAttributes);
+        }
+
+        seL4_CNode_Delete(SEL4UTILS_CNODE_SLOT, pt, DEFAULT_DEPTH);
+        (*free_slot)--;
+#endif
+
         addr += PAGE_SIZE_4K * PAGE_PER_TABLE;
     }
 }
@@ -91,12 +107,11 @@ static void inline prepare_pages(int npage, seL4_CPtr untyped,
         err = untyped_retype_root(untyped, seL4_ARCH_4KPage, seL4_PageBits,
                                   *free_slot);
         assert(err == 0);
-
         (*free_slot)++;
     }
 }
 
-static void inline map_pages(seL4_CPtr addr, seL4_CPtr page_cap, int npage)
+static void inline map_pages(seL4_Word addr, seL4_CPtr page_cap, int npage)
 {
     long err UNUSED;
     for (int i = 0; i < npage; i++) {
@@ -109,12 +124,13 @@ static void inline map_pages(seL4_CPtr addr, seL4_CPtr page_cap, int npage)
 }
 
 #define PROT_UNPROT_NPAGE(func, right)\
-    static void inline func(seL4_CPtr addr, seL4_CPtr page_cap, int npage){\
+    static void inline func(seL4_Word addr, seL4_CPtr page_cap, int npage){\
         long err UNUSED;\
         for(int i = 0; i < npage; i++){\
             err = seL4_ARCH_Page_Map(page_cap, SEL4UTILS_PD_SLOT, addr, right,\
                             seL4_ARCH_Default_VMAttributes);\
             assert(err == 0);\
+            addr += PAGE_SIZE_4K;\
             page_cap++;\
         }\
     }
@@ -134,8 +150,10 @@ bench_proc(int argc UNUSED, char *argv[])
 
     sel4bench_init();
 
+    /* First CPtr related to page tables */
     seL4_CPtr pt_ptr_start = free_slot;
-    /* Install page tables to avoid mapping to fail */
+
+    /* Map page tables */
     COMPILER_MEMORY_FENCE();
     SEL4BENCH_READ_CCNT(start);
 
@@ -145,8 +163,10 @@ bench_proc(int argc UNUSED, char *argv[])
     COMPILER_MEMORY_FENCE();
     send_result(result_ep, end - start);
 
+    /* First CPtr related to frame capabilities */
     seL4_CPtr page_ptr_start = free_slot;
-    /* allocate pages */
+
+    /* allocate frames */
     COMPILER_MEMORY_FENCE();
     SEL4BENCH_READ_CCNT(start);
 
@@ -156,7 +176,7 @@ bench_proc(int argc UNUSED, char *argv[])
     COMPILER_MEMORY_FENCE();
     send_result(result_ep, end - start);
 
-    /* Do the real mapping */
+    /* Map the frames with seL4_AllRights */
     COMPILER_MEMORY_FENCE();
     SEL4BENCH_READ_CCNT(start);
 
@@ -166,7 +186,7 @@ bench_proc(int argc UNUSED, char *argv[])
     COMPILER_MEMORY_FENCE();
     send_result(result_ep, end - start);
 
-    /* Protect mapped page as seL4_CanRead */
+    /* Protect mapped pages to seL4_CanRead */
     COMPILER_MEMORY_FENCE();
     SEL4BENCH_READ_CCNT(start);
 
@@ -176,7 +196,7 @@ bench_proc(int argc UNUSED, char *argv[])
     COMPILER_MEMORY_FENCE();
     send_result(result_ep, end - start);
 
-    /* Unprotect it back */
+    /* Unprotect mapped pages back to seL4_AllRights */
     COMPILER_MEMORY_FENCE();
     SEL4BENCH_READ_CCNT(start);
 
@@ -186,17 +206,26 @@ bench_proc(int argc UNUSED, char *argv[])
     COMPILER_MEMORY_FENCE();
     send_result(result_ep, end - start);
 
-    /* cleaning */
+    /* Cleaning up the pages */
     long err;
     for (int i = 0; i < npage; i++) {
         err = seL4_ARCH_Page_Unmap(page_ptr_start + i);
         ZF_LOGF_IFERR(err, "ummap page failed\n");
     }
 
-    for (int i = 0; i < NUM_PAGE_TABLE(npage); i++) {
-        err = seL4_ARCH_PageTable_Unmap(pt_ptr_start + i);
-        ZF_LOGF_IFERR(err, "ummap page table failed\n");
-
+    /* Cleaning up the page table structures */
+    for (int i = pt_ptr_start; i < page_ptr_start; i++) {
+#ifdef CONFIG_ARCH_X86_64
+        err = seL4_X86_PDPT_Map(i);
+        if (err) {
+            err = seL4_ARM_PageDirectory_Unmap(i);
+            if (err) {
+                err = seL4_ARM_PageTable_Unmap(i);
+            }
+        }
+#elif CONFIG_ARCH_AARCH64
+        seL4_ARM_PageTable_Unmap(i);
+#endif
     }
 
     sel4bench_destroy();