1<?xml version="1.0" ?> 2<!-- 3 Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 4 5 SPDX-License-Identifier: BSD-2-Clause 6--> 7 8<api name="ObjectApi"> 9 10 <interface name="seL4_Untyped" manual_name="Untyped" cap_description="CPTR to an untyped object."> 11 12 <method id="UntypedRetype" name="Retype" manual_name="Retype" manual_label="untyped_retype"> 13 <brief> 14 Retype an untyped object 15 </brief> 16 <description> 17 Given a capability, <texttt text="_service"/>, to an untyped object, 18 creates <texttt text="num_objects"/> of the requested type. Creates 19 <texttt text="num_objects"/> capabilities to the new objects starting 20 at <texttt text="node_offset"/> in the CNode specified by 21 <texttt text="root"/>, <texttt text="node_index"/>, and 22 <texttt text="node_depth"/>. 23 24 For variable-sized 25 kernel objects, the <texttt text="size_bits"/> argument is used to 26 determine the size of objects to create. The relationship between 27 <texttt text="size_bits"/> and object size depends on the type of object 28 being created. <docref>See <autoref label="sec:object_sizes"/> for more information 29 about object sizes.</docref> 30 31 <docref>See <autoref label="sec:kernmemalloc"/> for more information about how untyped 32 memory is retyped.</docref> 33 34 <docref>See <autoref label="sec:caps_to_new_objects"/> for more information about the 35 placement of capabilities to created objects.</docref> 36 </description> 37 <param dir="in" name="type" type="seL4_Word" 38 description="The seL4 object type that we are retyping to."/> 39 <param dir="in" name="size_bits" type="seL4_Word" 40 description="Used to determine the size of variable-sized objects."/> 41 <param dir="in" name="root" type="seL4_CNode" 42 description="CPTR to the CNode at the root of the destination CSpace."/> 43 <param dir="in" name="node_index" type="seL4_Word" 44 description="CPTR to the destination CNode. Resolved relative to the root parameter."/> 45 <param dir="in" name="node_depth" type="seL4_Word" 46 description="Number of bits of node_index to translate when addressing the destination CNode."/> 47 <param dir="in" name="node_offset" type="seL4_Word" 48 description="Number of slots into the node at which capabilities start being placed."/> 49 <param dir="in" name="num_objects" type="seL4_Word" 50 description="Number of capabilities to create."/> 51 <error name="seL4_DeleteFirst" description="A capability exists in the destination window of the CNode."/> 52 <error name="seL4_FailedLookup"> 53 <description> 54 The <texttt text="root"/>, <texttt text="node_index"/>, or <texttt text="node_depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 55 </description> 56 </error> 57 <error name="seL4_IllegalOperation"> 58 <description> 59 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 60 </description> 61 </error> 62 <error name="seL4_InvalidArgument"> 63 <description> 64 The <texttt text="size_bits"/> is too big or too small for the requested object type. 65 Or, <texttt text="type"/> cannot be created from a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>)</docref>. 66 Or, the requested object <texttt text="type"/> does not exist. 67 </description> 68 </error> 69 <error name="seL4_InvalidCapability"> 70 <description> 71 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 72 </description> 73 </error> 74 <error name="seL4_NotEnoughMemory" description="The total size of the new objects exceeds the space available."/> 75 <error name="seL4_RangeError"> 76 <description> 77 The <texttt text="num_objects"/> do not fit in the destination CNode at <texttt text="node_offset"/>. 78 Or, <texttt text="num_objects"/> is greater than <texttt text="CONFIG_RETYPE_FAN_OUT_LIMIT"/>. 79 Or, <texttt text="size_bits"/> is too large. 80 </description> 81 </error> 82 </method> 83 84 </interface> 85 86 <interface name="seL4_TCB" manual_name="TCB" cap_description="Capability to the TCB which is being operated on."> 87 88 <method id="TCBReadRegisters" name="ReadRegisters" manual_name="Read Registers" manual_label="tcb_readregisters"> 89 <brief> 90 Read a thread's registers into the first <texttt text="count"/> fields of a given 91 seL4_UserContext 92 </brief> 93 <description> 94 <docref>See <autoref label="sec:read_write_registers"/></docref> 95 </description> 96 <param dir="in" name="suspend_source" type="seL4_Bool" 97 description="The invocation should also suspend the source thread."/> 98 <param dir="in" name="arch_flags" type="seL4_Uint8" 99 description="Architecture dependent flags. These have no mearing on either x86 or ARM."/> 100 <param dir="in" name="count" type="seL4_Word" description="The number of registers to read."/> 101 <param dir="out" name="regs" type="seL4_UserContext" 102 description="The structure to read the registers into."/> 103 <error name="seL4_IllegalOperation"> 104 <description> 105 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 106 Or, <texttt text="_service"/> is the current thread's TCB. 107 </description> 108 </error> 109 <error name="seL4_InvalidCapability"> 110 <description> 111 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 112 </description> 113 </error> 114 <error name="seL4_RangeError"> 115 <description> 116 The <texttt text="count"/> requested too few or too many registers. 117 </description> 118 </error> 119 </method> 120 121 <method id="TCBWriteRegisters" name="WriteRegisters" manual_name="Write Registers" manual_label="tcb_writeregisters"> 122 <brief> 123 Set a thread's registers to the first <texttt text="count"/> fields of a given seL4_UserContext 124 </brief> 125 <description> 126 <docref>See <autoref label="sec:read_write_registers"/></docref> 127 </description> 128 <param dir="in" name="resume_target" type="seL4_Bool" 129 description="The invocation should also resume the destination thread."/> 130 <param dir="in" name="arch_flags" type="seL4_Uint8" 131 description="Architecture dependent flags. These have no mearing on either x86 or ARM."/> 132 <param dir="in" name="count" type="seL4_Word" 133 description="The number of registers to be set."/> 134 <param dir="in" name="regs" type="seL4_UserContext" 135 description="Data structure containing the new register values."/> 136 <error name="seL4_IllegalOperation"> 137 <description> 138 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 139 Or, <texttt text="_service"/> is the current thread's TCB. 140 </description> 141 </error> 142 <error name="seL4_InvalidCapability"> 143 <description> 144 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 145 </description> 146 </error> 147 </method> 148 149 <method id="TCBCopyRegisters" name="CopyRegisters" manual_name="Copy Registers" manual_label="tcb_copyregisters"> 150 <brief> 151 Copy the registers from one thread to another 152 </brief> 153 <description> 154 In the context of this function, frame registers are those that are read, modified or preserved by a 155 system call and integer registers are those that are not. Refer to the seL4 userland library source for specifics. 156 <docref><autoref label="sec:thread_deactivation"/></docref> 157 </description> 158 <cap_param append_description=" This is the destination TCB."/> 159 <param dir="in" name="source" type="seL4_TCB" description="Cap to the source TCB."/> 160 <param dir="in" name="suspend_source" type="seL4_Bool" 161 description="The invocation should also suspend the source thread."/> 162 <param dir="in" name="resume_target" type="seL4_Bool" 163 description="The invocation should also resume the destination thread."/> 164 <param dir="in" name="transfer_frame" type="seL4_Bool" 165 description="Frame registers should be transferred."/> 166 <param dir="in" name="transfer_integer" type="seL4_Bool" 167 description="Integer registers should be transferred."/> 168 <param dir="in" name="arch_flags" type="seL4_Uint8" 169 description="Architecture dependent flags. These have no mearing on either x86 or ARM."/> 170 <error name="seL4_IllegalOperation"> 171 <description> 172 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 173 </description> 174 </error> 175 <error name="seL4_InvalidCapability"> 176 <description> 177 The <texttt text="_service"/> or <texttt text="source"/> is a CPtr to a capability of the wrong type. 178 </description> 179 </error> 180 </method> 181 182 <method id="TCBConfigure" name="Configure" manual_name="Configure" manual_label="tcb_configure" condition="!defined(CONFIG_KERNEL_MCS)"> 183 <brief> 184 Set the parameters of a TCB 185 </brief> 186 <description> 187 <docref>See <autoref label="sec:threads"/></docref> 188 </description> 189 <param dir="in" name="fault_ep" type="seL4_Word" 190 description="CPTR to the endpoint which receives IPCs when this thread faults. This capability is in the CSpace of the thread being configured."/> 191 <param dir="in" name="cspace_root" type="seL4_CNode" 192 description="The new CSpace root."/> 193 <param dir="in" name="cspace_root_data" type="seL4_Word" 194 description="Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect."/> 195 <param dir="in" name="vspace_root" type="seL4_CPtr" 196 description="The new VSpace root."/> 197 <param dir="in" name="vspace_root_data" type="seL4_Word" 198 description="Has no effect on x86 or ARM processors."/> 199 <param dir="in" name="buffer" type="seL4_Word" 200 description="Location of the thread's IPC buffer. Must be 512-byte aligned. The IPC buffer may not cross a page boundary."/> 201 <param dir="in" name="bufferFrame" type="seL4_CPtr" 202 description="Capability to a page containing the thread's IPC buffer."/> 203 <error name="seL4_IllegalOperation"> 204 <description> 205 The <texttt text="_service"/>, <texttt text="bufferFrame"/>, <texttt text="cspace_root"/>, or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 206 Or, <texttt text="vspace_root"/> is not assigned to an ASID pool. 207 Or, <texttt text="cspace_root_data"/> is invalid. 208 Or, <texttt text="buffer"/> is not aligned. 209 Or, <texttt text="bufferFrame"/> is retyped from a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>)</docref>. 210 </description> 211 </error> 212 <error name="seL4_InvalidCapability"> 213 <description> 214 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 215 </description> 216 </error> 217 <error name="seL4_RevokeFirst"> 218 <description> 219 The <texttt text="bufferFrame"/>, <texttt text="cspace_root"/>, or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 220 </description> 221 </error> 222 </method> 223 <method id="TCBConfigure" name="Configure" manual_name="Configure (MCS)" manual_label="tcb_configure_mcs" condition="defined(CONFIG_KERNEL_MCS)"> 224 <brief> 225 Set the parameters of a TCB 226 </brief> 227 <description> 228 <docref>See <autoref label="sec:threads"/></docref> 229 </description> 230 <param dir="in" name="cspace_root" type="seL4_CNode" 231 description="The new CSpace root."/> 232 <param dir="in" name="cspace_root_data" type="seL4_Word" 233 description="Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect."/> 234 <param dir="in" name="vspace_root" type="seL4_CPtr" 235 description="The new VSpace root."/> 236 <param dir="in" name="vspace_root_data" type="seL4_Word" 237 description="Has no effect on x86 or ARM processors."/> 238 <param dir="in" name="buffer" type="seL4_Word" 239 description="Location of the thread's IPC buffer. Must be 512-byte aligned. The IPC buffer may not cross a page boundary."/> 240 <param dir="in" name="bufferFrame" type="seL4_CPtr" 241 description="Capability to a page containing the thread's IPC buffer."/> 242 <error name="seL4_AlignmentError"> 243 <description> 244 The <texttt text="buffer"/> is not aligned. 245 </description> 246 </error> 247 <error name="seL4_IllegalOperation"> 248 <description> 249 The <texttt text="_service"/>, <texttt text="bufferFrame"/>, <texttt text="cspace_root"/>, or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 250 Or, <texttt text="vspace_root"/> is not assigned to an ASID pool. 251 Or, <texttt text="cspace_root_data"/> is invalid. 252 Or, <texttt text="bufferFrame"/> is retyped from a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>)</docref>. 253 </description> 254 </error> 255 <error name="seL4_InvalidCapability"> 256 <description> 257 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 258 </description> 259 </error> 260 <error name="seL4_RevokeFirst"> 261 <description> 262 The <texttt text="bufferFrame"/>, <texttt text="cspace_root"/>, or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 263 </description> 264 </error> 265 </method> 266 267 <method id="TCBSetPriority" name="SetPriority" manual_name="Set Priority" manual_label="tcb_setpriority"> 268 <brief> 269 Change a thread's priority 270 </brief> 271 <description> 272 <docref>See <autoref label="sec:sched"/></docref> 273 </description> 274 <param dir="in" name="authority" type="seL4_TCB" 275 description="Capability to the TCB to use the MCP from when setting the priority."/> 276 <param dir="in" name="priority" type="seL4_Word" 277 description="The thread's new priority."/> 278 <error name="seL4_IllegalOperation"> 279 <description> 280 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 281 </description> 282 </error> 283 <error name="seL4_InvalidCapability"> 284 <description> 285 The <texttt text="_service"/> or <texttt text="authority"/> is a CPtr to a capability of the wrong type. 286 </description> 287 </error> 288 <error name="seL4_RangeError"> 289 <description> 290 The <texttt text="priority"/> is greater than the maximum controlled priority of <texttt text="authority"/>. 291 </description> 292 </error> 293 </method> 294 295 <method id="TCBSetMCPriority" name="SetMCPriority" manual_name="Set Maximum Controlled Priority" manual_label="tcb_setmcpriority"> 296 <brief> 297 Change a thread's maximum controlled priority 298 </brief> 299 <description> 300 <docref>See <autoref label="sec:sched"/></docref> 301 </description> 302 <param dir="in" name="authority" type="seL4_TCB" 303 description="Capability to the TCB to use the MCP from when setting the MCP."/> 304 <param dir="in" name="mcp" type="seL4_Word" 305 description="The thread's new maximum controlled priority."/> 306 <error name="seL4_IllegalOperation"> 307 <description> 308 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 309 </description> 310 </error> 311 <error name="seL4_InvalidCapability"> 312 <description> 313 The <texttt text="_service"/> or <texttt text="authority"/> is a CPtr to a capability of the wrong type. 314 </description> 315 </error> 316 <error name="seL4_RangeError"> 317 <description> 318 The <texttt text="mcp"/> is greater than the maximum controlled priority of <texttt text="authority"/>. 319 </description> 320 </error> 321 </method> 322 323 <method id="TCBSetSchedParams" name="SetSchedParams" manual_name="Set Sched Params" manual_label="tcb_setschedparams" condition="!defined(CONFIG_KERNEL_MCS)"> 324 <brief> 325 Change a thread's priority and maximum controlled priority. 326 </brief> 327 <description> 328 <docref>See <autoref label="sec:sched"/></docref> 329 </description> 330 <param dir="in" name="authority" type="seL4_TCB" 331 description="Capability to the TCB to use the MCP from when setting the priority and MCP."/> 332 <param dir="in" name="mcp" type="seL4_Word" 333 description="The thread's new maximum controlled priority."/> 334 <param dir="in" name="priority" type="seL4_Word" 335 description="The thread's new priority."/> 336 <error name="seL4_IllegalOperation"> 337 <description> 338 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 339 </description> 340 </error> 341 <error name="seL4_InvalidCapability"> 342 <description> 343 The <texttt text="_service"/> or <texttt text="authority"/> is a CPtr to a capability of the wrong type. 344 </description> 345 </error> 346 <error name="seL4_RangeError"> 347 <description> 348 The <texttt text="mcp"/> is greater than the maximum controlled priority of <texttt text="authority"/>. 349 Or, <texttt text="priority"/> is greater than the maximum controlled priority of <texttt text="authority"/>. 350 </description> 351 </error> 352 </method> 353 <method id="TCBSetSchedParams" name="SetSchedParams" manual_name="Set Sched Params (MCS)" manual_label="tcb_setschedparams_mcs" condition="defined(CONFIG_KERNEL_MCS)"> 354 <brief> 355 Change a thread's priority, maximum controlled priority, scheduling context 356 and fault handler. 357 </brief> 358 <description> 359 <docref>See <autoref label="sec:sched"/></docref> 360 </description> 361 <param dir="in" name="authority" type="seL4_TCB" 362 description="Capability to the TCB to use the MCP from when setting the priority and MCP."/> 363 <param dir="in" name="mcp" type="seL4_Word" 364 description="The thread's new maximum controlled priority."/> 365 <param dir="in" name="priority" type="seL4_Word" 366 description="The thread's new priority."/> 367 <param dir="in" name="sched_context" type="seL4_CPtr" 368 description="Capability to the scheduling context that the TCB should run on. If the scheduling context is already bound to a notification or TCB that is not this TCB this operation will fail. Similarly, if this TCB is already bound to a scheduling context that is not this scheduling context, this will also fail."/> 369 <param dir="in" name="fault_ep" type="seL4_CPtr" 370 description="CPTR to the endpoint which receives IPCs when this thread faults."/> 371 <error name="seL4_IllegalOperation"> 372 <description> 373 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 374 Or, <texttt text="_service"/> or <texttt text="sched_context"/> is already bound. 375 Or, <texttt text="_service"/> is the current thread's TCB. 376 Or, <texttt text="_service"/> is a TCB in the blocked state and <texttt text="sched_context"/> is not schedulable. 377 </description> 378 </error> 379 <error name="seL4_InvalidCapability"> 380 <description> 381 The <texttt text="_service"/>, <texttt text="authority"/>, <texttt text="sched_context"/>, or <texttt text="fault_ep"/> is a CPtr to a capability of the wrong type. 382 Or, <texttt text="fault_ep"/> does not have both Write rights and either Grant or GrantReply rights to the Endpoint <docref>(see <autoref label="sec:cap_rights"/>)</docref>. 383 </description> 384 </error> 385 <error name="seL4_RangeError"> 386 <description> 387 The <texttt text="mcp"/> is greater than the maximum controlled priority of <texttt text="authority"/>. 388 Or, <texttt text="priority"/> is greater than the maximum controlled priority of <texttt text="authority"/>. 389 </description> 390 </error> 391 </method> 392 393 <method id="TCBSetTimeoutEndpoint" name="SetTimeoutEndpoint" manual_name="Set Timeout Endpoint" manual_label="tcb_settimeoutendpoint" condition="defined(CONFIG_KERNEL_MCS)"> 394 <brief> 395 Set a thread's timeout endpoint. 396 </brief> 397 <description> 398 Timeout exception messages will be delivered to this endpoint if it is not a null capability. 399 </description> 400 <param dir="in" name="timeout_fault_ep" type="seL4_CPtr" 401 description="CPTR to the endpoint which receives IPCs when this thread triggers timeout faults. Can be null."/> 402 <error name="seL4_IllegalOperation"> 403 <description> 404 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 405 </description> 406 </error> 407 <error name="seL4_InvalidCapability"> 408 <description> 409 The <texttt text="_service"/> or <texttt text="timeout_fault_ep"/> is a CPtr to a capability of the wrong type. 410 Or, <texttt text="timeout_fault_ep"/> does not have both Write rights and either Grant or GrantReply rights to the Endpoint <docref>(see <autoref label="sec:cap_rights"/>)</docref>. 411 </description> 412 </error> 413 </method> 414 <method id="TCBSetIPCBuffer" name="SetIPCBuffer" manual_name="Set IPC Buffer" manual_label="tcb_setipcbuffer"> 415 <brief> 416 Set a thread's IPC buffer 417 </brief> 418 <description> 419 See Sections <shortref sec="threads"/> and <shortref sec="messageinfo"/> 420 </description> 421 <param dir="in" name="buffer" type="seL4_Word" 422 description="Location of the thread's IPC buffer. Must be 512-byte aligned. The IPC buffer may not cross a page boundary."/> 423 <param dir="in" name="bufferFrame" type="seL4_CPtr" 424 description="Capability to a page containing the thread's IPC buffer."/> 425 <error name="seL4_AlignmentError"> 426 <description> 427 The <texttt text="buffer"/> is not aligned. 428 </description> 429 </error> 430 <error name="seL4_IllegalOperation"> 431 <description> 432 The <texttt text="_service"/> or <texttt text="bufferFrame"/> is a CPtr to a capability of the wrong type. 433 Or, <texttt text="bufferFrame"/> is retyped from a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>)</docref>. 434 </description> 435 </error> 436 <error name="seL4_InvalidCapability"> 437 <description> 438 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 439 </description> 440 </error> 441 <error name="seL4_RevokeFirst"> 442 <description> 443 The <texttt text="bufferFrame"/> is a CPtr to a capability of the wrong type. 444 </description> 445 </error> 446 </method> 447 448 <method id="TCBSetSpace" name="SetSpace" manual_name="Set Space" manual_label="tcb_setspace" condition="!defined(CONFIG_KERNEL_MCS)"> 449 <brief> 450 Set the fault endpoint, CSpace and VSpace of a thread 451 </brief> 452 <description> 453 <docref>See <autoref label="sec:threads"/></docref> 454 </description> 455 <param dir="in" name="fault_ep" type="seL4_Word" 456 description="CPTR to the endpoint which receives IPCs when this thread faults. This capability is in the CSpace of the thread being configured."/> 457 <param dir="in" name="cspace_root" type="seL4_CNode" 458 description="The new CSpace root."/> 459 <param dir="in" name="cspace_root_data" type="seL4_Word" 460 description="Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect."/> 461 <param dir="in" name="vspace_root" type="seL4_CPtr" 462 description="The new VSpace root."/> 463 <param dir="in" name="vspace_root_data" type="seL4_Word" 464 description="Has no effect on x86 or ARM processors."/> 465 <error name="seL4_IllegalOperation"> 466 <description> 467 The <texttt text="_service"/>, <texttt text="cspace_root"/>, or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 468 Or, <texttt text="vspace_root"/> is not assigned to an ASID pool. 469 Or, <texttt text="cspace_root_data"/> is invalid. 470 </description> 471 </error> 472 <error name="seL4_InvalidCapability"> 473 <description> 474 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 475 </description> 476 </error> 477 <error name="seL4_RevokeFirst"> 478 <description> 479 The <texttt text="cspace_root"/> or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 480 </description> 481 </error> 482 </method> 483 484 <method id="TCBSetSpace" name="SetSpace" manual_name="Set Space" manual_label="tcb_setspace_mcs" condition="defined(CONFIG_KERNEL_MCS)"> 485 <brief> 486 Set the fault endpoint, CSpace and VSpace of a thread 487 </brief> 488 <description> 489 <docref>See <autoref label="sec:threads"/></docref> 490 </description> 491 <param dir="in" name="fault_ep" type="seL4_CPtr" 492 description="CPTR to the endpoint which receives IPCs when this thread faults. On MCS this cap gets copied into the TCB."/> 493 <param dir="in" name="cspace_root" type="seL4_CNode" 494 description="The new CSpace root."/> 495 <param dir="in" name="cspace_root_data" type="seL4_Word" 496 description="Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect."/> 497 <param dir="in" name="vspace_root" type="seL4_CPtr" 498 description="The new VSpace root."/> 499 <param dir="in" name="vspace_root_data" type="seL4_Word" 500 description="Has no effect on x86 or ARM processors."/> 501 <error name="seL4_IllegalOperation"> 502 <description> 503 The <texttt text="_service"/>, <texttt text="cspace_root"/>, or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 504 Or, <texttt text="vspace_root"/> is not assigned to an ASID pool. 505 Or, <texttt text="cspace_root_data"/> is invalid. 506 </description> 507 </error> 508 <error name="seL4_InvalidCapability"> 509 <description> 510 The <texttt text="_service"/> or <texttt text="fault_ep"/> is a CPtr to a capability of the wrong type. 511 Or, <texttt text="fault_ep"/> does not have both Write rights and either Grant or GrantReply rights to the Endpoint <docref>(see <autoref label="sec:cap_rights"/>)</docref>. 512 </description> 513 </error> 514 <error name="seL4_RevokeFirst"> 515 <description> 516 The <texttt text="cspace_root"/> or <texttt text="vspace_root"/> is a CPtr to a capability of the wrong type. 517 </description> 518 </error> 519 </method> 520 521 <method id="TCBSuspend" name="Suspend" manual_name="Suspend" manual_label="tcb_suspend"> 522 <brief> 523 Suspend a thread 524 </brief> 525 <description> 526 <docref>See <autoref label="sec:thread_deactivation"/></docref> 527 </description> 528 <error name="seL4_IllegalOperation"> 529 <description> 530 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 531 </description> 532 </error> 533 <error name="seL4_InvalidCapability"> 534 <description> 535 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 536 </description> 537 </error> 538 </method> 539 540 <method id="TCBResume" name="Resume" manual_name="Resume" manual_label="tcb_resume"> 541 <brief> 542 Resume a thread 543 </brief> 544 <description> 545 <docref>See <autoref label="sec:thread_deactivation"/></docref> 546 </description> 547 <error name="seL4_IllegalOperation"> 548 <description> 549 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 550 </description> 551 </error> 552 <error name="seL4_InvalidCapability"> 553 <description> 554 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 555 </description> 556 </error> 557 </method> 558 559 <method id="TCBBindNotification" name="BindNotification" manual_name="Bind Notification" manual_label="tcb_bindnotification"> 560 <brief> 561 Binds a notification object to a <obj name="TCB"/> 562 </brief> 563 <description> 564 <docref>See <autoref label="sec:notification-binding"/></docref> 565 </description> 566 <param dir="in" name="notification" type="seL4_CPtr" description="Notification to bind."/> 567 <error name="seL4_IllegalOperation"> 568 <description> 569 The <texttt text="_service"/> or <texttt text="notification"/> is a CPtr to a capability of the wrong type. 570 Or, <texttt text="_service"/> or <texttt text="notification"/> is already bound. 571 Or, <texttt text="notification"/> does not have Read rights to the Notification <docref>(see <autoref label="sec:cap_rights"/>)</docref>. 572 </description> 573 </error> 574 <error name="seL4_InvalidCapability"> 575 <description> 576 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 577 </description> 578 </error> 579 </method> 580 581 <method id="TCBUnbindNotification" name="UnbindNotification" manual_name="Unbind Notification" manual_label="tcb_unbindnotification"> 582 <brief> 583 Unbinds any notification object from a <obj name="TCB"/> 584 </brief> 585 <description> 586 <docref>See <autoref label="sec:notification-binding"/></docref> 587 </description> 588 <error name="seL4_IllegalOperation"> 589 <description> 590 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 591 Or, <texttt text="_service"/> is not bound to a notification. 592 </description> 593 </error> 594 <error name="seL4_InvalidCapability"> 595 <description> 596 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 597 </description> 598 </error> 599 </method> 600 601 <method id="TCBSetAffinity" name="SetAffinity" condition="(!defined CONFIG_KERNEL_MCS) && CONFIG_MAX_NUM_NODES > 1" manual_name="Set CPU Affinity" manual_label="tcb_setaffinity"> 602 <brief> 603 Change a thread's current CPU in multicore machine 604 </brief> 605 <description> 606 <docref>See <autoref label="sec:thread_creation"/></docref> 607 </description> 608 <param dir="in" name="affinity" type="seL4_Word" 609 description="The thread's new CPU to run."/> 610 <error name="seL4_IllegalOperation"> 611 <description> 612 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 613 Or, <texttt text="affinity"/> is not a valid CPU number. 614 </description> 615 </error> 616 <error name="seL4_InvalidCapability"> 617 <description> 618 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 619 </description> 620 </error> 621 </method> 622 623 <method id="TCBSetBreakpoint" name="SetBreakpoint" condition="defined(CONFIG_HARDWARE_DEBUG_API)" manual_name="Set Breakpoint" manual_label="tcb_setbreakpoint"> 624 <brief> 625 Set or modify a thread's breakpoints or watchpoints. Calls to this function 626 overwrite previous configurations for the target breakpoint. Do not use this 627 with seL4_SingleStep: the API will reject the call and return an error. 628 Instead, use seL4_TCB_ConfigureSingleStepping to configure single-stepping. 629 </brief> 630 <description> 631 <docref>See <autoref label="sec:debug_exceptions"/></docref> 632 </description> 633 <param dir="in" name="bp_num" type="seL4_Uint16" 634 description="The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1."/> 635 <param dir="in" name="vaddr" type="seL4_Word" 636 description="A virtual address which forms part of the match conditions for the triggering of the breakpoint."/> 637 <param dir="in" name="type" type="seL4_Word" 638 description="One of: seL4_InstructionBreakpoint, which specifies that the breakpoint should occur on instruction execution at the specified vaddr or seL4_DataBreakpoint, which states that the breakpoint should occur on data access at the specified vaddr."/> 639 <param dir="in" name="size" type="seL4_Word" 640 description="A positive integer indicating the trigger-span of the watchpoint. Must be zero when 'type' is seL4_InstructionBreakpoint."/> 641 <param dir="in" name="rw" type="seL4_Word" 642 description="One of seL4_BreakOnRead, meaning the breakpoint will only be triggered on read-access; seL4_BreakOnWrite meaning the breakpoint will only be triggered on write-access, and seL4_BreakOnReadWrite meaning the breakpoint will be triggered on any access."/> 643 <error name="seL4_AlignmentError"> 644 <description> 645 The <texttt text="vaddr"/> is not aligned to <texttt text="size"/> bytes. 646 </description> 647 </error> 648 <error name="seL4_IllegalOperation"> 649 <description> 650 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 651 </description> 652 </error> 653 <error name="seL4_InvalidArgument"> 654 <description> 655 The <texttt text="bp_num"/>, <texttt text="size"/>, or <texttt text="rw"/> is not valid for the given <texttt text="type"/>. 656 Or, argument values are inappropriate for the target architecture. 657 Or, <texttt text="vaddr"/> is in the kernel virtual address range. 658 </description> 659 </error> 660 <error name="seL4_InvalidCapability"> 661 <description> 662 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 663 </description> 664 </error> 665 <error name="seL4_RangeError"> 666 <description> 667 The argument values are inappropriate for the target architecture. 668 </description> 669 </error> 670 </method> 671 672 <method id="TCBGetBreakpoint" name="GetBreakpoint" condition="defined(CONFIG_HARDWARE_DEBUG_API)" manual_name="Get Breakpoint" manual_label="tcb_getbreakpoint"> 673 <brief> 674 Read a breakpoint or watchpoint's current configuration. 675 </brief> 676 <description> 677 <docref>See <autoref label="sec:debug_exceptions"/></docref> 678 </description> 679 <return> 680 A <texttt text="seL4_TCB_GetBreakpoint_t"/>: Struct that contains 681 <texttt text="seL4_Error error"/>, an seL4 API error value, 682 <texttt text="seL4_Word vaddr"/>, the virtual address at which the breakpoint will currently 683 be triggered; 684 <texttt text="seL4_Word type"/>, the type of operation which will currently trigger the 685 breakpoint, whether instruction execution, or data access; 686 <texttt text="seL4_Word size"/>, integer value for the span-size of the breakpoint. 687 Usually a power of two (1, 2, 4, etc.); 688 <texttt text="seL4_Word rw"/>, the access direction that will currently trigger the breakpoint, 689 whether read, write, or both and 690 <texttt text="seL4_Bool is_enabled"/>, which indicates whether or not the breakpoint 691 will currently be triggered if the match conditions are met. 692 </return> 693 <param dir="in" name="bp_num" type="seL4_Uint16" 694 description="The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1."/> 695 <param dir="out" name="vaddr" type="seL4_Word"/> 696 <param dir="out" name="type" type="seL4_Word"/> 697 <param dir="out" name="size" type="seL4_Word"/> 698 <param dir="out" name="rw" type="seL4_Word"/> 699 <param dir="out" name="is_enabled" type="seL4_Bool"/> 700 <error name="seL4_IllegalOperation"> 701 <description> 702 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 703 </description> 704 </error> 705 <error name="seL4_InvalidCapability"> 706 <description> 707 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 708 </description> 709 </error> 710 <error name="seL4_RangeError"> 711 <description> 712 The argument values are inappropriate for the target architecture. 713 </description> 714 </error> 715 </method> 716 717 <method id="TCBUnsetBreakpoint" name="UnsetBreakpoint" condition="defined(CONFIG_HARDWARE_DEBUG_API)" manual_name="Unset Breakpoint" manual_label="tcb_unsetbreakpoint"> 718 <brief> 719 Disables a hardware breakpoint or watchpoint. The caller should assume that 720 the underlying configuration of the hardware registers has also been cleared. 721 Do not use this to clear single-stepping: the API will reject the call and 722 return an error. Instead, use seL4_TCB_ConfigureSingleStepping to disable 723 single-stepping. 724 </brief> 725 <description> 726 <docref>See <autoref label="sec:debug_exceptions"/></docref> 727 </description> 728 <param dir="in" name="bp_num" type="seL4_Uint16" 729 description="The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1."/> 730 <error name="seL4_IllegalOperation"> 731 <description> 732 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 733 Or, the argument values are inappropriate for the target architecture. 734 </description> 735 </error> 736 <error name="seL4_InvalidCapability"> 737 <description> 738 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 739 </description> 740 </error> 741 <error name="seL4_RangeError"> 742 <description> 743 The argument values are inappropriate for the target architecture. 744 </description> 745 </error> 746 </method> 747 748 <method id="TCBConfigureSingleStepping" name="ConfigureSingleStepping" condition="defined(CONFIG_HARDWARE_DEBUG_API)" 749 manual_name="Configure Single Stepping" manual_label="tcb_configuresinglestepping"> 750 <brief> 751 Set or modify single stepping options for the target TCB. Subsequent calls to this 752 function overwrite previous configuration. Depending on your processor architecture, 753 this may or may not require the consumption of a hardware register. 754 </brief> 755 <description> 756 <docref>See Sections <shortref sec="single_stepping_debug_exception"/> and <shortref sec="debug_exceptions"/></docref> 757 </description> 758 <return> 759 A <texttt text="seL4_TCB_ConfigureSingleStepping_t"/>: Struct that contains 760 <texttt text="seL4_Error error"/>, an seL4 API error value, 761 <texttt text="seL4_Bool bp_was_consumed"/>, a boolean which indicates whether or not the <texttt text="bp_num"/> 762 breakpoint ID that was passed to the function, was consumed in the setup of the single-stepping 763 functionality: if this is <texttt text="true"/>, the caller should not attempt to re-use <texttt text="bp_num"/> 764 until it has disabled the single-stepping functionality via a subsequent call to 765 seL4_TCB_ConfigureSingleStepping with an <texttt text="num_instructions"/> argument of 0. 766 </return> 767 <param dir="in" name="bp_num" type="seL4_Uint16" 768 description="The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1."/> 769 <param dir="in" name="num_instructions" type="seL4_Word" 770 description="Number of instructions to step over before delivering a fault to the target thread's fault endpoint. Setting this to 0 disables single-stepping."/> 771 <param dir="out" name="bp_was_consumed" type="seL4_Bool"/> 772 <error name="seL4_IllegalOperation"> 773 <description> 774 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 775 Or, the argument values are inappropriate for the target architecture. 776 </description> 777 </error> 778 <error name="seL4_InvalidArgument"> 779 <description> 780 The argument values are inappropriate for the target architecture. 781 </description> 782 </error> 783 <error name="seL4_InvalidCapability"> 784 <description> 785 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 786 </description> 787 </error> 788 </method> 789 790 <method id="TCBSetTLSBase" name="SetTLSBase" manual_name="Set TLS Base" manual_label="tcb_settlsbase"> 791 <brief> 792 Set the TLS base of the target TCB. This intended for use on architectures where the register 793 used for TLS can only be written to in privilidged mode 794 </brief> 795 <description> 796 </description> 797 <return> 798 </return> 799 <param dir="in" name="tls_base" type="seL4_Word" 800 description="The TLS base to set"/> 801 <error name="seL4_IllegalOperation"> 802 <description> 803 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 804 </description> 805 </error> 806 <error name="seL4_InvalidCapability"> 807 <description> 808 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 809 </description> 810 </error> 811 </method> 812 813 </interface> 814 815 <interface name="seL4_CNode" manual_name="CNode"> 816 <method id="CNodeRevoke" name="Revoke" manual_name="Revoke" manual_label="cnode_revoke"> 817 <brief> 818 Delete all child capabilities of a capability 819 </brief> 820 <description> 821 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 822 </description> 823 <cap_param append_description="CPTR to the CNode at the root of the CSpace where the capability will be found. Must be at a depth equivalent to the wordsize."/> 824 <param dir="in" name="index" type="seL4_Word" description="CPTR to the capability. Resolved from the root of the _service parameter."/> 825 <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of index to resolve to find the capability being operated on."/> 826 <error name="seL4_FailedLookup"> 827 <description> 828 The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 829 </description> 830 </error> 831 <error name="seL4_IllegalOperation"> 832 <description> 833 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 834 </description> 835 </error> 836 <error name="seL4_InvalidCapability"> 837 <description> 838 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 839 </description> 840 </error> 841 <error name="seL4_RangeError"> 842 <description> 843 The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 844 </description> 845 </error> 846 </method> 847 848 <method id="CNodeDelete" name="Delete" manual_name="Delete" manual_label="cnode_delete"> 849 <brief> 850 Delete a capability 851 </brief> 852 <description> 853 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 854 </description> 855 <cap_param append_description="CPTR to the CNode at the root of the CSpace where the capability will be found. Must be at a depth equivalent to the wordsize."/> 856 <param dir="in" name="index" type="seL4_Word" description="CPTR to the capability. Resolved from the root of the _service parameter."/> 857 <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of index to resolve to find the capability being operated on."/> 858 <error name="seL4_FailedLookup"> 859 <description> 860 The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 861 </description> 862 </error> 863 <error name="seL4_IllegalOperation"> 864 <description> 865 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 866 </description> 867 </error> 868 <error name="seL4_InvalidCapability"> 869 <description> 870 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 871 </description> 872 </error> 873 <error name="seL4_RangeError"> 874 <description> 875 The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 876 </description> 877 </error> 878 </method> 879 880 <method id="CNodeCancelBadgedSends" name="CancelBadgedSends" manual_name="Cancel Badged Sends" manual_label="cnode_cancelbadgedsends"> 881 <brief> 882 The cancel badged sends method is intend to allow for the reuse of badges by an 883 authority. When used with a badged endpoint capability it 884 will cancel any outstanding send operations for that endpoint and badge. 885 This operation has no effect on un-badged or other objects. 886 </brief> 887 <description> 888 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 889 </description> 890 <cap_param append_description="CPTR to the CNode at the root of the CSpace where the capability will be found. Must be at a depth equivalent to the wordsize."/> 891 <param dir="in" name="index" type="seL4_Word" description="CPTR to the capability. Resolved from the root of the _service parameter."/> 892 <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of index to resolve to find the capability being operated on."/> 893 <error name="seL4_FailedLookup"> 894 <description> 895 The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 896 </description> 897 </error> 898 <error name="seL4_IllegalOperation"> 899 <description> 900 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 901 Or, the capability does not have full rights to the Endpoint <docref>(see <autoref label="sec:cap_rights"/>)</docref>. 902 </description> 903 </error> 904 <error name="seL4_InvalidCapability"> 905 <description> 906 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 907 </description> 908 </error> 909 <error name="seL4_RangeError"> 910 <description> 911 The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 912 </description> 913 </error> 914 </method> 915 916 <method id="CNodeCopy" name="Copy" manual_name="Copy" manual_label="cnode_copy"> 917 <brief> 918 Copy a capability, setting its access rights whilst doing so 919 </brief> 920 <description> 921 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 922 </description> 923 <cap_param append_description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/> 924 <param dir="in" name="dest_index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/> 925 <param dir="in" name="dest_depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/> 926 <param dir="in" name="src_root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the source CSpace. Must be at a depth equivalent to the wordsize."/> 927 <param dir="in" name="src_index" type="seL4_Word" description="CPTR to the source slot. Resolved from the root of the source CSpace."/> 928 <param dir="in" name="src_depth" type="seL4_Uint8" description="Number of bits of src_index to resolve to find the source slot."/> 929 <param dir="in" name="rights" type="seL4_CapRights_t"> 930 <description> 931 The rights inherited by the new capability.<docref>Possible values for this type are given in <autoref label="sec:cap_rights"/> .</docref> 932 </description> 933 </param> 934 <error name="seL4_DeleteFirst" description="The destination slot contains a capability."/> 935 <error name="seL4_FailedLookup"> 936 <description> 937 The index or depth of the source or destination is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 938 Or, <texttt text="src_root"/> is a CPtr to a capability of the wrong type. 939 Or, the source slot is empty. 940 </description> 941 </error> 942 <error name="seL4_IllegalOperation"> 943 <description> 944 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 945 Or, the source capability cannot be derived <docref>(see <autoref label="sec:cap_derivation"/>)</docref>. 946 </description> 947 </error> 948 <error name="seL4_InvalidCapability"> 949 <description> 950 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 951 </description> 952 </error> 953 <error name="seL4_RangeError"> 954 <description> 955 The <texttt text="dest_depth"/> or <texttt text="src_depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 956 </description> 957 </error> 958 <error name="seL4_RevokeFirst"> 959 <description> 960 The source capability cannot be derived <docref>(see <autoref label="sec:cap_derivation"/>)</docref>. 961 </description> 962 </error> 963 </method> 964 965 <method id="CNodeMint" name="Mint" manual_name="Mint" manual_label="cnode_mint"> 966 <brief> 967 Copy a capability, setting its access rights and badge whilst doing so 968 </brief> 969 <description> 970 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 971 </description> 972 <cap_param append_description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/> 973 <param dir="in" name="dest_index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/> 974 <param dir="in" name="dest_depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/> 975 <param dir="in" name="src_root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the source CSpace. Must be at a depth equivalent to the wordsize."/> 976 <param dir="in" name="src_index" type="seL4_Word" description="CPTR to the source slot. Resolved from the root of the source CSpace."/> 977 <param dir="in" name="src_depth" type="seL4_Uint8" description="Number of bits of src_index to resolve to find the source slot."/> 978 <param dir="in" name="rights" type="seL4_CapRights_t"> 979 <description> 980 The rights inherited by the new capability.<docref>Possible values for this type are given in <autoref label="sec:cap_rights"/> .</docref> 981 </description> 982 </param> 983 <param dir="in" name="badge" type="seL4_Word" description="Badge or guard to be applied to the new capability. For badges on 32-bit platforms, the high 4 bits are ignored."/> 984 <error name="seL4_DeleteFirst" description="The destination slot contains a capability."/> 985 <error name="seL4_FailedLookup"> 986 <description> 987 The index or depth of the source or destination is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 988 Or, <texttt text="src_root"/> is a CPtr to a capability of the wrong type. 989 Or, the source slot is empty. 990 </description> 991 </error> 992 <error name="seL4_IllegalOperation"> 993 <description> 994 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 995 Or, the source capability cannot be derived <docref>(see <autoref label="sec:cap_derivation"/>)</docref>. 996 Or, the badge or guard value is invalid. 997 </description> 998 </error> 999 <error name="seL4_InvalidCapability"> 1000 <description> 1001 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1002 </description> 1003 </error> 1004 <error name="seL4_RangeError"> 1005 <description> 1006 The <texttt text="dest_depth"/> or <texttt text="src_depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1007 </description> 1008 </error> 1009 <error name="seL4_RevokeFirst"> 1010 <description> 1011 The source capability cannot be derived <docref>(see <autoref label="sec:cap_derivation"/>)</docref>. 1012 </description> 1013 </error> 1014 </method> 1015 1016 <method id="CNodeMove" name="Move" manual_name="Move" manual_label="cnode_move"> 1017 <brief> 1018 Move a capability 1019 </brief> 1020 <description> 1021 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 1022 </description> 1023 <cap_param append_description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/> 1024 <param dir="in" name="dest_index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/> 1025 <param dir="in" name="dest_depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/> 1026 <param dir="in" name="src_root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the source CSpace. Must be at a depth equivalent to the wordsize."/> 1027 <param dir="in" name="src_index" type="seL4_Word" description="CPTR to the source slot. Resolved from the root of the source CSpace."/> 1028 <param dir="in" name="src_depth" type="seL4_Uint8" description="Number of bits of src_index to resolve to find the source slot."/> 1029 <error name="seL4_DeleteFirst" description="The destination slot contains a capability."/> 1030 <error name="seL4_FailedLookup"> 1031 <description> 1032 The index or depth of the source or destination is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1033 Or, <texttt text="src_root"/> is a CPtr to a capability of the wrong type. 1034 Or, the source slot is empty. 1035 </description> 1036 </error> 1037 <error name="seL4_IllegalOperation"> 1038 <description> 1039 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1040 </description> 1041 </error> 1042 <error name="seL4_InvalidCapability"> 1043 <description> 1044 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1045 </description> 1046 </error> 1047 <error name="seL4_RangeError"> 1048 <description> 1049 The <texttt text="dest_depth"/> or <texttt text="src_depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1050 </description> 1051 </error> 1052 </method> 1053 1054 <method id="CNodeMutate" name="Mutate" manual_name="Mutate" manual_label="cnode_mutate"> 1055 <brief> 1056 Move a capability, setting its guard in the process. This 1057 operation is mostly useful for setting the guard of a CNode 1058 capability without losing revokability of that CNode capability. 1059 All other uses can be replaced by a combination of Mint and 1060 Delete. 1061 </brief> 1062 <description> 1063 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 1064 </description> 1065 <cap_param append_description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/> 1066 <param dir="in" name="dest_index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/> 1067 <param dir="in" name="dest_depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/> 1068 <param dir="in" name="src_root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the source CSpace. Must be at a depth equivalent to the wordsize."/> 1069 <param dir="in" name="src_index" type="seL4_Word" description="CPTR to the source slot. Resolved from the root of the source CSpace."/> 1070 <param dir="in" name="src_depth" type="seL4_Uint8" description="Number of bits of src_index to resolve to find the source slot."/> 1071 <param dir="in" name="badge" type="seL4_Word" description="Guard to be applied to the new capability."/> 1072 <error name="seL4_DeleteFirst" description="The destination slot contains a capability."/> 1073 <error name="seL4_FailedLookup"> 1074 <description> 1075 The index or depth of the source or destination is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1076 Or, <texttt text="src_root"/> is a CPtr to a capability of the wrong type. 1077 Or, the source slot is empty. 1078 </description> 1079 </error> 1080 <error name="seL4_IllegalOperation"> 1081 <description> 1082 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1083 Or, the guard value is invalid. 1084 </description> 1085 </error> 1086 <error name="seL4_InvalidCapability"> 1087 <description> 1088 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1089 </description> 1090 </error> 1091 <error name="seL4_RangeError"> 1092 <description> 1093 The <texttt text="dest_depth"/> or <texttt text="src_depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1094 </description> 1095 </error> 1096 </method> 1097 1098 <method id="CNodeRotate" name="Rotate" manual_name="Rotate" manual_label="cnode_rotate"> 1099 <brief> 1100 Given 3 capability slots - a destination, pivot and source - move the capability in the 1101 pivot slot to the destination slot and the capability in the source slot to the pivot slot 1102 </brief> 1103 <description> 1104 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 1105 </description> 1106 <cap_param append_description="CPTR to the CNode at the root of the CSpace where the destination slot will be found. Must be at a depth equivalent to the wordsize."/> 1107 <param dir="in" name="dest_index" type="seL4_Word" description="CPTR to the destination slot. Resolved relative to _service. Must be empty unless it refers to the same slot as the source slot."/> 1108 <param dir="in" name="dest_depth" type="seL4_Uint8" description="Depth to resolve dest_index to."/> 1109 <param dir="in" name="dest_badge" type="seL4_Word" description="The new capdata for the capability that ends up in the destination slot."/> 1110 <param dir="in" name="pivot_root" type="seL4_CNode" description="CPTR to the CNode at the root of the CSpace where the pivot slot will be found. Must be at a depth equivalent to the wordsize."/> 1111 <param dir="in" name="pivot_index" type="seL4_Word" description="CPTR to the pivot slot. Resolved relative to pivot_root. The resolved slot must not refer to the source or destination slots."/> 1112 <param dir="in" name="pivot_depth" type="seL4_Uint8" description="Depth to resolve pivot_index to."/> 1113 <param dir="in" name="pivot_badge" type="seL4_Word" description="The new capdata for the capability that ends up in the pivot slot."/> 1114 <param dir="in" name="src_root" type="seL4_CNode" description="CPTR to the CNode at the root of the CSpace where the source slot will be found. Must be at a depth equivalent to the wordsize."/> 1115 <param dir="in" name="src_index" type="seL4_Word" description="CPTR to the source slot. Resolved relative to src_root."/> 1116 <param dir="in" name="src_depth" type="seL4_Uint8" description="Depth to resolve src_index to."/> 1117 <error name="seL4_DeleteFirst" description="If the destination is not the same slot as the source and the destination slot contains a capability."/> 1118 <error name="seL4_FailedLookup"> 1119 <description> 1120 The index or depth of the source, destination, or pivot is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1121 Or, <texttt text="src_root"/> or <texttt text="pivot_root"/> is a CPtr to a capability of the wrong type. 1122 Or, the source or pivot slot is empty. 1123 </description> 1124 </error> 1125 <error name="seL4_IllegalOperation"> 1126 <description> 1127 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1128 Or, the pivot is the same slot as the source or destination. 1129 Or, the guard value on the destination or pivot is invalid. 1130 </description> 1131 </error> 1132 <error name="seL4_InvalidCapability"> 1133 <description> 1134 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1135 </description> 1136 </error> 1137 <error name="seL4_RangeError"> 1138 <description> 1139 The <texttt text="dest_depth"/>, <texttt text="src_depth"/>, or <texttt text="pivot_depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1140 </description> 1141 </error> 1142 </method> 1143 1144 <method id="CNodeSaveCaller" name="SaveCaller" manual_name="Save Caller" manual_label="cnode_savecaller" condition="!defined(CONFIG_KERNEL_MCS)"> 1145 <brief> 1146 Save the reply capability from the last time the thread was called in the given CSpace so that it can be invoked later 1147 </brief> 1148 <description> 1149 <docref>See <autoref label="sec:cnode-ops"/>.</docref> 1150 </description> 1151 <cap_param append_description="CPTR to the CNode at the root of the CSpace where the capability is to be saved. Must be at a depth equivalent to the wordsize."/> 1152 <param dir="in" name="index" type="seL4_Word" description="CPTR to the slot in which to save the capability. Resolved from the root of the _service parameter."/> 1153 <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of index to resolve to find the slot being targeted."/> 1154 <error name="seL4_DeleteFirst" description="The destination slot contains a capability."/> 1155 <error name="seL4_FailedLookup"> 1156 <description> 1157 The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1158 </description> 1159 </error> 1160 <error name="seL4_IllegalOperation"> 1161 <description> 1162 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1163 </description> 1164 </error> 1165 <error name="seL4_InvalidCapability"> 1166 <description> 1167 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1168 </description> 1169 </error> 1170 <error name="seL4_RangeError"> 1171 <description> 1172 The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1173 </description> 1174 </error> 1175 </method> 1176 1177 </interface> 1178 1179 <interface name="seL4_IRQControl" manual_name="IRQ Control" cap_description="An IRQControl capability. This gives you the authority to make this call."> 1180 1181 <method id="IRQIssueIRQHandler" name="Get" manual_name="Get" manual_label="irq_controlget"> 1182 <brief> 1183 Create an IRQ handler capability 1184 </brief> 1185 <description> 1186 <docref>See <autoref label="sec:interrupts"/>.</docref> 1187 </description> 1188 <param dir="in" name="irq" type="seL4_Word" description="The IRQ that you want this capability to handle."/> 1189 <param dir="in" name="root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/> 1190 <param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/> 1191 <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/> 1192 <error name="seL4_DeleteFirst" description="The destination slot contains a capability."/> 1193 <error name="seL4_FailedLookup"> 1194 <description> 1195 The <texttt text="root"/>, <texttt text="index"/>, or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1196 </description> 1197 </error> 1198 <error name="seL4_IllegalOperation"> 1199 <description> 1200 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1201 Or, on x86, an IOAPIC is being used. 1202 </description> 1203 </error> 1204 <error name="seL4_InvalidCapability"> 1205 <description> 1206 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1207 </description> 1208 </error> 1209 <error name="seL4_RangeError"> 1210 <description> 1211 The <texttt text="irq"/> is invalid for the target architecture. 1212 Or, on x86, <texttt text="irq"/> is not in the ISA IRQ range. 1213 Or, <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>. 1214 </description> 1215 </error> 1216 <error name="seL4_RevokeFirst"> 1217 <description> 1218 An IRQ handler capability for <texttt text="irq"/> has already been created. 1219 </description> 1220 </error> 1221 </method> 1222 1223 </interface> 1224 1225 <interface name="seL4_IRQHandler" manual_name="IRQ Handler" cap_description="The IRQ handler capability."> 1226 1227 <method id="IRQAckIRQ" name="Ack" manual_name="Acknowledge" manual_label="irq_handleracknowledge"> 1228 <brief> 1229 Acknowledge the receipt of an interrupt and re-enable it 1230 </brief> 1231 <description> 1232 <docref>See <autoref label="sec:interrupts"/>.</docref> 1233 </description> 1234 <error name="seL4_IllegalOperation"> 1235 <description> 1236 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1237 </description> 1238 </error> 1239 <error name="seL4_InvalidCapability"> 1240 <description> 1241 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1242 </description> 1243 </error> 1244 </method> 1245 1246 <method id="IRQSetIRQHandler" name="SetNotification" manual_name="Set Notification" manual_label="irq_handlersetnotification"> 1247 <brief> 1248 Set the notification which the kernel will signal on interrupts 1249 controlled by the supplied IRQ handler capability 1250 </brief> 1251 <description> 1252 <docref>See <autoref label="sec:interrupts"/>.</docref> 1253 </description> 1254 <param dir="in" name="notification" type="seL4_CPtr" description="The notification which the IRQs will signal."/> 1255 <error name="seL4_IllegalOperation"> 1256 <description> 1257 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1258 </description> 1259 </error> 1260 <error name="seL4_InvalidCapability"> 1261 <description> 1262 The <texttt text="_service"/> or <texttt text="notification"/> is a CPtr to a capability of the wrong type. 1263 Or, <texttt text="notification"/> does not have the Write right <docref>(see <autoref label="sec:cap_rights"/>)</docref>. 1264 </description> 1265 </error> 1266 </method> 1267 1268 <method id="IRQClearIRQHandler" name="Clear" manual_name="Clear" manual_label="irq_handlerclear"> 1269 <brief> 1270 Clear the handler capability from the IRQ slot 1271 </brief> 1272 <description> 1273 <docref>See <autoref label="sec:interrupts"/>.</docref> 1274 </description> 1275 <error name="seL4_IllegalOperation"> 1276 <description> 1277 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1278 </description> 1279 </error> 1280 <error name="seL4_InvalidCapability"> 1281 <description> 1282 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1283 </description> 1284 </error> 1285 </method> 1286 1287 </interface> 1288 1289 <interface name="seL4_DomainSet" manual_name="Domain Set" cap_description="Capability allowing domain configuration."> 1290 1291 <method id="DomainSetSet" name="Set" manual_name="Set" manual_label="domainset_set"> 1292 <brief> 1293 Change the domain of a thread. 1294 </brief> 1295 <description> 1296 <docref>See <autoref label="sec:domains"/>.</docref> 1297 </description> 1298 <param dir="in" name="domain" type="seL4_Uint8" description="The thread's new domain."/> 1299 <param dir="in" name="thread" type="seL4_TCB" description="Capability to the TCB which is being operated on."/> 1300 <error name="seL4_IllegalOperation"> 1301 <description> 1302 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1303 </description> 1304 </error> 1305 <error name="seL4_InvalidArgument"> 1306 <description> 1307 The <texttt text="domain"/> is greater than <texttt text="CONFIG_NUM_DOMAINS"/>. 1308 Or, <texttt text="thread"/> is a CPtr to a capability of the wrong type. 1309 </description> 1310 </error> 1311 <error name="seL4_InvalidCapability"> 1312 <description> 1313 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1314 </description> 1315 </error> 1316 </method> 1317 </interface> 1318 1319 <interface name="seL4_SchedControl"> 1320 1321 <method id="SchedControlConfigureFlags" name="ConfigureFlags" manual_name="ConfigureFlags" manual_label="schedcontrol_configureflags" condition="defined(CONFIG_KERNEL_MCS)"> 1322 <brief> 1323 Set the parameters of a scheduling context by invoking the scheduling control capability. If the scheduling context is bound to a currently running thread, the parameters will take effect immediately: that is the current budget will be increased or reduced by the difference between the new and previous budget and the replenishment time will be updated according to any difference in the period. This can result in active threads being post-poned or released depending on the nature of the parameter change and the state of the thread. Additionally, if the scheduling context was previously empty (no budget) but bound to a runnable thread, this can result in a thread running for the first time since it now has access to CPU time. This call will return seL4 Invalid Argument if the parameters are too small (smaller than the kernel WCET for this platform) or too large (will overflow the timer). 1324 </brief> 1325 <description> 1326 See <autoref label="sec:threads"/> 1327 </description> 1328 <return><errorenumdesc/></return> 1329 <param dir="in" name="schedcontext" type="seL4_SchedContext" 1330 description="Capability to the scheduling context which is being operated on."/> 1331 <param dir="in" name="budget" type="seL4_Time" 1332 description="Timeslice in microseconds, when the budget expires the thread will be pre-empted."/> 1333 <param dir="in" name="period" type="seL4_Time" 1334 description="Period in microseconds, if equal to budget, this thread will be treated as a round-robin thread. Otherwise, sporadic servers will be used to assure the scheduling context does not exceed the budget over the specified period."/> 1335 <param dir="in" name="extra_refills" type="seL4_Word" 1336 description="Number of extra sporadic replenishments this scheduling context should use. Ignored for round-robin threads."/> 1337 <param dir="in" name="badge" type="seL4_Word" 1338 description="Identifier for this scheduling context. Delivered to timeout exception handler. Can be used to determine which scheduling context triggered the timeout." /> 1339 <param dir="in" name="flags" type="seL4_Word" 1340 description="Bitwise OR'd set of seL4_SchedContextFlag." /> 1341 <error name="seL4_IllegalOperation"> 1342 <description> 1343 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1344 </description> 1345 </error> 1346 <error name="seL4_InvalidCapability"> 1347 <description> 1348 The <texttt text="_service"/> or <texttt text="schedcontext"/> is a CPtr to a capability of the wrong type. 1349 </description> 1350 </error> 1351 <error name="seL4_RangeError"> 1352 <description> 1353 The <texttt text="budget"/> or <texttt text="period"/> or <texttt text="extra_refills"/> is too big or too small. 1354 Or, <texttt text="budget"/> is greater than <texttt text="period"/>. 1355 </description> 1356 </error> 1357 </method> 1358 1359 </interface> 1360 1361 <interface name="seL4_SchedContext"> 1362 1363 <method id="SchedContextBind" name="Bind" 1364 manual_name="Bind" manual_label="schedcontext_bind" condition="defined(CONFIG_KERNEL_MCS)"> 1365 <brief> 1366 Bind an object to a scheduling context. The object can be a notification object or a 1367 thread. 1368 1369 If the object is a thread and the thread is in a runnable state and the scheduling 1370 context has available budget, this will start the thread running. 1371 1372 If the object is a notification, when passive threads wait on the notification object and 1373 a signal arrives, the passive thread will receive the scheduling context and possess it 1374 until it waits on the notification object again. 1375 1376 This operation will fail for notification objects if the scheduling context is already 1377 bound to a notification object, and for thread objects if the the scheduling context is 1378 already bound to a thread. 1379 </brief> 1380 <description> 1381 See <autoref label="sec:threads"/> 1382 </description> 1383 <return><errorenumdesc/></return> 1384 <param dir="in" name="cap" type="seL4_CPtr" 1385 description="Capability to a TCB or a notification object"/> 1386 <error name="seL4_IllegalOperation"> 1387 <description> 1388 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1389 Or, <texttt text="_service"/> or <texttt text="cap"/> is already bound to the same type of object. 1390 Or, <texttt text="cap"/> is a TCB in the blocked state and <texttt text="_service"/> is not schedulable. 1391 </description> 1392 </error> 1393 <error name="seL4_InvalidCapability"> 1394 <description> 1395 The <texttt text="_service"/> or <texttt text="cap"/> is a CPtr to a capability of the wrong type. 1396 </description> 1397 </error> 1398 </method> 1399 1400 <method id="SchedContextUnbind" name="Unbind" 1401 manual_name="Unbind" manual_label="schedcontext_unbind" condition="defined(CONFIG_KERNEL_MCS)"> 1402 <brief> 1403 Unbind any objects (threads or notification objects) from a scheduling context. This 1404 will render the bound thread passive, see Section 6.1.5. 1405 </brief> 1406 <description> 1407 See <autoref label="sec:threads"/> 1408 </description> 1409 <return><errorenumdesc/></return> 1410 <error name="seL4_IllegalOperation"> 1411 <description> 1412 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1413 Or, the current thread's TCB is bound to <texttt text="_service"/>. 1414 </description> 1415 </error> 1416 <error name="seL4_InvalidCapability"> 1417 <description> 1418 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1419 </description> 1420 </error> 1421 </method> 1422 1423 <method id="SchedContextUnbindObject" name="UnbindObject" 1424 manual_name="UnbindObject" manual_label="schedcontext_unbindobject" condition="defined(CONFIG_KERNEL_MCS)"> 1425 <brief> 1426 Unbind an object from a scheduling context. The object can be either a thread or a 1427 notification. 1428 1429 If the thread being unbound is the thread that is bound to this scheduling context, 1430 this will render the thread passive. However if the thread being 1431 unbound received the scheduling context via scheduling context donation over IPC, 1432 the scheduling context will be returned to the thread that it was originally bound to. 1433 1434 If the object is a notification and it is bound to the scheduling context, unbind it. 1435 </brief> 1436 <description> 1437 See <autoref label="sec:passive"/> 1438 </description> 1439 <return><errorenumdesc/></return> 1440 <param dir="in" name="cap" type="seL4_CPtr" 1441 description="Capability to a notification that is bound to the scheduling context or capability to a tcb that is bound to this scheduling context or has received it through scheduling context donation."/> 1442 <error name="seL4_IllegalOperation"> 1443 <description> 1444 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1445 Or, <texttt text="cap"/> is not bound to <texttt text="_service"/>. 1446 Or, <texttt text="cap"/> is the current thread's TCB. 1447 </description> 1448 </error> 1449 <error name="seL4_InvalidCapability"> 1450 <description> 1451 The <texttt text="_service"/> or <texttt text="cap"/> is a CPtr to a capability of the wrong type. 1452 </description> 1453 </error> 1454 </method> 1455 <method id="SchedContextConsumed" name="Consumed" manual_name="Consumed" 1456 manual_label="schedcontext_consumed" condition="defined(CONFIG_KERNEL_MCS)"> 1457 <brief> 1458 Return the amount of time used by this scheduling context since this function was last called or a timeout exception triggered. 1459 </brief> 1460 <description> 1461 See <autoref label="sec:threads"/> 1462 </description> 1463 <return><errorenumdesc/></return> 1464 <param dir="out" name="consumed" type="seL4_Time" 1465 description="Amount consumed by this scheduling context."/> 1466 <error name="seL4_IllegalOperation"> 1467 <description> 1468 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1469 </description> 1470 </error> 1471 <error name="seL4_InvalidCapability"> 1472 <description> 1473 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1474 </description> 1475 </error> 1476 </method> 1477 <method id="SchedContextYieldTo" name="YieldTo" 1478 manual_name="YieldTo" manual_label="schedcontext_yieldto" condition="defined(CONFIG_KERNEL_MCS)"> 1479 <brief> 1480 If a thread is currently runnable and running on this scheduling context and the scheduling context has available budget, place it at the head of the scheduling queue. 1481 If the caller is at an equal priority to the thread this will result in the thread being scheduled. 1482 If the caller is at a higher priority the thread will not run until the threads priority is the highest priority in the system. 1483 The caller must have a maximum control priority greater than or equal to the threads priority. 1484 </brief> 1485 <description> 1486 TODO 1487 </description> 1488 <param dir="out" name="consumed" type="seL4_Time"/> 1489 <error name="seL4_IllegalOperation"> 1490 <description> 1491 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1492 Or, <texttt text="_service"/> is not bound to a TCB or is bound to the current thread's TCB. 1493 Or, the target thread's priority is greater than the current thread's maximum controlled priority <docref>(see <autoref label="sec:sched"/>)</docref>. 1494 </description> 1495 </error> 1496 <error name="seL4_InvalidCapability"> 1497 <description> 1498 The <texttt text="_service"/> is a CPtr to a capability of the wrong type. 1499 </description> 1500 </error> 1501 </method> 1502 </interface> 1503 1504</api> 1505