1-- 2-- Copyright 2014, General Dynamics C4 Systems 3-- 4-- SPDX-License-Identifier: GPL-2.0-only 5-- 6 7-- Default base size: uint32_t 8base 32 9 10block null_cap { 11 padding 32 12 13 padding 28 14 field capType 4 15} 16 17-- The combination of freeIndex and blockSize must match up with the 18-- definitions of MIN_SIZE_BITS and MAX_SIZE_BITS 19block untyped_cap { 20 field capFreeIndex 26 21 field capIsDevice 1 22 field capBlockSize 5 23 24 field_high capPtr 28 25 field capType 4 26} 27 28block endpoint_cap(capEPBadge, capCanGrantReply, capCanGrant, capCanSend, 29 capCanReceive, capEPPtr, capType) { 30 field_high capEPPtr 28 31 field capCanGrantReply 1 32 field capCanGrant 1 33 field capCanReceive 1 34 field capCanSend 1 35 36 field capEPBadge 28 37 field capType 4 38} 39 40block notification_cap { 41 field capNtfnBadge 28 42 padding 2 43 field capNtfnCanReceive 1 44 field capNtfnCanSend 1 45 46 field_high capNtfnPtr 28 47 field capType 4 48} 49 50#ifdef CONFIG_KERNEL_MCS 51block reply_cap { 52 field capReplyPtr 32 53 54 padding 27 55 field capReplyCanGrant 1 56 field capType 4 57} 58 59block call_stack { 60 field_high callStackPtr 28 61 padding 3 62 field isHead 1 63} 64#else 65block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) { 66 padding 32 67 68 field_high capTCBPtr 26 69 field capReplyCanGrant 1 70 field capReplyMaster 1 71 field capType 4 72} 73#endif 74-- The user-visible format of the data word is defined by cnode_capdata, below. 75block cnode_cap(capCNodeRadix, capCNodeGuardSize, capCNodeGuard, 76 capCNodePtr, capType) { 77 padding 4 78 field capCNodeGuardSize 5 79 field capCNodeRadix 5 80 field capCNodeGuard 18 81 82 field_high capCNodePtr 27 83 padding 1 84 field capType 4 85} 86 87block thread_cap { 88 padding 32 89 90 field_high capTCBPtr 28 91 field capType 4 92} 93 94block irq_control_cap { 95 padding 32 96 97 padding 24 98 field capType 8 99} 100 101block irq_handler_cap { 102#ifdef ENABLE_SMP_SUPPORT 103 field capIRQ 32 104#else 105 padding 24 106 field capIRQ 8 107#endif 108 109 padding 24 110 field capType 8 111} 112 113block zombie_cap { 114 field capZombieID 32 115 116 padding 18 117 field capZombieType 6 118 field capType 8 119} 120 121block domain_cap { 122 padding 32 123 124 padding 24 125 field capType 8 126} 127 128#ifdef CONFIG_KERNEL_MCS 129block sched_context_cap { 130 field_high capSCPtr 28 131 padding 4 132 133 padding 18 134 field capSCSizeBits 6 135 field capType 8 136} 137 138block sched_control_cap { 139 field core 32 140 141 padding 24 142 field capType 8 143} 144#endif 145---- Arch-independent object types 146 147-- Endpoint: size = 16 bytes 148block endpoint { 149 padding 64 150 151 field_high epQueue_head 28 152 padding 4 153 154 field_high epQueue_tail 28 155 padding 2 156 field state 2 157} 158 159-- Notification object: size = 16 bytes (32 bytes on mcs) 160block notification { 161#ifdef CONFIG_KERNEL_MCS 162 padding 96 163 164 field_high ntfnSchedContext 28 165 padding 4 166#endif 167 168 field_high ntfnBoundTCB 28 169 padding 4 170 171 field ntfnMsgIdentifier 32 172 173 field_high ntfnQueue_head 28 174 padding 4 175 176 field_high ntfnQueue_tail 28 177 padding 2 178 field state 2 179} 180 181-- Mapping database (MDB) node: size = 8 bytes 182block mdb_node { 183 field_high mdbNext 29 184 padding 1 185 field mdbRevocable 1 186 field mdbFirstBadged 1 187 188 field_high mdbPrev 29 189 padding 3 190} 191 192-- Thread state data 193-- 194-- tsType 195-- * Running 196-- * Restart 197-- * Inactive 198-- * BlockedOnReceive 199-- - Endpoint 200-- - CanGrant 201-- * BlockedOnSend 202-- - Endpoint 203-- - CanGrant 204-- - CanGrantReply 205-- - IsCall 206-- - IPCBadge 207-- - Fault 208-- - faultType 209-- * CapFault 210-- - Address 211-- - InReceivePhase 212-- - LookupFailure 213-- - lufType 214-- * InvalidRoot 215-- * MissingCapability 216-- - BitsLeft 217-- * DepthMismatch 218-- - BitsFound 219-- - BitsLeft 220-- * GuardMismatch 221-- - GuardFound 222-- - BitsLeft 223-- - GuardSize 224-- * VMFault 225-- - Address 226-- - FSR 227-- - FaultType 228-- * UnknownSyscall 229-- - Number 230-- * UserException 231-- - Number 232-- - Code 233-- * BlockedOnReply 234-- * BlockedOnFault 235-- - Fault 236-- * BlockedOnNotification 237-- - Notification 238-- * Idle 239 240-- Lookup fault: size = 8 bytes 241block invalid_root { 242 padding 62 243 field lufType 2 244} 245 246block missing_capability { 247 padding 56 248 field bitsLeft 6 249 field lufType 2 250} 251 252block depth_mismatch { 253 padding 50 254 field bitsFound 6 255 field bitsLeft 6 256 field lufType 2 257} 258 259block guard_mismatch { 260 field guardFound 32 261 padding 18 262 field bitsLeft 6 263 field bitsFound 6 264 field lufType 2 265} 266 267tagged_union lookup_fault lufType { 268 tag invalid_root 0 269 tag missing_capability 1 270 tag depth_mismatch 2 271 tag guard_mismatch 3 272} 273 274-- Fault: size = 8 bytes 275block NullFault { 276 padding 60 277 field seL4_FaultType 4 278} 279 280block CapFault { 281 field address 32 282 field inReceivePhase 1 283 padding 27 284 field seL4_FaultType 4 285} 286 287block UnknownSyscall { 288 field syscallNumber 32 289 padding 28 290 field seL4_FaultType 4 291} 292 293block UserException { 294 field number 32 295 field code 28 296 field seL4_FaultType 4 297} 298 299#ifdef CONFIG_HARDWARE_DEBUG_API 300block DebugException { 301 field breakpointAddress 32 302 303 padding 20 304 -- X86 has 4 breakpoints (DR0-3). 305 -- ARM has between 2 and 16 breakpoints 306 -- ( ARM Ref manual, C3.3). 307 -- So we just use 4 bits to cater for both. 308 field breakpointNumber 4 309 field exceptionReason 4 310 field seL4_FaultType 4 311} 312#endif 313 314#ifdef CONFIG_KERNEL_MCS 315block Timeout { 316 field badge 32 317 padding 28 318 field seL4_FaultType 4 319} 320#endif 321 322-- Thread state: size = 12 bytes 323block thread_state(blockingIPCBadge, blockingIPCCanGrant, 324 blockingIPCCanGrantReply, blockingIPCIsCall, 325 tcbQueued, blockingObject, 326#ifdef CONFIG_KERNEL_MCS 327 tcbInReleaseQueue, replyObject, 328#endif 329 tsType) { 330 field blockingIPCBadge 28 331 field blockingIPCCanGrant 1 332 field blockingIPCCanGrantReply 1 333 field blockingIPCIsCall 1 334 padding 1 335 336 -- this is fastpath-specific. it is useful to be able to write 337 -- tsType and without changing tcbQueued or tcbInReleaseQueue 338#ifdef CONFIG_KERNEL_MCS 339 field_high replyObject 28 340 padding 2 341#else 342 padding 31 343#endif 344 field tcbQueued 1 345#ifdef CONFIG_KERNEL_MCS 346 field tcbInReleaseQueue 1 347#endif 348 349 field_high blockingObject 28 350 field tsType 4 351} 352