Update to latest seL4

There are a couple of breaking changes to seL4 which affect the Microkit tool. * The size of seL4_MinSchedContextBits changing * The addition of the ARM SMC forwarding invocation * The change to page table invocations for AArch64 Signed-off-by: Ivan Velickovic <[email protected]>
seL4 · Jan 27, 2024 · 2f1ac4f · 2f1ac4f
1 parent 88666dc
commit 2f1ac4f
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 69 deletions.
diff --git a/README.md b/README.md
@@ -83,7 +83,7 @@ Please clone seL4 from:
 
 The correct branch to use is `microkit`.
 
-Testing has been performed using commit `92f0f3ab28f00c97851512216c855f4180534a60`.
+Testing has been performed using commit `7008430d4432c71a74b2a1da0afae58f7a8658df`.
 
 ## Building the SDK
 

diff --git a/tool/microkit/__main__.py b/tool/microkit/__main__.py
@@ -53,8 +53,6 @@
     Sel4Aarch64Regs,
     Sel4Invocation,
     Sel4AsidPoolAssign,
-    Sel4PageUpperDirectoryMap,
-    Sel4PageDirectoryMap,
     Sel4PageTableMap,
     Sel4PageMap,
     Sel4TcbSetSchedParams,
@@ -83,8 +81,6 @@
     SEL4_ENDPOINT_OBJECT,
     SEL4_NOTIFICATION_OBJECT,
     SEL4_VSPACE_OBJECT,
-    SEL4_PAGE_UPPER_DIRECTORY_OBJECT,
-    SEL4_PAGE_DIRECTORY_OBJECT,
     SEL4_SMALL_PAGE_OBJECT,
     SEL4_LARGE_PAGE_OBJECT,
     SEL4_PAGE_TABLE_OBJECT,
