Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update to latest seL4 #93

Merged
merged 1 commit into from
Jan 27, 2024
Merged

Update to latest seL4 #93

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
16 changes: 6 additions & 10 deletions tool/microkit/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,8 +53,6 @@
Sel4Aarch64Regs,
Sel4Invocation,
Sel4AsidPoolAssign,
Sel4PageUpperDirectoryMap,
Sel4PageDirectoryMap,
Sel4PageTableMap,
Sel4PageMap,
Sel4TcbSetSchedParams,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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):
Expand Down
79 changes: 21 additions & 58 deletions tool/microkit/sel4.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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",
Expand All @@ -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 = {
Expand All @@ -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,
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down
Loading