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#pragma once
14
15/* This file provides backwards compatible API wrappers for seemlessly switching between the MCS kernel
16   and non-MCS kernel without too many #ifdefs and without confusing cscope and other analysis tools.
17
18   Of course, if any of the new functionality of the MCS kernel is leveraged, the switch won't be
19   seemless.
20*/
21
22#include <autoconf.h>
23#include <sel4utils/gen_config.h>
24#include <sel4/sel4.h>
25#include <sel4utils/sel4_zf_logif.h>
26
27#ifdef CONFIG_KERNEL_MCS
28#define CONFIG_TIMER_TICK_MS CONFIG_BOOT_THREAD_TIME_SLICE
29#else
30#define CONFIG_BOOT_THREAD_TIME_SLICE CONFIG_TIMER_TICK_MS
31#endif
32
33static inline seL4_MessageInfo_t api_wait(seL4_CPtr ep, seL4_Word *badge)
34{
35#ifdef CONFIG_KERNEL_MCS
36    return seL4_Wait(ep, badge);
37#else
38    return seL4_Recv(ep, badge);
39#endif
40}
41
42static inline seL4_MessageInfo_t api_recv(seL4_CPtr ep, seL4_Word *badge, UNUSED seL4_CPtr reply)
43{
44#ifdef CONFIG_KERNEL_MCS
45    return seL4_Recv(ep, badge, reply);
46#else
47    return seL4_Recv(ep, badge);
48#endif
49}
50
51static inline seL4_MessageInfo_t api_nbrecv(seL4_CPtr ep, seL4_Word *badge, UNUSED seL4_CPtr reply)
52{
53#ifdef CONFIG_KERNEL_MCS
54    return seL4_NBRecv(ep, badge, reply);
55#else
56    return seL4_NBRecv(ep, badge);
57#endif
58}
59
60static inline void api_reply(UNUSED seL4_CPtr reply, seL4_MessageInfo_t msg)
61{
62#ifdef CONFIG_KERNEL_MCS
63    seL4_Send(reply, msg);
64#else
65    seL4_Reply(msg);
66#endif
67}
68
69static inline seL4_MessageInfo_t api_reply_recv(seL4_CPtr ep, seL4_MessageInfo_t msg, seL4_Word *badge,
70                                                UNUSED seL4_CPtr reply)
71{
72#ifdef CONFIG_KERNEL_MCS
73    return seL4_ReplyRecv(ep, msg, badge, reply);
74#else
75    return seL4_ReplyRecv(ep, msg, badge);
76#endif
77}
78
79static inline seL4_MessageInfo_t api_nbsend_recv(UNUSED seL4_CPtr send, UNUSED seL4_MessageInfo_t info,
80                                                 UNUSED seL4_CPtr recv, UNUSED seL4_Word *badge,
81                                                 UNUSED seL4_CPtr reply)
82{
83    ZF_LOGF_IF(!config_set(CONFIG_KERNEL_MCS), "Not available on non MCS kernel");
84#ifdef CONFIG_KERNEL_MCS
85    return seL4_NBSendRecv(send, info, recv, badge, reply);
86#else
87    return seL4_MessageInfo_new(0, 0, 0, 0);
88#endif
89}
90
91static inline seL4_MessageInfo_t api_nbsend_wait(UNUSED seL4_CPtr send, UNUSED seL4_MessageInfo_t info,
92                                                 UNUSED seL4_CPtr recv, UNUSED seL4_Word *badge)
93{
94    ZF_LOGF_IF(!config_set(CONFIG_KERNEL_MCS), "Not available on non MCS kernel");
95#ifdef CONFIG_KERNEL_MCS
96    return seL4_NBSendWait(send, info, recv, badge);
97#else
98    return seL4_MessageInfo_new(0, 0, 0, 0);
99#endif
100}
101
102static inline seL4_Error api_tcb_configure(seL4_CPtr tcb, seL4_CPtr ep, UNUSED seL4_CPtr timeout_ep,
103                                           UNUSED seL4_CPtr sc, seL4_CPtr cspace,
104                                           seL4_Word cdata, seL4_CPtr vspace, seL4_Word vdata,
105                                           seL4_Word ipc_buffer_addr, seL4_CPtr ipc_buffer_cap)
106{
107#ifdef CONFIG_KERNEL_MCS
108    seL4_Error error = seL4_TCB_SetSpace(tcb, ep, cspace, cdata, vspace, vdata);
109    if (!error) {
110        error = seL4_TCB_SetIPCBuffer(tcb, ipc_buffer_addr, ipc_buffer_cap);
111    }
112    if (!error) {
113        error = seL4_TCB_SetTimeoutEndpoint(tcb, timeout_ep);
114    }
115    if (!error && sc != seL4_CapNull) {
116        error = seL4_SchedContext_Bind(sc, tcb);
117    }
118    return error;
119#else
120    return seL4_TCB_Configure(tcb, ep, cspace, cdata, vspace, vdata,
121                              ipc_buffer_addr, ipc_buffer_cap);
122#endif
123}
124
125static inline seL4_Error api_tcb_set_sched_params(seL4_CPtr tcb, seL4_CPtr auth, seL4_Word prio,
126                                                  seL4_Word mcp, UNUSED seL4_CPtr sc, UNUSED seL4_CPtr ep)
127{
128#ifdef CONFIG_KERNEL_MCS
129    return seL4_TCB_SetSchedParams(tcb, auth, mcp, prio, sc, ep);
130#else
131    return seL4_TCB_SetSchedParams(tcb, auth, mcp, prio);
132#endif
133
134}
135
136static inline seL4_Error api_tcb_set_space(seL4_CPtr tcb, seL4_CPtr ep,
137                                           seL4_CPtr cspace,
138                                           seL4_Word cdata, seL4_CPtr vspace, seL4_Word vdata)
139{
140    return seL4_TCB_SetSpace(tcb, ep, cspace, cdata, vspace, vdata);
141}
142
143static inline seL4_Error api_sc_bind(UNUSED seL4_CPtr sc, UNUSED seL4_CPtr tcb)
144{
145    if (!config_set(CONFIG_KERNEL_MCS)) {
146        return (seL4_Error) - ENOSYS;
147    }
148#ifdef CONFIG_KERNEL_MCS
149    return seL4_SchedContext_Bind(sc, tcb);
150#endif
151}
152
153static inline seL4_Error api_sc_unbind_object(UNUSED seL4_CPtr sc, UNUSED seL4_CPtr tcb)
154{
155    if (!config_set(CONFIG_KERNEL_MCS)) {
156        return (seL4_Error) - ENOSYS;
157    }
158#ifdef CONFIG_KERNEL_MCS
159    return seL4_SchedContext_UnbindObject(sc, tcb);
160#endif
161}
162
163static inline seL4_Error api_sc_unbind(UNUSED seL4_CPtr sc)
164{
165    if (!config_set(CONFIG_KERNEL_MCS)) {
166        return (seL4_Error) - ENOSYS;
167    }
168#ifdef CONFIG_KERNEL_MCS
169    return seL4_SchedContext_Unbind(sc);
170#endif
171}
172
173static inline seL4_SchedContext_Consumed_t api_sc_consumed(UNUSED seL4_CPtr sc)
174{
175    if (!config_set(CONFIG_KERNEL_MCS)) {
176        return (seL4_SchedContext_Consumed_t) {
177            .error = (seL4_Error) - ENOSYS
178        };
179    }
180#ifdef CONFIG_KERNEL_MCS
181    return seL4_SchedContext_Consumed(sc);
182#endif
183}
184
185static inline seL4_Error api_sched_ctrl_configure(UNUSED seL4_CPtr sched_ctrl, UNUSED seL4_CPtr sc,
186                                                  UNUSED uint64_t budget, UNUSED uint64_t period,
187                                                  UNUSED seL4_Word refills, UNUSED seL4_Word badge)
188{
189    if (!config_set(CONFIG_KERNEL_MCS)) {
190        return (seL4_Error) - ENOSYS;
191    }
192#ifdef CONFIG_KERNEL_MCS
193    return seL4_SchedControl_Configure(sched_ctrl, sc, budget, period, refills, badge);
194#endif
195}
196