@@ -1154,11 +1150,11 @@ def build_system(
 
     vspace_objects = init_system.allocate_objects(SEL4_VSPACE_OBJECT, vspace_names)
 
-    ud_names = [f"PageUpperDirectory: PD={pd_names[pd_idx]} VADDR=0x{vaddr:x}" for pd_idx, vaddr in uds]
-    ud_objects = init_system.allocate_objects(SEL4_PAGE_UPPER_DIRECTORY_OBJECT, ud_names)
+    ud_names = [f"PageTable: PD={pd_names[pd_idx]} VADDR=0x{vaddr:x}" for pd_idx, vaddr in uds]
+    ud_objects = init_system.allocate_objects(SEL4_PAGE_TABLE_OBJECT, ud_names)
 
-    d_names = [f"PageDirectory: PD={pd_names[pd_idx]} VADDR=0x{vaddr:x}" for pd_idx, vaddr in ds]
-    d_objects = init_system.allocate_objects(SEL4_PAGE_DIRECTORY_OBJECT, d_names)
+    d_names = [f"PageTable: PD={pd_names[pd_idx]} VADDR=0x{vaddr:x}" for pd_idx, vaddr in ds]
+    d_objects = init_system.allocate_objects(SEL4_PAGE_TABLE_OBJECT, d_names)
 
     pt_names = [f"PageTable: PD={pd_names[pd_idx]} VADDR=0x{vaddr:x}" for pd_idx, vaddr in pts]
     pt_objects = init_system.allocate_objects(SEL4_PAGE_TABLE_OBJECT, pt_names)
@@ -1413,8 +1409,8 @@ def build_system(
 
     # Initialise the VSpaces -- assign them all the the initial asid pool.
     for map_cls, descriptors, objects in [
-        (Sel4PageUpperDirectoryMap, uds, ud_objects),
-        (Sel4PageDirectoryMap, ds, d_objects),
+        (Sel4PageTableMap, uds, ud_objects),
+        (Sel4PageTableMap, ds, d_objects),
         (Sel4PageTableMap, pts, pt_objects),
     ]:
         for ((pd_idx, vaddr), obj) in zip(descriptors, objects):

diff --git a/tool/microkit/sel4.py b/tool/microkit/sel4.py
@@ -20,8 +20,6 @@
 SEL4_NOTIFICATION_SIZE = (1 << 6)
 SEL4_REPLY_SIZE = (1 << 5)
 SEL4_PAGE_TABLE_SIZE = (1 << 12)
-SEL4_PAGE_DIRECTORY_SIZE = (1 << 12)
-SEL4_PAGE_UPPER_DIRECTORY_SIZE = (1 << 12)
 SEL4_LARGE_PAGE_SIZE = (2 * 1024 * 1024)
 SEL4_SMALL_PAGE_SIZE = (4 * 1024)
 SEL4_VSPACE_SIZE = (4 * 1024)
@@ -40,14 +38,10 @@
 SEL4_REPLY_OBJECT = 6
 
 SEL4_HUGE_PAGE_OBJECT = 7
-SEL4_PAGE_UPPER_DIRECTORY_OBJECT = 8
-SEL4_PAGE_GLOBAL_DIRECTORY_OBJECT = 9
-SEL4_SMALL_PAGE_OBJECT = 10
-SEL4_LARGE_PAGE_OBJECT = 11
-SEL4_PAGE_TABLE_OBJECT = 12
-SEL4_PAGE_DIRECTORY_OBJECT = 13
-
-SEL4_VSPACE_OBJECT = SEL4_PAGE_GLOBAL_DIRECTORY_OBJECT
+SEL4_VSPACE_OBJECT = 8
+SEL4_SMALL_PAGE_OBJECT = 9
+SEL4_LARGE_PAGE_OBJECT = 10
+SEL4_PAGE_TABLE_OBJECT = 11
 
 SEL4_OBJECT_TYPE_NAMES = {
     SEL4_UNTYPED_OBJECT: "SEL4_UNTYPED_OBJECT",
@@ -58,12 +52,10 @@
     SEL4_SCHEDCONTEXT_OBJECT: "SEL4_SCHEDCONTEXT_OBJECT",
     SEL4_REPLY_OBJECT: "SEL4_REPLY_OBJECT",
     SEL4_HUGE_PAGE_OBJECT: "SEL4_HUGE_PAGE_OBJECT",
-    SEL4_PAGE_UPPER_DIRECTORY_OBJECT: "SEL4_PAGE_UPPER_DIRECTORY_OBJECT",
-    SEL4_PAGE_GLOBAL_DIRECTORY_OBJECT: "SEL4_PAGE_GLOBAL_DIRECTORY_OBJECT",
     SEL4_SMALL_PAGE_OBJECT: "SEL4_SMALL_PAGE_OBJECT",
     SEL4_LARGE_PAGE_OBJECT: "SEL4_LARGE_PAGE_OBJECT",
     SEL4_PAGE_TABLE_OBJECT: "SEL4_PAGE_TABLE_OBJECT",
-    SEL4_PAGE_DIRECTORY_OBJECT: "SEL4_PAGE_DIRECTORY_OBJECT",
+    SEL4_VSPACE_OBJECT: "SEL4_VSPACE_OBJECT",
 }
 
 FIXED_OBJECT_SIZES = {
@@ -73,8 +65,6 @@
     SEL4_REPLY_OBJECT: SEL4_REPLY_SIZE,
 
     SEL4_VSPACE_OBJECT: SEL4_VSPACE_SIZE,
-    SEL4_PAGE_UPPER_DIRECTORY_OBJECT: SEL4_PAGE_UPPER_DIRECTORY_SIZE,
-    SEL4_PAGE_DIRECTORY_OBJECT: SEL4_PAGE_DIRECTORY_SIZE,
     SEL4_PAGE_TABLE_OBJECT: SEL4_PAGE_TABLE_SIZE,
 
     SEL4_LARGE_PAGE_OBJECT: SEL4_LARGE_PAGE_SIZE,
@@ -154,7 +144,7 @@ def calculate_rootserver_size(initial_task_region: MemoryRegion) -> int:
     asid_pool_bits = 12  # seL4_ASIDPoolBits
     vspace_bits = 12  # seL4_VSpaceBits
     page_table_bits = 12  # seL4_PageTableBits
-    min_sched_context_bits = 8  # seL4_MinSchedContextBits
+    min_sched_context_bits = 7  # seL4_MinSchedContextBits
 
     size = 0
     size += 1 << (root_cnode_bits + slot_bits)
@@ -352,27 +342,24 @@ class Sel4Label(IntEnum):
     ARMVSpaceInvalidate_Data = 37
     ARMVSpaceCleanInvalidate_Data = 38
     ARMVSpaceUnify_Instruction = 39
-    # ARM Page Upper Directory
-    ARMPageUpperDirectoryMap = 40
-    ARMPageUpperDirectoryUnmap = 41
-    ARMPageDirectoryMap = 42
-    ARMPageDirectoryUnmap = 43
+    # ARM SMC
+    ARMSMCCall = 40
     # ARM Page table
-    ARMPageTableMap = 44
-    ARMPageTableUnmap = 45
+    ARMPageTableMap = 41
+    ARMPageTableUnmap = 42
     # ARM Page
-    ARMPageMap = 46
-    ARMPageUnmap = 47
-    ARMPageClean_Data = 48
-    ARMPageInvalidate_Data = 49
-    ARMPageCleanInvalidate_Data = 50
-    ARMPageUnify_Instruction = 51
-    ARMPageGetAddress = 52
+    ARMPageMap = 43
+    ARMPageUnmap = 44
+    ARMPageClean_Data = 45
+    ARMPageInvalidate_Data = 46
+    ARMPageCleanInvalidate_Data = 47
+    ARMPageUnify_Instruction = 48
+    ARMPageGetAddress = 49
     # ARM Asid
-    ARMASIDControlMakePool = 53
-    ARMASIDPoolAssign = 54
+    ARMASIDControlMakePool = 50
+    ARMASIDPoolAssign = 51
     # ARM IRQ
-    ARMIRQIssueIRQHandlerTrigger = 55
+    ARMIRQIssueIRQHandlerTrigger = 52
 
 
 # Invocations
@@ -563,30 +550,6 @@ class Sel4IrqHandlerSetNotification(Sel4Invocation):
     notification: int
 
 
-@dataclass
-class Sel4PageUpperDirectoryMap(Sel4Invocation):
-    _object_type = "Page Upper Directory"
-    _method_name = "Map"
-    _extra_caps = ("vspace", )
-    label = Sel4Label.ARMPageUpperDirectoryMap
-    page_upper_directory: int
-    vspace: int
-    vaddr: int
-    attr: int
-
-
-@dataclass
-class Sel4PageDirectoryMap(Sel4Invocation):
-    _object_type = "Page Directory"
-    _method_name = "Map"
-    _extra_caps = ("vspace", )
-    label = Sel4Label.ARMPageDirectoryMap
-    page_directory: int
-    vspace: int
-    vaddr: int
-    attr: int
-
-
 @dataclass
 class Sel4PageTableMap(Sel4Invocation):
     _object_type = "Page Table"
@@ -858,7 +821,7 @@ def emulate_kernel_boot(
     else:
         raise Exception("Couldn't find appropriate region for initial task kernel objects")
 
-    fixed_cap_count = 0xf
+    fixed_cap_count = 0x10
     sched_control_cap_count = 1
     paging_cap_count = _get_arch_n_paging(initial_task_virt_region)
     page_cap_count = initial_task_virt_region.size // kernel_config.minimum_page_size