1c28462ebf
The kernel expects object sizes to be powers of two for size and alignment computations. - add missing padding for MCS 64-bit configurations for notifications (other configs were already fine) - add missing padding for reply object struct - strengthen compile time assertion to catch discrepancies in the future. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
468 lines
8.6 KiB
Brainfuck
468 lines
8.6 KiB
Brainfuck
--
|
|
-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
|
--
|
|
-- SPDX-License-Identifier: GPL-2.0-only
|
|
--
|
|
|
|
block null_cap {
|
|
padding 64
|
|
|
|
field capType 5
|
|
padding 59
|
|
}
|
|
|
|
block untyped_cap {
|
|
#if BF_CANONICAL_RANGE == 48
|
|
field capFreeIndex 48
|
|
padding 9
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
field capFreeIndex 39
|
|
padding 18
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
field capIsDevice 1
|
|
field capBlockSize 6
|
|
|
|
field capType 5
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 11
|
|
field_high capPtr 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 20
|
|
field_high capPtr 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
}
|
|
|
|
block endpoint_cap(capEPBadge, capCanGrantReply, capCanGrant, capCanSend,
|
|
capCanReceive, capEPPtr, capType) {
|
|
field capEPBadge 64
|
|
|
|
field capType 5
|
|
field capCanGrantReply 1
|
|
field capCanGrant 1
|
|
field capCanReceive 1
|
|
field capCanSend 1
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 7
|
|
field_high capEPPtr 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 16
|
|
field_high capEPPtr 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
|
|
}
|
|
|
|
block notification_cap {
|
|
field capNtfnBadge 64
|
|
|
|
field capType 5
|
|
field capNtfnCanReceive 1
|
|
field capNtfnCanSend 1
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 9
|
|
field_high capNtfnPtr 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 18
|
|
field_high capNtfnPtr 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
}
|
|
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
block reply_cap {
|
|
field capReplyPtr 64
|
|
|
|
field capType 5
|
|
field capReplyCanGrant 1
|
|
padding 58
|
|
}
|
|
|
|
block call_stack(callStackPtr, isHead) {
|
|
padding 15
|
|
field isHead 1
|
|
#if BF_CANONICAL_RANGE == 48
|
|
field_high callStackPtr 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 9
|
|
field_high callStackPtr 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
}
|
|
#else
|
|
block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
|
|
field capTCBPtr 64
|
|
|
|
field capType 5
|
|
padding 57
|
|
field capReplyCanGrant 1
|
|
field capReplyMaster 1
|
|
}
|
|
#endif
|
|
|
|
-- The user-visible format of the data word is defined by cnode_capdata, below.
|
|
block cnode_cap(capCNodeRadix, capCNodeGuardSize, capCNodeGuard,
|
|
capCNodePtr, capType) {
|
|
field capCNodeGuard 64
|
|
|
|
field capType 5
|
|
field capCNodeGuardSize 6
|
|
field capCNodeRadix 6
|
|
#if BF_CANONICAL_RANGE == 48
|
|
field_high capCNodePtr 47
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 9
|
|
field_high capCNodePtr 38
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
}
|
|
|
|
block thread_cap {
|
|
padding 64
|
|
|
|
field capType 5
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 11
|
|
field_high capTCBPtr 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 20
|
|
field_high capTCBPtr 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
}
|
|
|
|
block irq_control_cap {
|
|
padding 64
|
|
|
|
field capType 5
|
|
padding 59
|
|
}
|
|
|
|
block irq_handler_cap {
|
|
#ifdef ENABLE_SMP_SUPPORT
|
|
field capIRQ 64
|
|
#else
|
|
padding 52
|
|
field capIRQ 12
|
|
#endif
|
|
|
|
field capType 5
|
|
padding 59
|
|
}
|
|
|
|
block zombie_cap {
|
|
field capZombieID 64
|
|
|
|
field capType 5
|
|
padding 52
|
|
field capZombieType 7
|
|
}
|
|
|
|
block domain_cap {
|
|
padding 64
|
|
|
|
field capType 5
|
|
padding 59
|
|
}
|
|
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
block sched_context_cap {
|
|
#if BF_CANONICAL_RANGE == 48
|
|
field_high capSCPtr 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 9
|
|
field_high capSCPtr 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
field capSCSizeBits 6
|
|
padding 10
|
|
|
|
field capType 5
|
|
padding 59
|
|
}
|
|
|
|
block sched_control_cap {
|
|
field core 64
|
|
|
|
field capType 5
|
|
padding 59
|
|
}
|
|
#endif
|
|
|
|
---- Arch-independent object types
|
|
|
|
-- Endpoint: size = 16 bytes
|
|
block endpoint {
|
|
field epQueue_head 64
|
|
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 16
|
|
field_high epQueue_tail 46
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 25
|
|
field_high epQueue_tail 37
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
field state 2
|
|
}
|
|
|
|
-- Async endpoint: size = 32 bytes (64 bytes on mcs)
|
|
block notification {
|
|
#if BF_CANONICAL_RANGE == 48
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
padding 192
|
|
padding 16
|
|
field_high ntfnSchedContext 48
|
|
#endif
|
|
padding 16
|
|
field_high ntfnBoundTCB 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
padding 192
|
|
padding 25
|
|
field_high ntfnSchedContext 39
|
|
#endif
|
|
padding 25
|
|
field_high ntfnBoundTCB 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
|
|
field ntfnMsgIdentifier 64
|
|
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 16
|
|
field_high ntfnQueue_head 48
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 25
|
|
field_high ntfnQueue_head 39
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
|
|
#if BF_CANONICAL_RANGE == 48
|
|
field_high ntfnQueue_tail 48
|
|
padding 14
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
field_high ntfnQueue_tail 39
|
|
padding 23
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
field state 2
|
|
}
|
|
|
|
-- Mapping database (MDB) node: size = 16 bytes
|
|
block mdb_node {
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 16
|
|
field_high mdbNext 46
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 25
|
|
field_high mdbNext 37
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
field mdbRevocable 1
|
|
field mdbFirstBadged 1
|
|
|
|
field mdbPrev 64
|
|
}
|
|
|
|
-- Thread state data
|
|
--
|
|
-- tsType
|
|
-- * Running
|
|
-- * Restart
|
|
-- * Inactive
|
|
-- * BlockedOnReceive
|
|
-- - Endpoint
|
|
-- - CanGrant
|
|
-- * BlockedOnSend
|
|
-- - Endpoint
|
|
-- - CanGrant
|
|
-- - CanGrantReply
|
|
-- - IsCall
|
|
-- - IPCBadge
|
|
-- - Fault
|
|
-- - seL4_FaultType
|
|
-- * CapFault
|
|
-- - Address
|
|
-- - InReceivePhase
|
|
-- - LookupFailure
|
|
-- - lufType
|
|
-- * InvalidRoot
|
|
-- * MissingCapability
|
|
-- - BitsLeft
|
|
-- * DepthMismatch
|
|
-- - BitsFound
|
|
-- - BitsLeft
|
|
-- * GuardMismatch
|
|
-- - GuardFound
|
|
-- - BitsLeft
|
|
-- - GuardSize
|
|
-- * VMFault
|
|
-- - Address
|
|
-- - FSR
|
|
-- - FaultType
|
|
-- * UnknownSyscall
|
|
-- - Number
|
|
-- * UserException
|
|
-- - Number
|
|
-- - Code
|
|
-- * BlockedOnReply
|
|
-- * BlockedOnFault
|
|
-- - Fault
|
|
-- * BlockedOnNotification
|
|
-- - Notification
|
|
-- * Idle
|
|
|
|
-- Lookup fault: size = 16 bytes
|
|
block invalid_root {
|
|
padding 64
|
|
|
|
padding 62
|
|
field lufType 2
|
|
}
|
|
|
|
block missing_capability {
|
|
padding 64
|
|
|
|
padding 55
|
|
field bitsLeft 7
|
|
field lufType 2
|
|
}
|
|
|
|
block depth_mismatch {
|
|
padding 64
|
|
|
|
padding 48
|
|
field bitsFound 7
|
|
field bitsLeft 7
|
|
field lufType 2
|
|
}
|
|
|
|
block guard_mismatch {
|
|
field guardFound 64
|
|
|
|
padding 48
|
|
field bitsLeft 7
|
|
field bitsFound 7
|
|
field lufType 2
|
|
}
|
|
|
|
tagged_union lookup_fault lufType {
|
|
tag invalid_root 0
|
|
tag missing_capability 1
|
|
tag depth_mismatch 2
|
|
tag guard_mismatch 3
|
|
}
|
|
|
|
-- Fault: size = 16 bytes
|
|
block NullFault {
|
|
padding 64
|
|
|
|
padding 60
|
|
field seL4_FaultType 4
|
|
}
|
|
|
|
block CapFault {
|
|
field address 64
|
|
|
|
field inReceivePhase 1
|
|
padding 59
|
|
field seL4_FaultType 4
|
|
}
|
|
|
|
block UnknownSyscall {
|
|
field syscallNumber 64
|
|
|
|
padding 60
|
|
field seL4_FaultType 4
|
|
}
|
|
|
|
block UserException {
|
|
padding 64
|
|
|
|
field number 32
|
|
field code 28
|
|
field seL4_FaultType 4
|
|
}
|
|
|
|
#ifdef CONFIG_HARDWARE_DEBUG_API
|
|
block DebugException {
|
|
field breakpointAddress 64
|
|
|
|
padding 52
|
|
-- X86 has 4 breakpoints (DR0-3).
|
|
-- ARM has between 2 and 16 breakpoints
|
|
-- ( ARM Ref manual, C3.3).
|
|
-- So we just use 4 bits to cater for both.
|
|
field breakpointNumber 4
|
|
field exceptionReason 4
|
|
field seL4_FaultType 4
|
|
}
|
|
#endif
|
|
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
block Timeout {
|
|
field badge 64
|
|
padding 60
|
|
field seL4_FaultType 4
|
|
}
|
|
#endif
|
|
|
|
-- Thread state: size = 24 bytes
|
|
block thread_state(blockingIPCBadge, blockingIPCCanGrant,
|
|
blockingIPCCanGrantReply, blockingIPCIsCall,
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
tcbQueued, tsType,
|
|
tcbInReleaseQueue, blockingObject, replyObject) {
|
|
#else
|
|
tcbQueued, blockingObject,
|
|
tsType) {
|
|
#endif
|
|
field blockingIPCBadge 64
|
|
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 15
|
|
field_high replyObject 44
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 24
|
|
field_high replyObject 35
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
#else
|
|
padding 60
|
|
#endif
|
|
field blockingIPCCanGrant 1
|
|
field blockingIPCCanGrantReply 1
|
|
field blockingIPCIsCall 1
|
|
field tcbQueued 1
|
|
#ifdef CONFIG_KERNEL_MCS
|
|
field tcbInReleaseQueue 1
|
|
#endif
|
|
|
|
#if BF_CANONICAL_RANGE == 48
|
|
padding 16
|
|
field_high blockingObject 44
|
|
#elif BF_CANONICAL_RANGE == 39
|
|
padding 25
|
|
field_high blockingObject 35
|
|
#else
|
|
#error "Unspecified canonical address range"
|
|
#endif
|
|
field tsType 4
|
|
}
|