From 34248a6d7e5720eec1d6a358237af9e453631f75 Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Sat, 27 Jan 2024 12:04:46 +1100 Subject: [PATCH] tool: 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 --- README.md | 2 +- tool/microkit/__main__.py | 16 +++----- tool/microkit/sel4.py | 79 +++++++++++---------------------------- 3 files changed, 28 insertions(+), 69 deletions(-) diff --git a/README.md b/README.md index ce2b8b8a9..7542aa330 100644 --- 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 index 601c73ff6..24d43eaee 100644 --- 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 index f2005564b..87c16a7f8 100644 --- 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