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="ObjectApiArm" label_prefix="arm_">
9    <interface name="seL4_ARM_PageTable" manual_name="Page Table"
10        cap_description="Capability to the page table being operated on.">
11        <method id="ARMPageTableMap" name="Map" manual_label="pagetable_map">
12            <brief>
13                Map a page table into an address space.
14            </brief>
15            <description>
16                Takes a VSpace capability as an argument,
17                and installs a reference to the invoked
18                <texttt text='PageTable'/> in the VSpace according to the provided virtual address.
19            </description>
20            <param dir="in" name="vspace" type="seL4_CPtr"
21            description="Capability to the VSpace which will contain the mapping.
22                Must be assigned to an ASID pool."/>
23            <param dir="in" name="vaddr" type="seL4_Word"
24            description="Virtual address to map the page into."/>
25            <param dir="in" name="attr" type="seL4_ARM_VMAttributes">
26                <description>
27                    VM Attributes for the mapping. <docref>Possible values for this type are given in <autoref label="ch:vspace"/>  .</docref>
28                </description>
29            <error name="seL4_DeleteFirst">
30                <description>
31                    A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
32                </description>
33            </error>
34            <error name="seL4_FailedLookup">
35                <description>
36                    On aarch64, <texttt text="vspace"/> does not have a Page Directory mapped at <texttt text="vaddr"/>.
37                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
38                </description>
39            </error>
40            <error name="seL4_IllegalOperation">
41                <description>
42                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
43                </description>
44            </error>
45            <error name="seL4_InvalidArgument">
46                <description>
47                    The <texttt text="vaddr"/> is in the kernel virtual address range.
48                </description>
49            </error>
50            <error name="seL4_InvalidCapability">
51                <description>
52                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
53                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
54                    Or, <texttt text="_service"/> is already mapped in a VSpace.
55                </description>
56            </error>
57            </param>
58        </method>
59        <method id="ARMPageTableUnmap" name="Unmap" manual_label="pagetable_unmap">
60            <brief>
61                Unmap a page table from its <texttt text="Page Directory"/> and zero it out.
62            </brief>
63            <description>
64                Removes the reference to the invoked <texttt text="Page Table"/> from its
65                containing <texttt text="Page Directory"/>.
66            </description>
67            <error name="seL4_IllegalOperation">
68                <description>
69                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
70                </description>
71            </error>
72            <error name="seL4_InvalidCapability">
73                <description>
74                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
75                </description>
76            </error>
77            <error name="seL4_RevokeFirst">
78                <description>
79                    A copy of the <texttt text="_service"/> capability exists.
80                </description>
81            </error>
82        </method>
83    </interface>
84    <interface name="seL4_ARM_IOPageTable" manual_name="I/O Page Table"
85        cap_description="Capability to the I/O page table being operated on.">
86        <method id="ARMIOPageTableMap" name="Map" condition="defined(CONFIG_TK1_SMMU)">
87            <description>
88                TODO
89            </description>
90            <param dir="in" name="iospace" type="seL4_ARM_IOSpace"/>
91            <param dir="in" name="ioaddr" type="seL4_Word"/>
92            <error name="seL4_DeleteFirst">
93                <description>
94                    All required page tables are already mapped in <texttt text="iospace"/> at <texttt text="ioaddr"/>.
95                </description>
96            </error>
97            <error name="seL4_IllegalOperation">
98                <description>
99                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
100                </description>
101            </error>
102            <error name="seL4_InvalidCapability">
103                <description>
104                    The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
105                    Or, <texttt text="_service"/> is already mapped in an IOSpace.
106                </description>
107            </error>
108        </method>
109        <method id="ARMIOPageTableUnmap" name="Unmap" condition="defined(CONFIG_TK1_SMMU)">
110            <description>
111                TODO
112            </description>
113            <error name="seL4_IllegalOperation">
114                <description>
115                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
116                </description>
117            </error>
118            <error name="seL4_InvalidCapability">
119                <description>
120                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
121                </description>
122            </error>
123        </method>
124    </interface>
125    <interface name="seL4_ARM_Page" manual_name="Page"
126        cap_description="Capability to the page being operated on.">
127        <method id="ARMPageMap" name="Map">
128            <brief>
129                Map a page into an address space or update the mapping attributes.
130            </brief>
131            <description>
132                Takes a VSpace capability, as an argument and installs a reference
133                to the given <texttt text="Page"/> in the lowest-level unmapped paging structure
134                corresponding to the given address, or updates the mapping attributes if the page is
135                already mapped at this address. The page must not already be mapped through this
136                capability in a different VSpace or at a different address; the page may be mapped
137                in multiple VSpaces by copying the capability.
138            </description>
139            <param dir="in" name="vspace" type="seL4_CPtr"
140            description="Capability to the VSpace which will contain the mapping.
141                Must be assigned to an ASID pool."/>
142            <param dir="in" name="vaddr" type="seL4_Word"
143            description="Virtual address to map the page into."/>
144            <param dir="in" name="rights" type="seL4_CapRights_t">
145                <description>
146                    Rights for the mapping.<docref>Possible values for this type are given in <autoref label="sec:cap_rights"/>  .</docref>
147                </description>
148            </param>
149            <param dir="in" name="attr" type="seL4_ARM_VMAttributes">
150                <description>
151                    VM Attributes for the mapping.<docref>Possible values for this type are given in <autoref label="ch:vspace"/>  .</docref>
152                </description>
153            </param>
154            <error name="seL4_AlignmentError">
155                <description>
156                    The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service"/>.
157                </description>
158            </error>
159            <error name="seL4_DeleteFirst">
160                <description>
161                    A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr"/>.
162                </description>
163            </error>
164            <error name="seL4_FailedLookup">
165                <description>
166                    The <texttt text="vspace"/> does not have a paging structure at the required level mapped at <texttt text="vaddr"/>.
167                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
168                </description>
169            </error>
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_InvalidArgument">
176                <description>
177                    The <texttt text="_service"/> is already mapped in <texttt text="vspace"/> at a different virtual address.
178                    Or, <texttt text="vaddr"/> is in the kernel virtual address range.
179                </description>
180            </error>
181            <error name="seL4_InvalidCapability">
182                <description>
183                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
184                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
185                    Or, <texttt text="_service"/> is already mapped in a different VSpace.
186                </description>
187            </error>
188        </method>
189        <method id="ARMPageUnmap" name="Unmap">
190            <brief>
191                Unmap a page.
192            </brief>
193            <description>
194                Removes an existing mapping.
195            </description>
196            <error name="seL4_IllegalOperation">
197                <description>
198                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
199                </description>
200            </error>
201            <error name="seL4_InvalidCapability">
202                <description>
203                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
204                </description>
205            </error>
206        </method>
207        <method id="ARMPageMapIO" name="MapIO" condition="defined(CONFIG_TK1_SMMU)" manual_name="Map I/O">
208            <brief>
209                TODO
210            </brief>
211            <description>
212                TODO
213            </description>
214            <param dir="in" name="iospace" type="seL4_ARM_IOSpace"/>
215            <param dir="in" name="rights" type="seL4_CapRights_t"/>
216            <param dir="in" name="ioaddr" type="seL4_Word"/>
217            <error name="seL4_DeleteFirst">
218                <description>
219                    A mapping already exists in <texttt text="iospace"/> at <texttt text="ioaddr"/>.
220                </description>
221            </error>
222            <error name="seL4_FailedLookup">
223                <description>
224                    The <texttt text="iospace"/> does not have a sufficient number of IO Page Tables mapped at <texttt text="ioaddr"/>.
225                </description>
226            </error>
227            <error name="seL4_IllegalOperation">
228                <description>
229                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
230                </description>
231            </error>
232            <error name="seL4_InvalidArgument">
233                <description>
234                    No rights were specified in <texttt text="rights"/>.
235                    Or, the rights in the <texttt text="_service"/> capability do not include <texttt text="rights"/>.
236                </description>
237            </error>
238            <error name="seL4_InvalidCapability">
239                <description>
240                    The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
241                    Or, <texttt text="_service"/> is already mapped.
242                    Or, <texttt text="_service"/> is not a page of size 4 KiB.
243                </description>
244            </error>
245        </method>
246        <method id="ARMPageClean_Data" name="Clean_Data" manual_name="Clean Data">
247            <brief>
248                Cleans the data cache out to RAM. The start and end are relative to the page being serviced.
249            </brief>
250            <description>
251                <docref>See <autoref label="ch:vspace"/>.</docref>
252            </description>
253            <param dir="in" name="start_offset" type="seL4_Word"
254            description="The offset, relative to the start of the page inclusive."/>
255            <param dir="in" name="end_offset" type="seL4_Word"
256            description="The offset, relative to the start of the page exclusive."/>
257            <error name="seL4_FailedLookup">
258                <description>
259                    The VSpace of <texttt text="_service"/> is not assigned to an ASID pool.
260                </description>
261            </error>
262            <error name="seL4_IllegalOperation">
263                <description>
264                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
265                    Or, <texttt text="_service"/> is not mapped in a VSpace.
266                    Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
267                </description>
268            </error>
269            <error name="seL4_InvalidArgument">
270                <description>
271                    The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
272                    Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
273                </description>
274            </error>
275            <error name="seL4_InvalidCapability">
276                <description>
277                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
278                </description>
279            </error>
280        </method>
281        <method id="ARMPageInvalidate_Data" name="Invalidate_Data" manual_name="Invalidate Data">
282            <brief>
283                Invalidates the cache range within the given page. The start and end are relative to the page being serviced
284                and should be aligned to a cache line boundary where possible.
285                An additional clean is performed on the outer cache lines if the start and end are
286                not aligned, to clean out the bytes between the requested and the cache line boundary.
287            </brief>
288            <description>
289                <docref>See <autoref label="ch:vspace"/>.</docref>
290            </description>
291            <param dir="in" name="start_offset" type="seL4_Word"
292            description="The offset, relative to the start of the page inclusive."/>
293            <param dir="in" name="end_offset" type="seL4_Word"
294            description="The offset, relative to the start of the page exclusive."/>
295            <error name="seL4_FailedLookup">
296                <description>
297                    The VSpace of <texttt text="_service"/> is not assigned to an ASID pool.
298                </description>
299            </error>
300            <error name="seL4_IllegalOperation">
301                <description>
302                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
303                    Or, <texttt text="_service"/> is not mapped in a VSpace.
304                    Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
305                </description>
306            </error>
307            <error name="seL4_InvalidArgument">
308                <description>
309                    The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
310                    Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
311                </description>
312            </error>
313            <error name="seL4_InvalidCapability">
314                <description>
315                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
316                </description>
317            </error>
318        </method>
319        <method id="ARMPageCleanInvalidate_Data" name="CleanInvalidate_Data"
320            manual_name="Clean and Invalidate Data">
321            <brief>
322                Clean and invalidates the cache range within the given page. The range will be flushed out to RAM.
323                The start and end are relative to the page being serviced.
324            </brief>
325            <description>
326                <docref>See <autoref label="ch:vspace"/>.</docref>
327            </description>
328            <param dir="in" name="start_offset" type="seL4_Word"
329            description="The offset, relative to the start of the page inclusive."/>
330            <param dir="in" name="end_offset" type="seL4_Word"
331            description="The offset, relative to the start of the page exclusive."/>
332            <error name="seL4_FailedLookup">
333                <description>
334                    The VSpace of <texttt text="_service"/> is not assigned to an ASID pool.
335                </description>
336            </error>
337            <error name="seL4_IllegalOperation">
338                <description>
339                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
340                    Or, <texttt text="_service"/> is not mapped in a VSpace.
341                    Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
342                </description>
343            </error>
344            <error name="seL4_InvalidArgument">
345                <description>
346                    The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
347                    Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
348                </description>
349            </error>
350            <error name="seL4_InvalidCapability">
351                <description>
352                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
353                </description>
354            </error>
355        </method>
356        <method id="ARMPageUnify_Instruction" name="Unify_Instruction" manual_name="Unify Instruction">
357            <brief>
358                Unify Instruction Cache. Cleans data lines to point of unification, invalidate
359                corresponding instruction lines to point of unification, then invalidates branch
360                predictors. The start and end are relative to the page being
361                serviced.
362            </brief>
363            <description>
364                <docref>See <autoref label="ch:vspace"/>.</docref>
365            </description>
366            <param dir="in" name="start_offset" type="seL4_Word"
367            description="The offset, relative to the start of the page inclusive."/>
368            <param dir="in" name="end_offset" type="seL4_Word"
369            description="The offset, relative to the start of the page exclusive."/>
370            <error name="seL4_FailedLookup">
371                <description>
372                    The VSpace of <texttt text="_service"/> is not assigned to an ASID pool.
373                </description>
374            </error>
375            <error name="seL4_IllegalOperation">
376                <description>
377                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
378                    Or, <texttt text="_service"/> is not mapped in a VSpace.
379                    Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
380                </description>
381            </error>
382            <error name="seL4_InvalidArgument">
383                <description>
384                    The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
385                    Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
386                </description>
387            </error>
388            <error name="seL4_InvalidCapability">
389                <description>
390                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
391                </description>
392            </error>
393        </method>
394        <method id="ARMPageGetAddress" name="GetAddress" manual_name="Get Address">
395            <brief>
396                Get the physical address of the underlying frame.
397            </brief>
398            <description>
399                <docref>See <autoref label="ch:vspace"/>.</docref>
400            </description>
401            <return>
402                A <texttt text='seL4_ARM_Page_GetAddress_t'/> struct that contains a
403                <texttt text='seL4_Word paddr'/>, which holds the physical address of the page,
404                and <texttt text='int error'/>.<docref> See <autoref label='sec:errors'/> for a description
405                of the message register and tag contents upon error.</docref>
406            </return>
407            <param dir="out" name="paddr" type="seL4_Word"/>
408            <error name="seL4_IllegalOperation">
409                <description>
410                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
411                </description>
412            </error>
413            <error name="seL4_InvalidCapability">
414                <description>
415                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
416                </description>
417            </error>
418        </method>
419    </interface>
420    <interface name="seL4_ARM_ASIDControl" manual_name="ASID Control"
421        cap_description="The master ASIDControl capability being operated on.">
422        <method id="ARMASIDControlMakePool" name="MakePool" manual_name="Make Pool">
423            <brief>
424                Create an ASID Pool.
425            </brief>
426            <description>
427                Together with a capability to <texttt text="Untyped Memory"/>, which is passed as an argument,
428                create an <texttt text="ASID Pool"/>. The untyped capability must represent a
429                4K memory object. This will create an ASID pool with enough space for 1024 VSpaces.
430            </description>
431            <param dir="in" name="untyped" type="seL4_Untyped"
432            description="Capability to an untyped memory object that will become the pool. Must be 4K bytes."/>
433            <param dir="in" name="root" type="seL4_CNode"
434            description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/>
435            <param dir="in" name="index" type="seL4_Word"
436            description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
437            <param dir="in" name="depth" type="seL4_Uint8"
438            description="Number of bits of index to resolve to find the destination slot."/>
439            <error name="seL4_DeleteFirst">
440                <description>
441                    The destination slot contains a capability.
442                    Or, there are no more ASID pools available.
443                </description>
444            </error>
445            <error name="seL4_FailedLookup">
446                <description>
447                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
448                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
449                </description>
450            </error>
451            <error name="seL4_IllegalOperation">
452                <description>
453                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
454                </description>
455            </error>
456            <error name="seL4_InvalidCapability">
457                <description>
458                    The <texttt text="_service"/> or <texttt text="untyped"/> is a CPtr to a capability of the wrong type.
459                    Or, <texttt text="untyped"/> is not the exact size of an ASID pool object.
460                    Or, <texttt text="untyped"/> is a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>)</docref>.
461                </description>
462            </error>
463            <error name="seL4_RangeError">
464                <description>
465                    The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
466                </description>
467            </error>
468            <error name="seL4_RevokeFirst">
469                <description>
470                    The <texttt text="untyped"/> has been used to retype an object.
471                    Or, a copy of the <texttt text="untyped"/> capability exists.
472                </description>
473            </error>
474        </method>
475    </interface>
476    <interface name="seL4_ARM_ASIDPool" manual_name="ASID Pool"
477        cap_description="The ASID pool which is being assigned to. Must not be full. Each ASID pool can contain 1024 entries.">
478        <method id="ARMASIDPoolAssign" name="Assign" manual_label="asidpool_assign"
479            manual_name="Asid Pool Assign">
480            <brief>
481                Assign an ASID Pool.
482            </brief>
483            <description>
484                Assigns an ASID to the VSpace passed in as an argument.
485            </description>
486            <param dir="in" name="vspace" type="seL4_CPtr"
487            description="The VSpace that is being assigned to an ASID pool. Must not already be assigned to an ASID pool."/>
488            <error name="seL4_DeleteFirst">
489                <description>
490                    There are no more ASIDs available in <texttt text="_service"/>.
491                </description>
492            </error>
493            <error name="seL4_FailedLookup">
494                <description>
495                    The ASID pool of <texttt text="_service"/> is no longer assigned.
496                </description>
497            </error>
498            <error name="seL4_IllegalOperation">
499                <description>
500                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
501                </description>
502            </error>
503            <error name="seL4_InvalidCapability">
504                <description>
505                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
506                    Or, <texttt text="vspace"/> is already assigned to an ASID pool.
507                </description>
508            </error>
509        </method>
510    </interface>
511    <interface name="seL4_ARM_VCPU" manual_name="VCPU"
512        cap_description="Capability to the VCPU being operated on.">
513        <method id="ARMVCPUSetTCB" name="SetTCB" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
514            manual_name="Set TCB">
515                <brief>
516                    Bind a TCB to a virtual CPU
517                </brief>
518             <description>
519                 There is a 1:1 relationship between a virtual CPU and a TCB. If either (or both) of them is
520                 associated with another one, they will be dissociated, and then associated to the
521                 ones called in this system calls.
522             </description>
523            <param dir="in" name="tcb" type="seL4_TCB"
524            description="Capability to TCB to bind to a virtual CPU"/>
525            <error name="seL4_IllegalOperation">
526                <description>
527                    The <texttt text="_service"/> or <texttt text="tcb"/> is a CPtr to a capability of the wrong type.
528                </description>
529            </error>
530            <error name="seL4_InvalidCapability">
531                <description>
532                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
533                </description>
534            </error>
535        </method>
536        <method id="ARMVCPUInjectIRQ" name="InjectIRQ" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
537            manual_name="Inject IRQ">
538                <brief>
539                    Inject an IRQ to a virtual CPU
540                </brief>
541            <description>
542                TODO
543            </description>
544            <param dir="in" name="virq" type="seL4_Uint16"
545            description="Virtual IRQ ID"/>
546            <param dir="in" name="priority" type="seL4_Uint8"
547            description="Priority of the IRQ to be injected"/>
548            <param dir="in" name="group" type="seL4_Uint8"
549            description="IRQ group"/>
550            <param dir="in" name="index" type="seL4_Uint8"
551            description="IRQ index"/>
552            <error name="seL4_DeleteFirst">
553                <description>
554                    The <texttt text="index"/> is in use.
555                </description>
556            </error>
557            <error name="seL4_IllegalOperation">
558                <description>
559                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
560                </description>
561            </error>
562            <error name="seL4_InvalidCapability">
563                <description>
564                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
565                </description>
566            </error>
567            <error name="seL4_RangeError">
568                <description>
569                    The <texttt text="virq"/>, <texttt text="priority"/>, <texttt text="group"/>, or <texttt text="index"/> is invalid.
570                </description>
571            </error>
572        </method>
573        <method id="ARMVCPUReadReg" name="ReadRegs" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
574            manual_name="Read Registers">
575                <brief>
576                    Read a virtual CPU register
577                </brief>
578            <description>
579                TODO
580            </description>
581            <param dir="in" name="field" type="seL4_Word"
582            description="Register to read from a VCPU"/>
583            <param dir="out" name="value" type="seL4_Word"
584            description="Returned value of the VCPU register"/>
585            <error name="seL4_IllegalOperation">
586                <description>
587                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
588                </description>
589            </error>
590            <error name="seL4_InvalidArgument">
591                <description>
592                    The <texttt text="field"/> is invalid.
593                </description>
594            </error>
595            <error name="seL4_InvalidCapability">
596                <description>
597                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
598                </description>
599            </error>
600        </method>
601        <method id="ARMVCPUWriteReg" name="WriteRegs" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
602            manual_name="Write Registers">
603                <brief>
604                    Write a virtual CPU register
605                </brief>
606            <description>
607                TODO
608            </description>
609            <param dir="in" name="field" type="seL4_Word"
610            description="Register ID to write to a VCPU"/>
611            <param dir="in" name="value" type="seL4_Word"
612            description="Value to be written to the VCPU register"/>
613            <error name="seL4_IllegalOperation">
614                <description>
615                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
616                </description>
617            </error>
618            <error name="seL4_InvalidArgument">
619                <description>
620                    The <texttt text="field"/> is invalid.
621                </description>
622            </error>
623            <error name="seL4_InvalidCapability">
624                <description>
625                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
626                </description>
627            </error>
628        </method>
629        <method id="ARMVCPUAckVPPI" name="AckVPPI" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
630            manual_name="Acknowledge Virtual PPI IRQ">
631                <brief>
632                    Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault
633                </brief>
634            <description>
635                Acknowledge and unmask the PPI interrupt so that further interrupts can be forwarded
636                through VPPIEvent faults.
637            </description>
638            <param dir="in" name="irq" type="seL4_Word"
639            description="irq to ack."/>
640            <error name="seL4_IllegalOperation">
641                <description>
642                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
643                </description>
644            </error>
645            <error name="seL4_InvalidArgument">
646                <description>
647                    The <texttt text="irq"/> is invalid.
648                </description>
649            </error>
650            <error name="seL4_InvalidCapability">
651                <description>
652                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
653                </description>
654            </error>
655        </method>
656    </interface>
657   <interface name="seL4_IRQControl" manual_name="IRQ Control" cap_description="An IRQControl capability. This gives you the authority to make this call.">
658
659       <method id="ARMIRQIssueIRQHandlerTrigger" name="GetTrigger" manual_name="GetTrigger"
660           manual_label="irq_controlgettrigger">
661            <brief>
662                Create an IRQ handler capability and specify the trigger method (edge or level).
663            </brief>
664            <description>
665                <docref>See <autoref label="sec:interrupts"/>.</docref>
666            </description>
667            <param dir="in" name="irq" type="seL4_Word" description="The IRQ that you want this capability to handle."/>
668
669            <param dir="in" name="trigger" type="seL4_Word" description="Indicates whether this IRQ is edge (1) or level (0) triggered."/>
670            <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."/>
671            <param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
672            <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
673            <error name="seL4_DeleteFirst">
674                <description>
675                    The destination slot contains a capability.
676                </description>
677            </error>
678            <error name="seL4_FailedLookup">
679                <description>
680                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
681                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
682                </description>
683            </error>
684            <error name="seL4_IllegalOperation">
685                <description>
686                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
687                    Or, the platform does not support setting the IRQ trigger.
688                </description>
689            </error>
690            <error name="seL4_InvalidCapability">
691                <description>
692                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
693                </description>
694            </error>
695            <error name="seL4_RangeError">
696                <description>
697                    The <texttt text="irq"/> is invalid.
698                    Or, <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
699                </description>
700            </error>
701            <error name="seL4_RevokeFirst">
702                <description>
703                    An IRQ handler capability for <texttt text="irq"/> has already been created.
704                </description>
705            </error>
706        </method>
707
708       <method id="ARMIRQIssueIRQHandlerTriggerCore" name="GetTriggerCore" manual_name="GetTriggerCore"
709           manual_label="irq_controlgettriggercore" condition="CONFIG_MAX_NUM_NODES > 1">
710            <brief>
711                Create an IRQ handler capability and specify the trigger method (edge or level) and the target core.
712            </brief>
713            <description>
714                <docref>See <autoref label="sec:interrupts"/>.</docref>
715            </description>
716            <param dir="in" name="irq" type="seL4_Word" description="The IRQ that you want this capability to handle."/>
717
718            <param dir="in" name="trigger" type="seL4_Word" description="Indicates whether this IRQ is edge (1) or level (0) triggered."/>
719            <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."/>
720            <param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
721            <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
722            <param dir="in" name="target" type="seL4_Word" description="Indicates the target core ID to which this irq will be sent."/>
723            <error name="seL4_DeleteFirst">
724                <description>
725                    The destination slot contains a capability.
726                </description>
727            </error>
728            <error name="seL4_FailedLookup">
729                <description>
730                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
731                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
732                </description>
733            </error>
734            <error name="seL4_IllegalOperation">
735                <description>
736                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
737                    Or, SMP support is not enabled.
738                </description>
739            </error>
740            <error name="seL4_InvalidArgument">
741                <description>
742                    The <texttt text="target"/> is invalid.
743                </description>
744            </error>
745            <error name="seL4_InvalidCapability">
746                <description>
747                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
748                </description>
749            </error>
750            <error name="seL4_RangeError">
751                <description>
752                    The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
753                </description>
754            </error>
755            <error name="seL4_RevokeFirst">
756                <description>
757                    An IRQ handler capability for <texttt text="irq"/> has already been created.
758                </description>
759            </error>
760        </method>
761    </interface>
762    <interface name="seL4_ARM_SIDControl" manual_name="SID Control" cap_description="A SIDControl capability. This gives you the authority to make this call.">
763       <method id="ARMSIDIssueSIDManager" name="GetSID" manual_name="GetSID"
764           manual_label="sid_controlgetsid" condition="defined(CONFIG_ARM_SMMU)">
765            <brief>
766                Create a SID capability.
767            </brief>
768            <description>
769                <docref>See <autoref label="sec:smmuv2-creating-sel4-arm-sid-capabilities"/>.</docref>
770            </description>
771            <param dir="in" name="sid" type="seL4_Word" description="The SID that you want this capability to manage."/>
772            <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."/>
773            <param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
774            <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
775            <error name="seL4_DeleteFirst">
776                <description>
777                    The destination slot contains a capability.
778                </description>
779            </error>
780            <error name="seL4_FailedLookup">
781                <description>
782                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
783                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
784                </description>
785            </error>
786            <error name="seL4_IllegalOperation">
787                <description>
788                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
789                </description>
790            </error>
791            <error name="seL4_InvalidCapability">
792                <description>
793                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
794                </description>
795            </error>
796            <error name="seL4_RangeError">
797                <description>
798                    The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
799                    Or, <texttt text="sid"/> is invalid.
800                </description>
801            </error>
802            <error name="seL4_RevokeFirst">
803                <description>
804                    An SID capability for <texttt text="sid"/> has already been created.
805                </description>
806            </error>
807        </method>
808       <method id="ARMSIDGetFault" name="GetFault" manual_name="GetFault"
809           manual_label="sid_controlgetfault" condition="defined(CONFIG_ARM_SMMU)">
810            <brief>
811                Get the fault status of the SMMU.
812            </brief>
813            <description>
814                <docref>See <autoref label="sec:smmuv2-fault-handling"/>.</docref>
815            </description>
816            <return>
817                A <texttt text='seL4_ARM_SMMU_GetFault_t'/> struct that contains a
818                <texttt text='seL4_Word status'/>, which holds the global fault status of the SMMU,
819                <texttt text='seL4_Word syndrome_0'/>, which holds the global fault syndrome 0 of the SMMU,
820                <texttt text='seL4_Word syndrome_1'/>, which holds the global fault syndrome 1 of the SMMU,
821                and <texttt text='int error'/>.<docref> See <autoref label='sec:errors'/> for a description
822                of the message register and tag contents upon error.</docref>
823            </return>
824            <param dir="out" name="status" type="seL4_Word"/>
825            <param dir="out" name="syndrome_0" type="seL4_Word"/>
826            <param dir="out" name="syndrome_1" type="seL4_Word"/>
827            <error name="seL4_IllegalOperation">
828                <description>
829                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
830                </description>
831            </error>
832            <error name="seL4_InvalidCapability">
833                <description>
834                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
835                </description>
836            </error>
837        </method>
838        <method id="ARMSIDClearFault" name="ClearFault" manual_name="ClearFault"
839           manual_label="sid_controlclearfault" condition="defined(CONFIG_ARM_SMMU)">
840            <brief>
841                Clear the fault status of the SMMU.
842            </brief>
843            <description>
844                <docref>See <autoref label="sec:smmuv2-fault-handling"/>.</docref>
845            </description>
846            <error name="seL4_IllegalOperation">
847                <description>
848                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
849                </description>
850            </error>
851            <error name="seL4_InvalidCapability">
852                <description>
853                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
854                </description>
855            </error>
856        </method>
857    </interface>
858    <interface name="seL4_ARM_SID" manual_name="SID" cap_description="A SID capability. This gives you the authority to make this call.">
859       <method id="ARMSIDBindCB" name="BindCB" manual_name="BindCB"
860           manual_label="sid_bindcb" condition="defined(CONFIG_ARM_SMMU)">
861            <brief>
862                Binding a context bank to a stream ID.
863            </brief>
864            <description>
865                <docref>See <autoref label="sec:smmuv2-configuring-streams-transactions"/>.</docref>
866            </description>
867           <param dir="in" name="cb" type="seL4_CPtr"
868            description="The CB that is being binded to a stream ID. Must already has an assigned vspace."/>
869            <error name="seL4_DeleteFirst">
870                <description>
871                    The <texttt text="_service"/> is already bound to a context bank.
872                </description>
873            </error>
874            <error name="seL4_IllegalOperation">
875                <description>
876                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
877                </description>
878            </error>
879            <error name="seL4_InvalidCapability">
880                <description>
881                    The <texttt text="_service"/> or <texttt text="cb"/> is a CPtr to a capability of the wrong type.
882                    Or, <texttt text="cb"/> is not assigned to a VSpace.
883                </description>
884            </error>
885        </method>
886       <method id="ARMSIDUnbindCB" name="UnbindCB" manual_name="UnbindCB"
887           manual_label="sid_unbindcb" condition="defined(CONFIG_ARM_SMMU)">
888            <brief>
889                Unbinding a context bank from a stream ID.
890            </brief>
891            <description>
892                <docref>See <autoref label="sec:smmuv2-configuring-streams-transactions"/>.</docref>
893            </description>
894            <error name="seL4_IllegalOperation">
895                <description>
896                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
897                    Or, <texttt text="_service"/> is not bound to a context block.
898                </description>
899            </error>
900            <error name="seL4_InvalidCapability">
901                <description>
902                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
903                </description>
904            </error>
905        </method>
906    </interface>
907    <interface name="seL4_ARM_CBControl" manual_name="CB Control" cap_description="A CBControl capability. This gives you the authority to make this call.">
908       <method id="ARMCBIssueCBManager" name="GetCB" manual_name="GetCB"
909           manual_label="cb_controlgetcb" condition="defined(CONFIG_ARM_SMMU)">
910            <brief>
911                Create a CB capability.
912            </brief>
913            <description>
914                <docref>See <autoref label="sec:smmuv2-creating-sel4-arm-cb-capabilities"/>.</docref>
915            </description>
916            <param dir="in" name="cb" type="seL4_Word" description="The CB that you want this capability to manage."/>
917            <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."/>
918            <param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
919            <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
920            <error name="seL4_DeleteFirst">
921                <description>
922                    The destination slot contains a capability.
923                </description>
924            </error>
925            <error name="seL4_FailedLookup">
926                <description>
927                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
928                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
929                </description>
930            </error>
931            <error name="seL4_IllegalOperation">
932                <description>
933                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
934                </description>
935            </error>
936            <error name="seL4_InvalidCapability">
937                <description>
938                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
939                </description>
940            </error>
941            <error name="seL4_RangeError">
942                <description>
943                    The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
944                    Or, <texttt text="cb"/> is invalid.
945                </description>
946            </error>
947            <error name="seL4_RevokeFirst">
948                <description>
949                    A CB capability for <texttt text="cb"/> has already been created.
950                </description>
951            </error>
952        </method>
953        <method id="ARMCBTLBInvalidateAll" name="TLBInvalidateAll" manual_name="TLBInvalidateAll"
954           manual_label="cb_controltlbinvalidate" condition="defined(CONFIG_ARM_SMMU)">
955            <brief>
956                Invalidate all TLB entries.
957            </brief>
958            <description>
959                <docref>See <autoref label="sec:smmuv2-tlb-invalidation"/>.</docref>
960            </description>
961            <error name="seL4_IllegalOperation">
962                <description>
963                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
964                </description>
965            </error>
966            <error name="seL4_InvalidCapability">
967                <description>
968                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
969                </description>
970            </error>
971        </method>
972    </interface>
973    <interface name="seL4_ARM_CB" manual_name="CB" cap_description="A CB capability. This gives you the authority to make this call.">
974       <method id="ARMCBAssignVspace" name="AssignVspace" manual_name="AssignVspace"
975           manual_label="cb_assignvspace" condition="defined(CONFIG_ARM_SMMU)">
976            <brief>
977                Assigning a vspace to a context bank.
978            </brief>
979            <description>
980                <docref>See <autoref label="sec:smmuv2-configuring-context-banks"/>.</docref>
981            </description>
982           <param dir="in" name="vspace" type="seL4_CPtr"
983            description="The VSpace that is being assigned to a context bank. Must already has an assigned ASID."/>
984            <error name="seL4_DeleteFirst">
985                <description>
986                    The <texttt text="_service"/> is already assigned to a VSpace.
987                </description>
988            </error>
989            <error name="seL4_IllegalOperation">
990                <description>
991                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
992                </description>
993            </error>
994            <error name="seL4_InvalidCapability">
995                <description>
996                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
997                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
998                </description>
999            </error>
1000        </method>
1001        <method id="ARMCBUnassignVspace" name="UnassignVspace" manual_name="UnassignVspace"
1002           manual_label="cb_unassignvspace" condition="defined(CONFIG_ARM_SMMU)">
1003            <brief>
1004                Unassigning a vspace to a context bank.
1005            </brief>
1006            <description>
1007                <docref>See <autoref label="sec:smmuv2-configuring-context-banks"/>.</docref>
1008            </description>
1009            <error name="seL4_IllegalOperation">
1010                <description>
1011                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1012                    Or, <texttt text="_service"/> is not assigned to a VSpace.
1013                </description>
1014            </error>
1015            <error name="seL4_InvalidCapability">
1016                <description>
1017                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1018                </description>
1019            </error>
1020        </method>
1021        <method id="ARMCBTLBInvalidate" name="TLBInvalidate" manual_name="TLBInvalidate"
1022           manual_label="cb_tlbinvalidate" condition="defined(CONFIG_ARM_SMMU)">
1023            <brief>
1024                Invalidating TLB entries used by the current ASID in this context bank.
1025            </brief>
1026            <description>
1027                <docref>See <autoref label="sec:smmuv2-tlb-invalidation"/>.</docref>
1028            </description>
1029            <error name="seL4_IllegalOperation">
1030                <description>
1031                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1032                    Or, <texttt text="_service"/> is not assigned to a VSpace.
1033                </description>
1034            </error>
1035            <error name="seL4_InvalidCapability">
1036                <description>
1037                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1038                </description>
1039            </error>
1040        </method>
1041        <method id="ARMCBGetFault" name="CBGetFault" manual_name="CBGetFault"
1042           manual_label="cb_getfault" condition="defined(CONFIG_ARM_SMMU)">
1043            <brief>
1044                Get the fault status of the context bank.
1045            </brief>
1046            <description>
1047                <docref>See <autoref label="sec:smmuv2-fault-handling"/>.</docref>
1048            </description>
1049            <return>
1050                A <texttt text='seL4_ARM_SMMU_CB_GetFault_t'/> struct that contains a
1051                <texttt text='seL4_Word status'/>, which holds the fault status of the context bank,
1052                <texttt text='seL4_Word address'/>, which holds the faulty address,
1053                and <texttt text='int error'/>.<docref> See <autoref label='sec:errors'/> for a description
1054                of the message register and tag contents upon error.</docref>
1055            </return>
1056            <param dir="out" name="status" type="seL4_Word"/>
1057            <param dir="out" name="address" type="seL4_Word"/>
1058            <error name="seL4_IllegalOperation">
1059                <description>
1060                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1061                </description>
1062            </error>
1063            <error name="seL4_InvalidCapability">
1064                <description>
1065                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1066                </description>
1067            </error>
1068        </method>
1069        <method id="ARMCBClearFault" name="CBClearFault" manual_name="CBClearFault"
1070           manual_label="cb_clearfault" condition="defined(CONFIG_ARM_SMMU)">
1071            <brief>
1072                 Clear the fault status of the context bank.
1073            </brief>
1074            <description>
1075                <docref>See <autoref label="sec:smmuv2-fault-handling"/>.</docref>
1076            </description>
1077            <error name="seL4_IllegalOperation">
1078                <description>
1079                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1080                </description>
1081            </error>
1082            <error name="seL4_InvalidCapability">
1083                <description>
1084                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1085                </description>
1086            </error>
1087        </method>
1088    </interface>
1089</api>
1090