1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13#ifndef __LIBSEL4_SYSCALLS_H
14#define __LIBSEL4_SYSCALLS_H
15#include <autoconf.h>
16
17/**
18 * @defgroup SystemCalls System Calls
19 * @{
20 *
21 * @defgroup GeneralSystemCalls General System Calls
22 * @{
23 */
24
25/**
26 * @xmlonly <manual name="Send" label="sel4_send"/> @endxmlonly
27 * @brief Send to a capability
28 *
29 * @xmlonly
30 * <docref>See <autoref label="sec:sys_send"/></docref>
31 * @endxmlonly
32 *
33 * @param[in] dest The capability to be invoked.
34 * @param[in] msgInfo The messageinfo structure for the IPC.
35 */
36LIBSEL4_INLINE_FUNC void
37seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
38
39/**
40 * @xmlonly <manual name="Recv" label="sel4_recv"/> @endxmlonly
41 * @brief Block until a message is received on an endpoint
42 *
43 * @xmlonly
44 * <docref>See <autoref label="sec:sys_recv"/></docref>
45 * @endxmlonly
46 *
47 * @param[in] src The capability to be invoked.
48 * @param[out] sender The address to write sender information to.
49 *               The sender information is the badge of the
50 *               endpoint capability that was invoked by the
51 *               sender, or the notification word of the
52 *               notification object that was signalled.
53 *               This parameter is ignored if `NULL`.
54 *
55 * @return A `seL4_MessageInfo_t` structure
56 * @xmlonly
57 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
58 * @endxmlonly
59 */
60LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
61seL4_Recv(seL4_CPtr src, seL4_Word* sender);
62
63/**
64 * @xmlonly <manual name="Call" label="sel4_call"/> @endxmlonly
65 * @brief  Call a capability
66 *
67 * @xmlonly
68 * <docref>See <autoref label="sec:sys_call"/></docref>
69 * @endxmlonly
70 *
71 * @param[in] dest The capability to be invoked.
72 * @param[in] msgInfo The messageinfo structure for the IPC.
73 *
74 * @return A `seL4_MessageInfo_t` structure
75 * @xmlonly
76 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
77 * @endxmlonly
78 */
79LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
80seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
81
82/**
83 * @xmlonly <manual name="Reply" label="sel4_reply"/> @endxmlonly
84 * @brief Perform a send to a one-off reply capability stored when
85 *        the thread was last called
86 *
87 * @xmlonly
88 * <docref>See <autoref label="sec:sys_reply"/></docref>
89 * @endxmlonly
90 *
91 * @param[in] msgInfo The messageinfo structure for the IPC.
92 */
93LIBSEL4_INLINE_FUNC void
94seL4_Reply(seL4_MessageInfo_t msgInfo);
95
96/**
97 * @xmlonly <manual name="Non-Blocking Send" label="sel4_nbsend"/> @endxmlonly
98 * @brief Perform a non-blocking send to a capability
99 *
100 * @xmlonly
101 * <docref>See <autoref label="sec:sys_nbsend"/></docref>
102 * @endxmlonly
103 *
104 * @param[in] dest The capability to be invoked.
105 * @param[in] msgInfo The messageinfo structure for the IPC.
106 */
107LIBSEL4_INLINE_FUNC void
108seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
109
110/**
111 * @xmlonly <manual name="Reply Recv" label="sel4_replyrecv"/> @endxmlonly
112 * @brief Perform a reply followed by a receive in one system call
113 *
114 * @xmlonly
115 * <docref>See <autoref label="sec:sys_replyrecv"/></docref>
116 * @endxmlonly
117 *
118 * @param[in] dest The capability to be invoked.
119 * @param[in] msgInfo The messageinfo structure for the IPC.
120 * @param[out] sender The address to write sender information to.
121 *               The sender information is the badge of the
122 *               endpoint capability that was invoked by the
123 *               sender, or the notification word of the
124 *               notification object that was signalled.
125 *               This parameter is ignored if `NULL`.
126 *
127 * @return A `seL4_MessageInfo_t` structure
128 * @xmlonly
129 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
130 * @endxmlonly
131 */
132LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
133seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender);
134
135/**
136 * @xmlonly <manual name="NBRecv" label="sel4_nbrecv"/> @endxmlonly
137 * @brief Receive a message from an endpoint but do not block
138 *        in the case that no messages are pending
139 *
140 * @xmlonly
141 * <docref>See <autoref label="sec:sys_nbrecv"/></docref>
142 * @endxmlonly
143 *
144 * @param[in] src The capability to be invoked.
145 * @param[out] sender The address to write sender information to.
146 *                    The sender information is the badge of the
147 *                    endpoint capability that was invoked by the
148 *                    sender, or the notification word of the
149 *                    notification object that was signalled.
150 *                    This parameter is ignored if `NULL`.
151 *
152 * @return A `seL4_MessageInfo_t` structure
153 * @xmlonly
154 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
155 * @endxmlonly
156 */
157LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
158seL4_NBRecv(seL4_CPtr src, seL4_Word* sender);
159
160/**
161 * @xmlonly <manual name="Yield" label="sel4_yield"/> @endxmlonly
162 * @brief Donate the remaining timeslice to a thread of the same priority
163 *
164 * @xmlonly
165 * <docref>See <autoref label="sec:sys_yield"/></docref>
166 * @endxmlonly
167 */
168LIBSEL4_INLINE_FUNC void
169seL4_Yield(void);
170
171/**
172 * @xmlonly <manual name="Signal" label="sel4_signal"/> @endxmlonly
173 * @brief Signal a notification
174 *
175 * This is not a proper system call known by the kernel. Rather, it is a
176 * convenience wrapper which calls seL4_Send().
177 * It is useful for signalling a notification.
178 *
179 * @xmlonly
180 * <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref>
181 * @endxmlonly
182 *
183 * @param[in] dest The capability to be invoked.
184 */
185LIBSEL4_INLINE_FUNC void
186seL4_Signal(seL4_CPtr dest);
187
188/**
189 * @xmlonly <manual name="Wait" label="sel4_wait"/> @endxmlonly
190 * @brief Perform a receive on a notification object
191 *
192 * This is not a proper system call known by the kernel. Rather, it is a
193 * convenience wrapper which calls seL4_Recv().
194 *
195 * @xmlonly
196 * <docref>See the description of <nameref name="seL4_Recv"/> in <autoref label="sec:sys_recv"/>.</docref>
197 * @endxmlonly
198 *
199 * @param[in] src The capability to be invoked.
200 * @param[out] sender The address to write sender information to.
201 *               The sender information is the badge of the
202 *               endpoint capability that was invoked by the
203 *               sender, or the notification word of the
204 *               notification object that was signalled.
205 *               This parameter is ignored if `NULL`.
206 */
207LIBSEL4_INLINE_FUNC void
208seL4_Wait(seL4_CPtr src, seL4_Word *sender);
209
210/**
211 * @xmlonly <manual name="Poll" label="sel4_poll"/> @endxmlonly
212 * @brief Perform a non-blocking recv on a notification object
213 *
214 * This is not a proper system call known by the kernel. Rather, it is a
215 * convenience wrapper which calls seL4_NBRecv().
216 * It is useful for doing a non-blocking wait on a notification.
217 *
218 * @xmlonly
219 * <docref>See the description of <nameref name="seL4_NBRecv"/> in <autoref label="sec:sys_nbrecv"/>.</docref>
220 * @endxmlonly
221 *
222 * @param[in] src The capability to be invoked.
223 * @param[out] sender The address to write sender information to.
224 *               The sender information is the badge of the
225 *               endpoint capability that was invoked by the
226 *               sender, or the notification word of the
227 *               notification object that was signalled.
228 *               This parameter is ignored if `NULL`.
229 *
230 * @return A `seL4_MessageInfo_t` structure
231 * @xmlonly
232 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
233 * @endxmlonly
234 */
235LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
236seL4_Poll(seL4_CPtr src, seL4_Word *sender);
237
238/** @} */
239
240/**
241 * @defgroup DebuggingSystemCalls
242 * This section documents debugging system calls available when the kernel is
243 * build with the `DEBUG_BUILD` configuration. For any system calls that rely
244 * on a kernel serial driver, `PRINTING` must also be enabled.
245 *
246 * @{
247 */
248#ifdef CONFIG_PRINTING
249/**
250 * @xmlonly <manual name="Put Char" label="sel4_debugputchar"/> @endxmlonly
251 * @brief Output a single char through the kernel.
252 *
253 * Use the kernel serial driver to output a single character. This is useful for
254 * debugging when a user level serial driver is not available.
255 *
256 * @param c The character to output.
257 *
258 */
259LIBSEL4_INLINE_FUNC void
260seL4_DebugPutChar(char c);
261
262/**
263 * @xmlonly <manual name="Dump scheduler" label="sel4_dumpscheduler"/> @endxmlonly
264 * @brief Output the contents of the kernel scheduler.
265 *
266 * Dump the state of the all TCB objects to kernel serial output. This system call
267 * will output a table containing:
268 *    - Address: the address of the TCB object for that thread,
269 *    - Name:    the name of the thread (if set),
270 *    - IP:      the contents of the instruction pointer the thread is at,
271 *    - Priority: the priority of that thread,
272 *    - State   : the state of the thread.
273 */
274
275LIBSEL4_INLINE_FUNC void
276seL4_DebugDumpScheduler(void);
277#endif
278
279#if CONFIG_DEBUG_BUILD
280/**
281 * @xmlonly <manual name="Halt" label="sel4_debughalt"/> @endxmlonly
282 * @brief Halt the system.
283 *
284 * This debugging system call will cause the kernel immediately cease responding to
285 * system calls. The kernel will switch permanently to the idle thread with
286 * interrupts disabled. Depending on the platform, the kernel may switch
287 * the hardware into a low-power state.
288 *
289 */
290LIBSEL4_INLINE_FUNC void
291seL4_DebugHalt(void);
292
293/**
294 * @xmlonly <manual name="Snapshot" label="sel4_debugsnapshot"/> @endxmlonly
295 * @brief Output a capDL dump of the current kernel state.
296 *
297 * This debugging system call will output all of the capabilities in the current
298 * kernel using capDL.
299 *
300 */
301LIBSEL4_INLINE_FUNC void
302seL4_DebugSnapshot(void);
303
304/**
305 * @xmlonly <manual name="Cap Identify" label="sel4_debugcapidentify"/> @endxmlonly
306 * @brief Identify the type of a capability in the current cspace.
307 *
308 * This debugging system call returns the type of capability in a capability
309 * slot in the current cspace. The type returned is not a libsel4 type, but
310 * refers to an internal seL4 type. This can be looked up in a built kernel by
311 * looking for the (generated) `enum cap_tag`, type `cap_tag_t`.
312 *
313 * @param cap A capability slot in the current cspace.
314 * @return The type of capability passed in.
315 *
316 */
317LIBSEL4_INLINE_FUNC seL4_Uint32
318seL4_DebugCapIdentify(seL4_CPtr cap);
319
320/**
321 * @xmlonly <manual name="Name Thread" label="sel4_debugnamethread"/> @endxmlonly
322 * @brief Name a thread.
323 *
324 * Name a thread. This name will then be output by the kernel in all debugging output.
325 * Note that the max name length that can be passed to this function is limited by the
326 * number of chars that will fit in an IPC message (`seL4_MsgMaxLength` multiplied by the
327 * amount of chars that fit in a word). However the name is also truncated in order to fit into a TCB object.
328 * For some platforms you may need to increase `seL4_TCBBits` by 1 in a debug build in order to
329 * fit a long enough name.
330 *
331 * @param tcb A capability to the tcb object for the thread to name.
332 * @param name The name for the thread.
333 *
334 */
335LIBSEL4_INLINE_FUNC void
336seL4_DebugNameThread(seL4_CPtr tcb, const char *name);
337#endif
338
339#ifdef CONFIG_DANGEROUS_CODE_INJECTION
340/**
341 * @xmlonly <manual name="Run" label="sel4_debugrun"/> @endxmlonly
342 * @brief Run a user level function in kernel mode.
343 *
344 * This extremely dangerous function is for running benchmarking and debugging code that
345 * needs to be executed in kernel mode from userlevel. It should never be used in a release kernel.
346 * This works because the kernel can access all user mappings of device memory, and does not switch page directories
347 * on kernel entry.
348 *
349 * Unlike the other system calls in this section, `seL4_DebugRun` does not
350 * depend on the `DEBUG_BUILD` configuration option, but its own config
351 * variable `DANGEROUS_CODE_INJECTION`.
352 *
353 * @param userfn The address in userspace of the function to run.
354 * @param userarg A single argument to pass to the function.
355 *
356 */
357LIBSEL4_INLINE_FUNC void
358seL4_DebugRun(void (* userfn) (void *), void* userarg);
359#endif
360/** @} */
361
362/**
363 * @defgroup BenchmarkingSystemCalls
364 * This section documents system calls available when the kernel is
365 * configured with benchmarking enabled.
366 * There are several different benchmarking modes which can be configured
367 * when building the kernel:
368 *     1. `BENCHMARK_TRACEPOINTS`: Enable using tracepoints in the kernel and timing code.
369 *     2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: Keep track of information on kernel entries.
370 *     3. `BENCHMARK_TRACK_UTILISATION`: Allow users to get CPU timing info for the system, threads and/or idle thread.
371 *
372 * `BENCHMARK_TRACEPOINTS` and `BENCHMARK_TRACK_KERNEL_ENTRIES` use a log buffer that has to be allocated by the user and mapped
373 * to a fixed location in the kernel window.
374 * All of timing information is output in cycles.
375 *
376 * @{
377 */
378#ifdef CONFIG_ENABLE_BENCHMARKS
379/*
380  */
381
382/**
383 * @xmlonly <manual name="Reset Log" label="sel4_benchmarkresetlog"/> @endxmlonly
384 * @brief Reset benchmark logging.
385 *
386 * The behaviour of this system call depends on benchmarking mode in action while invoking
387 * this system call:
388 *    1. `BENCHMARK_TRACEPOINTS`: resets the log index to 0,
389 *    2. `BENCHMARK_TRACK_KERNEL_ENTRIES`:  as above,
390 *    3. `BENCHMARK_TRACK_UTILISATION`: resets benchmark and current thread
391 *        start time (to the time of invoking this syscall), resets idle
392 *        thread utilisation to 0, and starts tracking utilisation.
393 *
394 * @return A `seL4_Error` error if the user-level log buffer has not been set by the user
395 *                         (`BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES`).
396 */
397LIBSEL4_INLINE_FUNC seL4_Error
398seL4_BenchmarkResetLog(void);
399
400/**
401 * @xmlonly <manual name="Finalize Log" label="sel4_benchmarkfinalizelog"/> @endxmlonly
402 * @brief Stop benchmark logging.
403 *
404 * The behaviour of this system call depends on benchmarking mode in action while invoking this system call:
405 *    1. `BENCHMARK_TRACEPOINTS`: Sets the final log buffer index to the current index,
406 *    2. `BENCHMARK_TRACK_KERNEL_ENTRIES`:  as above,
407 *    3. `BENCHMARK_TRACK_UTILISATION`: sets benchmark end time to current time, stops tracking utilisation.
408 *
409 * @return The index of the final entry in the log buffer (if `BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES` are enabled).
410 *
411 */
412LIBSEL4_INLINE_FUNC seL4_Word
413seL4_BenchmarkFinalizeLog(void);
414
415/**
416 * @xmlonly <manual name="Set Log Buffer" label="sel4_benchmarksetlogbuffer"/> @endxmlonly
417 * @brief Set log buffer.
418 *
419 * Provide a large frame object for the kernel to use as a log-buffer.
420 * The object must not be device memory, and must be seL4_LargePageBits in size.
421 *
422 * @param[in] frame_cptr A capability pointer to a user allocated frame of seL4_LargePage size.
423 * @return A `seL4_IllegalOperation` error if `frame_cptr` is not valid and couldn't set the buffer.
424 *
425 */
426LIBSEL4_INLINE_FUNC seL4_Error
427seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr);
428
429/**
430 * @xmlonly <manual name="Null Syscall" label="sel4_benchmarknullsyscall"/> @endxmlonly
431 * @brief Null system call that enters and exits the kernel immediately, for timing kernel traps in microbenchmarks.
432 *
433 *  Used to time kernel traps (in and out).
434 *
435 */
436LIBSEL4_INLINE_FUNC void
437seL4_BenchmarkNullSyscall(void);
438
439/**
440 * @xmlonly <manual name="Flush Caches" label="sel4_benchmarkflushcaches"/> @endxmlonly
441 * @brief Flush hardware caches.
442 *
443 * Flush all possible hardware caches for this platform.
444 */
445LIBSEL4_INLINE_FUNC void
446seL4_BenchmarkFlushCaches(void);
447
448#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
449/**
450 * @xmlonly <manual name="Get Thread Utilisation" label="sel4_benchmarkgetthreadutilisation"/> @endxmlonly
451 * @brief Get utilisation timing information.
452 *
453 * Get timing information for the system, requested thread and idle thread. Such information is written
454 * into the caller's IPC buffer; see the definition of `benchmark_track_util_ipc_index` enum for more
455 * details on the data/format returned on the IPC buffer.
456 *
457 * @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.
458 */
459LIBSEL4_INLINE_FUNC void
460seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr);
461
462/**
463 * @xmlonly <manual name="Reset Thread Utilisation" label="sel4_benchmarkresetthreadutilisation"/> @endxmlonly
464 * @brief Reset utilisation timing for a specific thread.
465 *
466 * Reset the kernel's timing information data (start time and utilisation) for a specific thread.
467 *
468 * @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.
469 *
470 */
471LIBSEL4_INLINE_FUNC void
472seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr);
473#endif
474#endif
475/** @} */
476
477#ifdef CONFIG_ARCH_X86
478/**
479 * @defgroup X86SystemCalls X86 System Calls
480 * @{
481 */
482
483#ifdef CONFIG_VTX
484/**
485 * @xmlonly <manual name="VMEnter" label="sel4_vmenter"/> @endxmlonly
486 * @brief Change current thread to execute from its bound VCPU
487 *
488 * Changes the execution mode of the current thread from normal TCB execution, to
489 * guest execution using its bound VCPU.
490 * @xmlonly
491 * <docref>For details on VCPUs and execution modes see <autoref label="sec:virt"/>.</docref>
492 * @endxmlonly
493 *
494 * Invoking `seL4_VMEnter` is similar to replying to a fault in that updates to the registers
495 * can be given in the message, but unlike a fault no message info
496 * @xmlonly
497 * <docref>(see <autoref label="sec:messageinfo"/>)</docref>
498 * @endxmlonly
499 * is sent as the registers are not optional and the number that must be sent is fixed.
500 * The mapping of hardware register to message register is
501 *      - `SEL4_VMENTER_CALL_EIP_MR` Address to start executing instructions at in the guest mode
502 *      - `SEL4_VMENTER_CALL_CONTROL_PPC_MR` New value for the Primary Processor Based VM Execution Controls
503 *      - `SEL4_VMENTER_CALL_CONTROL_ENTRY_MR` New value for the VM Entry Controls
504 *
505 * On return these same three message registers will be filled with the values at the point
506 * that the privlidged mode ceased executing. If this function returns with `SEL4_VMENTER_RESULT_FAULT`
507 * then the following additional message registers will be filled out
508 *      - `SEL4_VMENTER_FAULT_REASON_MR`
509 *      - `SEL4_VMENTER_FAULT_QUALIFICATION_MR`
510 *      - `SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR`
511 *      - `SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR`
512 *      - `SEL4_VMENTER_FAULT_RFLAGS_MR`
513 *      - `SEL4_VMENTER_FAULT_GUEST_INT_MR`
514 *      - `SEL4_VMENTER_FAULT_CR3_MR`
515 *      - `SEL4_VMENTER_FAULT_EAX`
516 *      - `SEL4_VMENTER_FAULT_EBX`
517 *      - `SEL4_VMENTER_FAULT_ECX`
518 *      - `SEL4_VMENTER_FAULT_EDX`
519 *      - `SEL4_VMENTER_FAULT_ESI`
520 *      - `SEL4_VMENTER_FAULT_EDI`
521 *      - `SEL4_VMENTER_FAULT_EBP`
522 *
523 * @param[out] sender The address to write sender information to.
524 *               If the syscall returns due to receiving a notification
525 *               on the bound notification then the sender information
526 *               is the badge of the notification capability that was invoked.
527 *               This parameter is ignored if `NULL`.
528 * @return `SEL4_VMENTER_RESULT_NOTIF` if a notification was received or `SEL4_VMENTER_RESULT_FAULT`
529 *  if the guest mode execution faulted for any reason
530 */
531LIBSEL4_INLINE_FUNC seL4_Word
532seL4_VMEnter(seL4_Word *sender);
533#endif
534
535/** @} */
536#endif
537
538/** @} */
539
540#endif /* __LIBSEL4_SYSCALLS_H */
541