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