portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

mcs: scheduling context donation over ipc

Browse source 
After this commit, threads blocked on an endpoint can recieve a
scheduling context from the thread that wakes the blocked thread.
This commit is contained in:
Anna Lyons 2016-11-09 16:39:49 +11:00 committed by Kent Mcleod
parent 7b25653de7
commit 554f812da3
74 changed files with 2815 additions and 411 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
CMakeLists.txt
View file

@ -311,6 +311,9 @@ list(APPEND gen_files_list "${header_dest}")
set(syscall_xml_base "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/include/api")
set(syscall_dest "gen_headers/arch/api/syscall.h")
if(KernelIsMCS)
set(mcs --mcs)
endif()
add_custom_command(
OUTPUT ${syscall_dest}
COMMAND
@ -322,7 +325,7 @@ add_custom_command(
COMMAND
${PYTHON3} "${SYSCALL_ID_GEN_PATH}"
--xml "${syscall_xml_base}/syscall.xml"
--kernel_header "${syscall_dest}"
--kernel_header "${syscall_dest}" ${mcs}
DEPENDS
"${XMLLINT_PATH}"
"${SYSCALL_ID_GEN_PATH}"

4
include/arch/arm/arch/32/mode/fastpath/fastpath.h
View file

@ -63,6 +63,7 @@ static inline void FORCE_INLINE switchToThread_fp(tcb_t *thread, pde_t *cap_pd,
clearExMonitor_fp();
}
#ifndef CONFIG_KERNEL_MCS
static inline void mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged(
mdb_node_t *node_ptr, word_t mdbNext,
word_t mdbRevocable, word_t mdbFirstBadged)
@ -74,6 +75,7 @@ static inline void mdb_node_ptr_set_mdbPrev_np(mdb_node_t *node_ptr, word_t mdbP
{
node_ptr->words[0] = mdbPrev;
}
#endif
static inline bool_t isValidVTableRoot_fp(cap_t pd_cap)
{
@ -107,10 +109,12 @@ static inline void fastpath_copy_mrs(word_t length, tcb_t *src, tcb_t *dest)
}
}
#ifndef CONFIG_KERNEL_MCS
static inline int fastpath_reply_cap_check(cap_t cap)
{
return (cap.words[0] & MASK(5)) == cap_reply_cap;
}
#endif
/** DONT_TRANSLATE */
static inline void NORETURN fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread)

7
include/arch/arm/arch/32/mode/machine/registerset.h
View file

@ -80,8 +80,15 @@ enum _register {
R4 = 4,
R5 = 5,
R6 = 6,
#ifdef CONFIG_KERNEL_MCS
replyRegister = 6,
#endif
R7 = 7,
R8 = 8,
#ifdef CONFIG_KERNEL_MCS
nbsendRecvDest = 8,
#endif
R9 = 9,
R10 = 10,
R11 = 11,

2
include/arch/arm/arch/64/mode/fastpath/fastpath.h
View file

@ -94,10 +94,12 @@ static inline void fastpath_copy_mrs(word_t length, tcb_t *src, tcb_t *dest)
}
}
#ifndef CONFIG_KERNEL_MCS
static inline int fastpath_reply_cap_check(cap_t cap)
{
return cap_capType_equals(cap, cap_reply_cap);
}
#endif
/** DONT_TRANSLATE */
static inline void NORETURN fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread)

6
include/arch/arm/arch/64/mode/machine/registerset.h
View file

@ -105,8 +105,14 @@ enum _register {
X4 = 4, /* 0x20 */
X5 = 5, /* 0x28 */
X6 = 6, /* 0x30 */
#ifdef CONFIG_KERNEL_MCS
replyRegister = 6,
#endif
X7 = 7, /* 0x38 */
X8 = 8, /* 0x40 */
#ifdef CONFIG_KERNEL_MCS
nbsendRecvDest = 8,
#endif
X9 = 9, /* 0x48 */
X10 = 10, /* 0x50 */
X11 = 11, /* 0x58 */

4
include/arch/arm/arch/fastpath/fastpath.h
View file

@ -22,7 +22,11 @@ NORETURN;
void fastpath_call(word_t cptr, word_t r_msgInfo)
NORETURN SECTION(".vectors.fastpath_call");
#ifdef CONFIG_KERNEL_MCS
void fastpath_reply_recv(word_t cptr, word_t r_msgInfo, word_t reply)
#else
void fastpath_reply_recv(word_t cptr, word_t r_msgInfo)
#endif
NORETURN SECTION(".vectors.fastpath_reply_recv");
#endif /* __ARCH_FASTPATH_H */

4
include/arch/arm/arch/kernel/traps.h
View file

@ -27,7 +27,11 @@ static inline void arch_c_exit_hook(void)
void VISIBLE NORETURN restore_user_context(void);
#ifdef CONFIG_KERNEL_MCS
void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall, word_t reply)
#else
void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
#endif
VISIBLE SECTION(".vectors.text");
void c_handle_interrupt(void)

13
include/arch/x86/arch/32/mode/fastpath/fastpath.h
View file

@ -54,6 +54,7 @@ static inline void FORCE_INLINE switchToThread_fp(tcb_t *thread, vspace_root_t *
NODE_STATE(ksCurThread) = thread;
}
#ifndef CONFIG_KERNEL_MCS
static inline void mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged(
mdb_node_t *node_ptr, word_t mdbNext,
word_t mdbRevocable, word_t mdbFirstBadged)
@ -65,6 +66,7 @@ static inline void mdb_node_ptr_set_mdbPrev_np(mdb_node_t *node_ptr, word_t mdbP
{
node_ptr->words[0] = mdbPrev;
}
#endif
static inline bool_t isValidVTableRoot_fp(cap_t vspace_root_cap)
{
@ -83,14 +85,13 @@ static inline void fastpath_copy_mrs(word_t length, tcb_t *src, tcb_t *dest)
}
/* This is an accelerated check that msgLength, which appears
in the bottom of the msgInfo word, is <= 2 and that msgExtraCaps
which appears above it is zero. We are assuming that n_msgRegisters == 2
in the bottom of the msgInfo word, is <= seL4_FastMessageRegisters and that msgExtraCaps
which appears above it is zero. We are assuming that n_msgRegisters == seL4_FastMessageRegisters
for this check to be useful.*/
compile_assert(n_msgRegisters_eq_2, n_msgRegisters == 2)
static inline int
fastpath_mi_check(word_t msgInfo)
compile_assert(n_msgRegisters_eq, n_msgRegisters == seL4_FastMessageRegisters)
static inline int fastpath_mi_check(word_t msgInfo)
{
return (msgInfo & MASK(seL4_MsgLengthBits + seL4_MsgExtraCapBits)) > 2;
return (msgInfo & MASK(seL4_MsgLengthBits + seL4_MsgExtraCapBits)) > seL4_FastMessageRegisters;
}
static inline void NORETURN FORCE_INLINE fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread)

4
include/arch/x86/arch/32/mode/machine/registerset.h
View file

@ -39,6 +39,10 @@ enum _register {
msgInfoRegister = ESI,
/* 0x18 */ EDI = 6,
/* 0x1C */ EBP = 7,
#ifdef CONFIG_KERNEL_MCS
replyRegister = 7,
n_generalRegisters = 7,
#endif
/* virtual registers (not actually present in hardware) */

2
include/arch/x86/arch/64/mode/fastpath/fastpath.h
View file

@ -74,6 +74,7 @@ static inline void FORCE_INLINE switchToThread_fp(tcb_t *thread, vspace_root_t *
NODE_STATE(ksCurThread) = thread;
}
#ifndef CONFIG_KERNEL_MCS
static inline void thread_state_ptr_set_blockingIPCDiminish_np(thread_state_t *ts_ptr, word_t dim)
{
ts_ptr->words[1] = (ts_ptr->words[1] & 1) | dim;
@ -90,6 +91,7 @@ static inline void mdb_node_ptr_set_mdbPrev_np(mdb_node_t *node_ptr, word_t mdbP
{
node_ptr->words[0] = mdbPrev;
}
#endif
static inline bool_t isValidVTableRoot_fp(cap_t vspace_root_cap)
{

6
include/arch/x86/arch/64/mode/machine/registerset.h
View file

@ -41,7 +41,13 @@ enum _register {
RBX = 3, /* 0x18 */
RBP = 4, /* 0x20 */
R12 = 5, /* 0x28 */
#ifdef CONFIG_KERNEL_MCS
replyRegister = 5,
#endif
R13 = 6, /* 0x30 */
#ifdef CONFIG_KERNEL_MCS
nbsendRecvDest = 6,
#endif
R14 = 7, /* 0x38 */
RDX = 8, /* 0x40 */
// Group the message registers so they can be efficiently copied

6
include/arch/x86/arch/fastpath/fastpath.h
View file

@ -13,10 +13,12 @@
#include <mode/fastpath/fastpath.h>
#ifndef CONFIG_KERNEL_MCS
static inline int fastpath_reply_cap_check(cap_t cap)
{
return cap_capType_equals(cap, cap_reply_cap);
}
#endif
void slowpath(syscall_t syscall)
NORETURN;
@ -24,7 +26,11 @@ NORETURN;
void fastpath_call(word_t cptr, word_t r_msgInfo)
NORETURN;
#ifdef CONFIG_KERNEL_MCS
void fastpath_reply_recv(word_t cptr, word_t r_msgInfo, word_t reply)
#else
void fastpath_reply_recv(word_t cptr, word_t r_msgInfo)
#endif
NORETURN;
#endif

4
include/arch/x86/arch/kernel/traps.h
View file

@ -29,7 +29,11 @@ static inline void arch_c_exit_hook(void)
x86_load_fsgs_base(tcb, SMP_TERNARY(getCurrentCPUIndex(), 0));
}
#ifdef CONFIG_KERNEL_MCS
void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall, word_t reply)
#else
void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
#endif
VISIBLE NORETURN;
void restore_user_context(void)

26
include/fastpath/fastpath.h
View file

@ -69,6 +69,7 @@ static inline void thread_state_ptr_mset_blockingObject_tsType(thread_state_t *t
ts_ptr->words[0] = ep_ref | tsType;
}
#ifndef CONFIG_KERNEL_MCS
static inline void cap_reply_cap_ptr_new_np(cap_t *cap_ptr, word_t capReplyCanGrant,
word_t capReplyMaster, word_t capTCBPtr)
{
@ -81,6 +82,7 @@ static inline void cap_reply_cap_ptr_new_np(cap_t *cap_ptr, word_t capReplyCanGr
(capReplyCanGrant << 5) | cap_reply_cap ;
#endif
}
#endif
static inline void endpoint_ptr_mset_epQueue_tail_state(endpoint_t *ep_ptr, word_t epQueue_tail,
word_t state)
@ -93,6 +95,30 @@ static inline void endpoint_ptr_set_epQueue_head_np(endpoint_t *ep_ptr, word_t e
ep_ptr->words[1] = epQueue_head;
}
#ifdef CONFIG_KERNEL_MCS
static inline void thread_state_ptr_set_replyObject_np(thread_state_t *ts_ptr, word_t reply)
{
assert(!thread_state_ptr_get_tcbQueued(ts_ptr));
assert(!thread_state_ptr_get_tcbInReleaseQueue(ts_ptr));
#if CONFIG_WORD_SIZE == 64
thread_state_ptr_set_replyObject(ts_ptr, REPLY_REF(reply));
#else
ts_ptr->words[1] = REPLY_REF(reply);
#endif
}
static inline reply_t *thread_state_get_replyObject_np(thread_state_t ts)
{
assert(!thread_state_get_tcbQueued(ts));
assert(!thread_state_get_tcbInReleaseQueue(ts));
#if CONFIG_WORD_SIZE == 64
return REPLY_PTR(thread_state_get_replyObject(ts));
#else
return REPLY_PTR(ts.words[1]);
#endif
}
#endif
#include <arch/fastpath/fastpath.h>
#endif

8
include/kernel/thread.h
View file

@ -126,7 +126,12 @@ void suspend(tcb_t *target);
void restart(tcb_t *target);
void doIPCTransfer(tcb_t *sender, endpoint_t *endpoint,
word_t badge, bool_t grant, tcb_t *receiver);
#ifdef CONFIG_KERNEL_MCS
void doReplyTransfer(tcb_t *sender, reply_t *reply, bool_t grant);
#else
void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot, bool_t grant);
void timerTick(void);
#endif
void doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint,
word_t badge, bool_t canGrant, tcb_t *receiver,
word_t *receiveBuffer);
@ -143,9 +148,6 @@ void setMCPriority(tcb_t *tptr, prio_t mcp);
void scheduleTCB(tcb_t *tptr);
void possibleSwitchTo(tcb_t *tptr);
void setThreadState(tcb_t *tptr, _thread_state_t ts);
#ifndef CONFIG_KERNEL_MCS
void timerTick(void);
#endif
void rescheduleRequired(void);
/* declare that the thread has had its registers (in its user_context_t) modified and it

4
include/machine/registerset.h
View file

@ -34,4 +34,8 @@ static inline word_t PURE getRegister(tcb_t *thread, register_t reg)
return thread->tcbArch.tcbContext.registers[reg];
}
#ifdef CONFIG_KERNEL_MCS
word_t getNBSendRecvDest(void);
#endif
#endif

6
include/object/cnode.h
View file

@ -32,7 +32,6 @@ exception_t invokeCNodeInsert(cap_t cap, cte_t *srcSlot, cte_t *destSlot);
exception_t invokeCNodeMove(cap_t cap, cte_t *srcSlot, cte_t *destSlot);
exception_t invokeCNodeRotate(cap_t cap1, cap_t cap2, cte_t *slot1,
cte_t *slot2, cte_t *slot3);
exception_t invokeCNodeSaveCaller(cte_t *destSlot);
void cteInsert(cap_t newCap, cte_t *srcSlot, cte_t *destSlot);
void cteMove(cap_t newCap, cte_t *srcSlot, cte_t *destSlot);
void capSwapForDelete(cte_t *slot1, cte_t *slot2);
@ -41,7 +40,6 @@ exception_t cteRevoke(cte_t *slot);
exception_t cteDelete(cte_t *slot, bool_t exposed);
void cteDeleteOne(cte_t *slot);
void insertNewCap(cte_t *parent, cte_t *slot, cap_t cap);
void setupReplyMaster(tcb_t *thread);
bool_t PURE isMDBParentOf(cte_t *cte_a, cte_t *cte_b);
exception_t ensureNoChildren(cte_t *slot);
exception_t ensureEmptySlot(cte_t *slot);
@ -50,4 +48,8 @@ bool_t PURE slotCapLongRunningDelete(cte_t *slot);
cte_t *getReceiveSlots(tcb_t *thread, word_t *buffer);
cap_transfer_t PURE loadCapTransfer(word_t *buffer);
#ifndef CONFIG_KERNEL_MCS
exception_t invokeCNodeSaveCaller(cte_t *destSlot);
void setupReplyMaster(tcb_t *thread);
#endif
#endif

8
include/object/endpoint.h
View file

@ -25,13 +25,17 @@ static inline tcb_queue_t PURE ep_ptr_get_queue(endpoint_t *epptr)
}
#ifdef CONFIG_KERNEL_MCS
void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
bool_t canGrant, bool_t canGrantReply, bool_t canDonate, tcb_t *thread,
endpoint_t *epptr);
void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking, cap_t replyCPtr);
void reorderEP(endpoint_t *epptr, tcb_t *thread);
#endif
#else
void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
bool_t canGrant, bool_t canGrantReply, tcb_t *thread,
endpoint_t *epptr);
void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking);
#endif
void cancelIPC(tcb_t *tptr);
void cancelAllIPC(endpoint_t *epptr);
void cancelBadgedSends(endpoint_t *epptr, word_t badge);

13
include/object/objecttype.h
View file

@ -30,6 +30,18 @@ cap_t CONST maskCapRights(seL4_CapRights_t seL4_CapRights, cap_t cap);
cap_t createObject(object_t t, void *regionBase, word_t, bool_t deviceMemory);
void createNewObjects(object_t t, cte_t *parent, slot_range_t slots,
void *regionBase, word_t userSize, bool_t deviceMemory);
#ifdef CONFIG_KERNEL_MCS
exception_t decodeInvocation(word_t invLabel, word_t length,
cptr_t capIndex, cte_t *slot, cap_t cap,
extra_caps_t excaps, bool_t block, bool_t call,
bool_t canDonate, word_t *buffer);
exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
bool_t canGrant, bool_t canGrantReply,
bool_t block, bool_t call, bool_t canDonate);
exception_t performInvocation_Notification(notification_t *ntfn,
word_t badge);
exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply, bool_t canGrant);
#else
exception_t decodeInvocation(word_t invLabel, word_t length,
cptr_t capIndex, cte_t *slot, cap_t cap,
extra_caps_t excaps, bool_t block, bool_t call,
@ -40,6 +52,7 @@ exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
exception_t performInvocation_Notification(notification_t *ntfn,
word_t badge);
exception_t performInvocation_Reply(tcb_t *thread, cte_t *slot, bool_t canGrant);
#endif
word_t getObjectSize(word_t t, word_t userObjSize);
static inline void postCapDeletion(cap_t cap)

26
include/object/reply.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(DATA61_GPL)
*/
#ifndef __OBJECT_REPLY_H
#define __OBJECT_REPLY_H
#include <types.h>
#include <api/failures.h>
#include <object/structures.h>
/* Push a reply object onto the call stack */
void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t canDonate);
/* Pop the head reply from the call stack */
void reply_pop(reply_t *reply);
/* Remove a reply from the middle of the call stack */
void reply_remove(reply_t *reply);
#endif /* __OBJECT_REPLY_H */

12
include/object/schedcontext.h
View file

@ -54,9 +54,19 @@ void schedContext_unbindAllTCBs(sched_context_t *sc);
/*
* Resume a scheduling context. This will check if a the tcb bound to the scheduling context
* is runnable and add it to the scheduling queue if required
* is runnable, if so, it will then check if the budget is due to be recharged and do so.
* If the scheduling context has insufficient budget the bound tcb is placed in the release queue.
*
* @pre (sc != NULL)
*/
void schedContext_resume(sched_context_t *sc);
/*
* Donate sc to tcb.
*
* @pre (sc != NULL && tcb != NULL)
* @post (sc->scTcb == tcb && tcb->tcbSchedContext == sc)
*/
void schedContext_donate(sched_context_t *sc, tcb_t *to);
#endif /* __OBJECT_SCHED_CONTEXT_H */

48
include/object/structures.h
View file

@ -92,6 +92,9 @@ typedef word_t notification_state_t;
#define SC_REF(p) ((word_t) (p))
#define SC_PTR(r) ((sched_context_t *) (r))
#define REPLY_REF(p) ((word_t) (p))
#define REPLY_PTR(r) ((reply_t *) (r))
#define WORD_PTR(r) ((word_t *)(r))
#define WORD_REF(p) ((word_t)(p))
@ -173,6 +176,10 @@ enum tcb_cnode_index {
/* VSpace root */
tcbVTable = 1,
#ifdef CONFIG_KERNEL_MCS
/* IPC buffer cap slot */
tcbBuffer = 2,
#else
/* Reply cap slot */
tcbReply = 2,
@ -181,7 +188,7 @@ enum tcb_cnode_index {
/* IPC buffer cap slot */
tcbBuffer = 4,
#endif
tcbCNodeEntries
};
typedef word_t tcb_cnode_index_t;
@ -218,8 +225,10 @@ static inline vm_attributes_t CONST vmAttributesFromWord(word_t w)
#ifdef CONFIG_KERNEL_MCS
typedef struct sched_context sched_context_t;
typedef struct reply reply_t;
#endif
/* TCB: size >= 18 words + sizeof(arch_tcb_t) (aligned to nearest power of 2) */
/* TCB: size >= 19 words + sizeof(arch_tcb_t) (aligned to nearest power of 2) */
struct tcb {
/* arch specific tcb state (including context)*/
arch_tcb_t tcbArch;
@ -274,6 +283,10 @@ struct tcb {
struct tcb *tcbEPNext;
struct tcb *tcbEPPrev;
#ifdef CONFIG_KERNEL_MCS
/* if tcb is in a call, pointer to the reply object, 1 word */
reply_t *tcbReply;
#endif
#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
/* 16 bytes (12 bytes aarch32) */
benchmark_util_t benchmark;
@ -311,6 +324,10 @@ struct sched_context {
/* thread that this scheduling context is bound to */
tcb_t *scTcb;
/* if this is not NULL, it points to the last reply object that was generated
* when the scheduling context was passed over a Call */
reply_t *scReply;
/* Amount of refills this sc tracks */
word_t scRefillMax;
/* Index of the head of the refill circular buffer */
@ -321,6 +338,20 @@ struct sched_context {
/* circular buffer of budget refills, ordered by rAmount */
refill_t scRefills[MAX_REFILLS];
};
struct reply {
/* the caller that is blocked on this reply object */
tcb_t *replyCaller;
/* 0 if this is the start of the call chain, or points to the
* previous reply object in a call chain */
call_stack_t replyPrev;
/* Either a scheduling context if this reply object is the head of the call chain
* (the last caller before the server) or another reply object. 0 if no scheduling
* context was passed along the call chain */
call_stack_t replyNext;
};
#endif
/* Ensure object sizes are sane */
@ -337,6 +368,7 @@ compile_assert(notification_size_sane, sizeof(notification_t) <= BIT(seL4_Notifi
compile_assert(ipc_buf_size_sane, sizeof(seL4_IPCBuffer) == BIT(seL4_IPCBufferSizeBits))
#ifdef CONFIG_KERNEL_MCS
compile_assert(sc_size_sane, sizeof(sched_context_t) <= BIT(seL4_SchedContextBits))
compile_assert(reply_size_sane, sizeof(reply_t) <= BIT(seL4_ReplyBits))
#endif
/* helper functions */
@ -385,7 +417,11 @@ static inline word_t CONST cap_get_capSizeBits(cap_t cap)
return 0;
case cap_reply_cap:
#ifdef CONFIG_KERNEL_MCS
return seL4_ReplyBits;
#else
return 0;
#endif
case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
@ -442,7 +478,11 @@ static inline bool_t CONST cap_get_capIsPhysical(cap_t cap)
return false;
case cap_reply_cap:
#ifdef CONFIG_KERNEL_MCS
return true;
#else
return false;
#endif
case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
@ -487,7 +527,11 @@ static inline void *CONST cap_get_capPtr(cap_t cap)
return NULL;
case cap_reply_cap:
#ifdef CONFIG_KERNEL_MCS
return REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap));
#else
return NULL;
#endif
case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS

23
include/object/structures_32.bf
View file

@ -51,6 +51,21 @@ block notification_cap {
field capType 4
}
#ifdef CONFIG_KERNEL_MCS
block reply_cap {
field capReplyPtr 32
padding 27
field capReplyCanGrant 1
field capType 4
}
block call_stack {
field_high callStackPtr 28
padding 3
field isHead 1
}
#else
block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
padding 32
@ -59,7 +74,7 @@ block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
field capReplyMaster 1
field capType 4
}
#endif
-- The user-visible format of the data word is defined by cnode_capdata, below.
block cnode_cap(capCNodeRadix, capCNodeGuardSize, capCNodeGuard,
capCNodePtr, capType) {
@ -297,7 +312,7 @@ block thread_state(blockingIPCBadge, blockingIPCCanGrant,
blockingIPCCanGrantReply, blockingIPCIsCall,
tcbQueued, blockingObject,
#ifdef CONFIG_KERNEL_MCS
tcbInReleaseQueue,
tcbInReleaseQueue, replyObject,
#endif
tsType) {
field blockingIPCBadge 28
@ -309,7 +324,8 @@ block thread_state(blockingIPCBadge, blockingIPCCanGrant,
-- this is fastpath-specific. it is useful to be able to write
-- tsType and without changing tcbQueued or tcbInReleaseQueue
#ifdef CONFIG_KERNEL_MCS
padding 30
field_high replyObject 28
padding 2
#else
padding 31
#endif
@ -321,4 +337,3 @@ block thread_state(blockingIPCBadge, blockingIPCCanGrant,
field_high blockingObject 28
field tsType 4
}

27
include/object/structures_64.bf
View file

@ -80,6 +80,21 @@ block notification_cap {
#endif
}
#ifdef CONFIG_KERNEL_MCS
block reply_cap {
field capReplyPtr 64
field capType 5
field capReplyCanGrant 1
padding 58
}
block call_stack(callStackPtr, isHead) {
padding 15
field isHead 1
field_high callStackPtr 48
}
#else
block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
field capTCBPtr 64
@ -88,6 +103,7 @@ block reply_cap(capReplyCanGrant, capReplyMaster, capTCBPtr, capType) {
field capReplyCanGrant 1
field capReplyMaster 1
}
#endif
-- The user-visible format of the data word is defined by cnode_capdata, below.
block cnode_cap(capCNodeRadix, capCNodeGuardSize, capCNodeGuard,
@ -382,15 +398,18 @@ block DebugException {
-- Thread state: size = 24 bytes
block thread_state(blockingIPCBadge, blockingIPCCanGrant,
blockingIPCCanGrantReply, blockingIPCIsCall,
tcbQueued,
#ifdef CONFIG_KERNEL_MCS
tcbInReleaseQueue,
tcbQueued, tsType,
tcbInReleaseQueue, blockingObject, replyObject) {
#else
tcbQueued, blockingObject,
tsType) {
#endif
blockingObject, tsType) {
field blockingIPCBadge 64
#ifdef CONFIG_KERNEL_MCS
padding 59
padding 15
field_high replyObject 44
#else
padding 60
#endif

38
include/object/tcb.h
View file

@ -82,11 +82,49 @@ void remoteTCBStall(tcb_t *tcb);
#define SCHED_ENQUEUE_CURRENT_TCB tcbSchedEnqueue(NODE_STATE(ksCurThread))
#define SCHED_APPEND_CURRENT_TCB tcbSchedAppend(NODE_STATE(ksCurThread))
#ifdef CONFIG_KERNEL_MCS
/* Add TCB into the priority ordered endpoint queue */
static inline tcb_queue_t tcbEPAppend(tcb_t *tcb, tcb_queue_t queue)
{
/* start at the back of the queue as FIFO is the common case */
tcb_t *before = queue.end;
tcb_t *after = NULL;
/* find a place to put the tcb */
while (unlikely(before != NULL && tcb->tcbPriority > before->tcbPriority)) {
after = before;
before = after->tcbEPPrev;
}
if (unlikely(before == NULL)) {
/* insert at head */
queue.head = tcb;
} else {
before->tcbEPNext = tcb;
}
if (likely(after == NULL)) {
/* insert at tail */
queue.end = tcb;
} else {
after->tcbEPPrev = tcb;
}
tcb->tcbEPNext = after;
tcb->tcbEPPrev = before;
return queue;
}
tcb_queue_t tcbEPDequeue(tcb_t *tcb, tcb_queue_t queue);
#else
tcb_queue_t tcbEPAppend(tcb_t *tcb, tcb_queue_t queue);
tcb_queue_t tcbEPDequeue(tcb_t *tcb, tcb_queue_t queue);
void setupCallerCap(tcb_t *sender, tcb_t *receiver, bool_t canGrant);
void deleteCallerCap(tcb_t *receiver);
#endif
word_t copyMRs(tcb_t *sender, word_t *sendBuf, tcb_t *receiver,
word_t *recvBuf, word_t n);

7
libsel4/CMakeLists.txt
View file

@ -116,6 +116,9 @@ genbf(
"${CMAKE_CURRENT_BINARY_DIR}/sel4_arch_include/${KernelSel4Arch}/sel4/sel4_arch/types_gen.h"
)
if(KernelIsMCS)
set(mcs --mcs)
endif()
add_custom_command(
OUTPUT include/sel4/syscall.h
COMMAND rm -f include/sel4/syscall.h
@ -128,7 +131,7 @@ add_custom_command(
COMMAND
${PYTHON3} "${SYSCALL_ID_GEN_PATH}"
--xml "${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xml"
--libsel4_header include/sel4/syscall.h
--libsel4_header include/sel4/syscall.h ${mcs}
DEPENDS
"${SYSCALL_ID_GEN_PATH}" "${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xsd"
"${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xml"
@ -148,7 +151,7 @@ add_custom_command(
COMMAND
echo "CONFIG_WORD_SIZE=${KernelWordSize}" > config
COMMAND
"${PYTHON3}" "${SYSCALL_STUB_GEN_PATH}" ${buffer} -a "${KernelSel4Arch}" -c config -o
"${PYTHON3}" "${SYSCALL_STUB_GEN_PATH}" ${buffer} ${mcs} -a "${KernelSel4Arch}" -c config -o
include/interfaces/sel4_client.h ${interface_xmls}
DEPENDS
"${SYSCALL_STUB_GEN_PATH}"

327
libsel4/arch_include/arm/sel4/arch/syscalls.h
View file

@ -18,6 +18,12 @@
#include <sel4/sel4_arch/syscalls.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
#define LIBSEL4_MCS_REPLY reply
#else
#define LIBSEL4_MCS_REPLY 0
#endif
LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
@ -50,6 +56,7 @@ LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t m
);
}
#ifndef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo)
{
arm_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
@ -65,13 +72,19 @@ LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
);
}
#endif
LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest)
{
arm_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -80,7 +93,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sende
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
@ -94,8 +107,13 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sende
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -104,7 +122,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
/* Write the message back out to memory. */
if (mr0 != seL4_Null) {
@ -127,7 +145,11 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -136,7 +158,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sen
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
@ -158,7 +180,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInf
seL4_Word msg2 = seL4_GetMR(2);
seL4_Word msg3 = seL4_GetMR(3);
arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
/* Write out the data back to memory. */
seL4_SetMR(0, msg0);
@ -192,7 +214,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_Mes
msg3 = *mr3;
}
arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
@ -211,7 +233,12 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_Mes
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -226,7 +253,8 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_Messag
msg2 = seL4_GetMR(2);
msg3 = seL4_GetMR(3);
arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
LIBSEL4_MCS_REPLY);
/* Write the message back out to memory. */
seL4_SetMR(0, msg0);
@ -242,9 +270,15 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_Messag
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -266,7 +300,8 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4
msg3 = *mr3;
}
arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
LIBSEL4_MCS_REPLY);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
@ -290,12 +325,259 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
/* Load beginning of the message into registers. */
msg0 = seL4_GetMR(0);
msg1 = seL4_GetMR(1);
msg2 = seL4_GetMR(2);
msg3 = seL4_GetMR(3);
arm_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
reply);
/* Write the message back out to memory. */
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
arm_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
reply);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
/* Load beginning of the message into registers. */
msg0 = seL4_GetMR(0);
msg1 = seL4_GetMR(1);
msg2 = seL4_GetMR(2);
msg3 = seL4_GetMR(3);
arm_sys_nbsend_recv(seL4_SysNBSendWait, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
dest);
/* Write the message back out to memory. */
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
arm_sys_nbsend_recv(seL4_SysNBSendRecv, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
dest);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#endif
LIBSEL4_INLINE_FUNC void seL4_Yield(void)
{
arm_sys_null(seL4_SysYield);
asm volatile("" ::: "memory");
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
arm_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
/* Write the message back out to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#endif
#ifdef CONFIG_PRINTING
LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
{
@ -306,7 +588,7 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
@ -318,7 +600,7 @@ LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
arm_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
#endif
@ -342,7 +624,7 @@ LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
arm_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
arm_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Uint32)cap;
}
@ -358,7 +640,7 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
#if CONFIG_MAX_NUM_NODES > 1
@ -388,7 +670,7 @@ LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void)
seL4_Word unused4 = 0;
seL4_Word ret;
arm_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
arm_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Error) ret;
}
@ -400,10 +682,11 @@ LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void)
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word index_ret;
arm_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
return (seL4_Word)index_ret;
seL4_Word index_ret;
arm_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Word) index_ret;
}
LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
@ -415,7 +698,7 @@ LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
seL4_Word unused4 = 0;
arm_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3,
&unused4);
&unused4, 0);
return (seL4_Error) frame_cptr;
}
@ -443,7 +726,7 @@ LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
&unused5);
&unused5, 0);
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
@ -456,8 +739,9 @@ LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3,
&unused4, &unused5);
&unused4, &unused5, 0);
}
#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
#endif /* CONFIG_ENABLE_BENCHMARKS */
@ -469,14 +753,21 @@ LIBSEL4_INLINE_FUNC void seL4_SetTLSBase(seL4_Word tls_base)
}
#endif /* CONFIG_SET_TLS_BASE_SELF */
#ifndef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_Recv(src, sender);
}
#endif
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender)
{
#ifdef CONFIG_KERNEL_MCS
return seL4_NBWait(src, sender);
#else
return seL4_NBRecv(src, sender);
#endif
}
#endif

9
libsel4/arch_include/x86/sel4/arch/syscalls.h
View file

@ -18,14 +18,19 @@
#include <sel4/sel4_arch/syscalls.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender)
{
return seL4_NBWait(src, sender);
}
#else /* CONFIG_KERNEL_MCS */
LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_Recv(src, sender);
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender)
{
return seL4_NBRecv(src, sender);
}
#endif /* !CONFIG_KERNEL_MCS */
#endif

21
libsel4/include/api/syscall.xml
View file

@ -13,7 +13,7 @@
<!-- Please see syscalls.xsd to see the format of this file -->
<syscalls>
<!-- official API syscalls -->
<api>
<api-master>
<config>
<syscall name="Call" />
<syscall name="ReplyRecv" />
@ -22,9 +22,24 @@
<syscall name="Recv" />
<syscall name="Reply" />
<syscall name="Yield" />
<syscall name="NBRecv" />
<syscall name="NBRecv" />
</config>
</api>
</api-master>
<api-mcs>
<config>
<syscall name="Call" />
<syscall name="ReplyRecv" />
<syscall name="NBSendRecv" />
<syscall name="NBSendWait" />
<syscall name="Send" />
<syscall name="NBSend" />
<syscall name="Recv" />
<syscall name="NBRecv" />
<syscall name="Wait" />
<syscall name="NBWait" />
<syscall name="Yield" />
</config>
</api-mcs>
<!-- Syscalls on the unknown syscall path. These definitions will be wrapped in #if condition -->
<debug>
<config condition="defined CONFIG_PRINTING">

3
libsel4/include/api/syscall.xsd
View file

@ -21,7 +21,8 @@
<xsd:complexType name="SyscallListType">
<xsd:sequence>
<xsd:element name="api" type="ApiType" />
<xsd:element name="api-master" type="ApiType" />
<xsd:element name="api-mcs" type="ApiType" />
<xsd:element name="debug" type="DebugType" />
</xsd:sequence>
</xsd:complexType>

2
libsel4/include/interfaces/sel4.xml
View file

@ -517,7 +517,7 @@
<param dir="in" name="src_depth" type="seL4_Uint8" description="Depth to resolve src_index to."/>
</method>
<method id="CNodeSaveCaller" name="SaveCaller" manual_name="Save Caller" manual_label="cnode_savecaller">
<method id="CNodeSaveCaller" name="SaveCaller" manual_name="Save Caller" manual_label="cnode_savecaller" condition="!defined(CONFIG_KERNEL_MCS)">
<brief>
Save the reply capability from the last time the thread was called in the given CSpace so that it can be invoked later
</brief>

2
libsel4/include/sel4/macros.h
View file

@ -48,6 +48,8 @@
#define LIBSEL4_INLINE_FUNC static inline
#endif
#define LIBSEL4_UNUSED __attribute__((unused))
#define SEL4_DEPRECATED(x) __attribute__((deprecated(x)))
#define SEL4_DEPRECATE_MACRO(x) _Pragma("deprecated") x

1
libsel4/include/sel4/objecttype.h
View file

@ -21,6 +21,7 @@ typedef enum api_object {
seL4_CapTableObject,
#ifdef CONFIG_KERNEL_MCS
seL4_SchedContextObject,
seL4_ReplyObject,
#endif
seL4_NonArchObjectTypeCount,
} seL4_ObjectType;

221
libsel4/include/sel4/syscalls.h
View file

@ -20,224 +20,13 @@
* @defgroup SystemCalls System Calls
* @{
*
* @defgroup GeneralSystemCalls General System Calls
* @{
*/
/**
* @xmlonly <manual name="Send" label="sel4_send"/> @endxmlonly
* @brief Send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_send"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Recv" label="sel4_recv"/> @endxmlonly
* @brief Block until a message is received on an endpoint
*
* @xmlonly
* <docref>See <autoref label="sec:sys_recv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Recv(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Call" label="sel4_call"/> @endxmlonly
* @brief Call a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_call"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply" label="sel4_reply"/> @endxmlonly
* @brief Perform a send to a one-off reply capability stored when
* the thread was last called
*
* @xmlonly
* <docref>See <autoref label="sec:sys_reply"/></docref>
* @endxmlonly
*
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Reply(seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Non-Blocking Send" label="sel4_nbsend"/> @endxmlonly
* @brief Perform a non-blocking send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsend"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply Recv" label="sel4_replyrecv"/> @endxmlonly
* @brief Perform a reply followed by a receive in one system call
*
* @xmlonly
* <docref>See <autoref label="sec:sys_replyrecv"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender);
/**
* @xmlonly <manual name="NBRecv" label="sel4_nbrecv"/> @endxmlonly
* @brief Receive a message from an endpoint but do not block
* in the case that no messages are pending
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbrecv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBRecv(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Yield" label="sel4_yield"/> @endxmlonly
* @brief Donate the remaining timeslice to a thread of the same priority
*
* @xmlonly
* <docref>See <autoref label="sec:sys_yield"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC void
seL4_Yield(void);
/**
* @xmlonly <manual name="Signal" label="sel4_signal"/> @endxmlonly
* @brief Signal a notification
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Send().
* It is useful for signalling a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
*/
LIBSEL4_INLINE_FUNC void
seL4_Signal(seL4_CPtr dest);
/**
* @xmlonly <manual name="Wait" label="sel4_wait"/> @endxmlonly
* @brief Perform a receive on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Recv().
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Recv"/> in <autoref label="sec:sys_recv"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*/
LIBSEL4_INLINE_FUNC void
seL4_Wait(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Poll" label="sel4_poll"/> @endxmlonly
* @brief Perform a non-blocking recv on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_NBRecv().
* It is useful for doing a non-blocking wait on a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_NBRecv"/> in <autoref label="sec:sys_nbrecv"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Poll(seL4_CPtr src, seL4_Word *sender);
/** @} */
#ifdef CONFIG_KERNEL_MCS
#include "syscalls_mcs.h"
#else
#include "syscalls_master.h"
#endif
/**
* @defgroup DebuggingSystemCalls

237
libsel4/include/sel4/syscalls_master.h Normal file
View file

@ -0,0 +1,237 @@
/*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(DATA61_BSD)
*/
#ifndef __LIBSEL4_MASTER_SYSCALLSH
#define __LIBSEL4_MASTER_SYSCALLSH
#include <autoconf.h>
/**
* @defgroup GeneralSystemCalls System Calls (non-MCS)
* @{
*/
/**
* @xmlonly <manual name="Send" label="sel4_send"/> @endxmlonly
* @brief Send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_send"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Recv" label="sel4_recv"/> @endxmlonly
* @brief Block until a message is received on an endpoint
*
* @xmlonly
* <docref>See <autoref label="sec:sys_recv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Recv(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Call" label="sel4_call"/> @endxmlonly
* @brief Call a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_call"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply" label="sel4_reply"/> @endxmlonly
* @brief Perform a send to a one-off reply capability stored when
* the thread was last called
*
* @xmlonly
* <docref>See <autoref label="sec:sys_reply"/></docref>
* @endxmlonly
*
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Reply(seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Non-Blocking Send" label="sel4_nbsend"/> @endxmlonly
* @brief Perform a non-blocking send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsend"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply Recv" label="sel4_replyrecv"/> @endxmlonly
* @brief Perform a reply followed by a receive in one system call
*
* @xmlonly
* <docref>See <autoref label="sec:sys_replyrecv"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender);
/**
* @xmlonly <manual name="NBRecv" label="sel4_nbrecv"/> @endxmlonly
* @brief Receive a message from an endpoint but do not block
* in the case that no messages are pending
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbrecv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBRecv(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Yield" label="sel4_yield"/> @endxmlonly
* @brief Donate the remaining timeslice to a thread of the same priority
*
* @xmlonly
* <docref>See <autoref label="sec:sys_yield"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC void
seL4_Yield(void);
/**
* @xmlonly <manual name="Signal" label="sel4_signal"/> @endxmlonly
* @brief Signal a notification
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Send().
* It is useful for signalling a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
*/
LIBSEL4_INLINE_FUNC void
seL4_Signal(seL4_CPtr dest);
/**
* @xmlonly <manual name="Wait" label="sel4_wait"/> @endxmlonly
* @brief Perform a receive on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Recv().
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Recv"/> in <autoref label="sec:sys_recv"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*/
LIBSEL4_INLINE_FUNC void
seL4_Wait(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Poll" label="sel4_poll"/> @endxmlonly
* @brief Perform a non-blocking recv on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_NBRecv().
* It is useful for doing a non-blocking wait on a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_NBRecv"/> in <autoref label="sec:sys_nbrecv"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Poll(seL4_CPtr src, seL4_Word *sender);
/** @} */
#endif /* __LIBSEL4_MASTER_SYSCALLSH */

307
libsel4/include/sel4/syscalls_mcs.h Normal file
View file

@ -0,0 +1,307 @@
/*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(DATA61_BSD)
*/
#ifndef __LIBSEL4_MCS_SYSCALLSH
#define __LIBSEL4_MCS_SYSCALLSH
#include <autoconf.h>
/**
* @defgroup MCSSystemCalls MCS System Calls
* @{
*/
/**
* @xmlonly <manual name="Send" label="sel4_mcs_send"/> @endxmlonly
* @brief Send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_send"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Recv" label="sel4_mcs_recv"/> @endxmlonly
* @brief Block until a message is received on an endpoint
*
* @xmlonly
* <docref>See <autoref label="sec:sys_recv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] reply The capability to the reply object to use on a call (only used on MCS).
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="Call" label="sel4_mcs_call"/> @endxmlonly
* @brief Call a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_call"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Non-Blocking Send" label="sel4_mcs_nbsend"/> @endxmlonly
* @brief Perform a non-blocking send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsend"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply Recv" label="sel4_mcs_replyrecv"/> @endxmlonly
* @brief Perform a reply followed by a receive in one system call
*
* @xmlonly
* <docref>See <autoref label="sec:sys_replyrecv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to perform the receive on.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @param[in] reply The capability to the reply object, which is first invoked and then used
* for the recv phase to store a new reply capability.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="NBRecv" label="sel4_mcs_nbrecv"/> @endxmlonly
* @brief Receive a message from an endpoint but do not block
* in the case that no messages are pending
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbrecv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to receive on.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] reply The capability to the reply object to use on a call.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="NBSend Recv" label="sel4_nbsendrecv"/> @endxmlonly
* @brief Non-blocking send on one capability, and a blocking recieve on another in a single
* system call.
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsendrecv"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] src The capability to receive on.
* @param[in] reply The capability to the reply object, which is first invoked and then used
* for the recv phase to store a new reply capability.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* as described in <autoref label="sec:messageinfo"/>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="NBSend Wait" label="sel4_nbsendwait"/> @endxmlonly
* @brief Non-blocking invoke of a capability and wait on another in one system call
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsendwait"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] src The capability to receive on.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* as described in <autoref label="sec:messageinfo"/>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Yield" label="sel4_mcs_yield"/> @endxmlonly
* @brief Yield the remaining timeslice. Periodic threads will not be scheduled again until their
* next sporadic replenishment.
*
* @xmlonly
* <docref>See <autoref label="sec:sys_yield"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC void
seL4_Yield(void);
/**
* @xmlonly <manual name="Wait" label="sel4_mcs_wait"/> @endxmlonly
* @brief Perform a wait on an endpoint or notification object
*
* Block on a notification or endpoint waiting for a message. No reply object is
* required for a Wait. Wait should not be paired with Call, as it does not provide
* a reply object. If Wait is paired with a Call the waiter will block after recieving
* the message.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Wait"/> in <autoref label="sec:sys_wait"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Wait(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="NBWait" label="sel4_nbwait"/> @endxmlonly
* @brief Perform a polling wait on an endpoint or notification object
*
* Poll a notification or endpoint waiting for a message. No reply object is
* required for a Wait. Wait should not be paired with Call.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_NBWait"/> in <autoref label="sec:sys_nbwait"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBWait(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Poll" label="sel4_mcs_poll"/> @endxmlonly
* @brief Perform a non-blocking recv on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_NBWait().
* It is useful for doing a non-blocking wait on a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_NBWait"/> in <autoref label="sec:sys_nbwait"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Poll(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Signal" label="sel4_mcs_signal"/> @endxmlonly
* @brief Signal a notification
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Send().
* It is useful for signalling a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
*/
LIBSEL4_INLINE_FUNC void
seL4_Signal(seL4_CPtr dest);
/** @} */
#endif /* __LIBSEL4_MCS_SYSCALLSH */

3
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
View file

@ -153,6 +153,9 @@ enum {
#define seL4_EndpointBits 4
#define seL4_NotificationBits 4
#define seL4_SchedContextBits 8
#ifdef CONFIG_KERNEL_MCS
#define seL4_ReplyBits 4
#endif
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
#define seL4_PageTableBits 12

63
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/syscalls.h
View file

@ -16,6 +16,14 @@
#include <autoconf.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
#define MCS_PARAM_DECL(r) register seL4_Word reply_reg asm(r) = reply
#define MCS_PARAM , "r"(reply_reg)
#else
#define MCS_PARAM_DECL(r)
#define MCS_PARAM
#endif
/*
* To simplify the definition of the various seL4 syscalls/syscall-wrappers we define
* some helper assembly functions. These functions are designed to cover the different
@ -43,6 +51,10 @@
* to be filled on return by the kernel. Used for directed send+receives
* where data flows both directions (e.g. seL4_Call, seL4_ReplyWait)
*
* arm_sys_send_recv: Fills all registers into the kernel and expects all of them
* to be filled on return by the kernel. Used for directed send+receives
* where data flows both directions on separate caps (e.g. seL4_NBSendRecv)
*
* arm_sys_null: Does not send any registers to the kernel or expect anything to
* be returned from the kernel. Used to trigger implicit kernel actions without
* any data (e.g. seL4_Yield)
@ -70,6 +82,7 @@ static inline void arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_ar
);
}
#ifndef CONFIG_KERNEL_MCS
static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2,
seL4_Word mr3)
{
@ -90,6 +103,7 @@ static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr
: "r"(scno)
);
}
#endif
static inline void arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg)
{
@ -106,7 +120,7 @@ static inline void arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word inf
}
static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3)
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3, LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word src_and_badge asm("r0") = src;
register seL4_Word info asm("r1");
@ -117,13 +131,15 @@ static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
register seL4_Word msg2 asm("r4");
register seL4_Word msg3 asm("r5");
MCS_PARAM_DECL("r6");
/* Perform the system call. */
register seL4_Word scno asm("r7") = sys;
asm volatile(
"swi $0"
: "=r"(msg0), "=r"(msg1), "=r"(msg2), "=r"(msg3),
"=r"(info), "+r"(src_and_badge)
: "r"(scno)
: "r"(scno) MCS_PARAM
: "memory"
);
*out_badge = src_and_badge;
@ -135,7 +151,8 @@ static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
}
static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info_arg,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3)
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3,
LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word destptr asm("r0") = dest;
register seL4_Word info asm("r1") = info_arg;
@ -147,12 +164,13 @@ static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
register seL4_Word msg3 asm("r5") = *in_out_mr3;
/* Perform the system call. */
MCS_PARAM_DECL("r6");
register seL4_Word scno asm("r7") = sys;
asm volatile(
"swi $0"
: "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
"+r"(info), "+r"(destptr)
: "r"(scno)
: "r"(scno) MCS_PARAM
: "memory"
);
*out_info = info;
@ -163,6 +181,43 @@ static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
*in_out_mr3 = msg3;
}
#ifdef CONFIG_KERNEL_MCS
static inline void arm_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_badge,
seL4_Word info_arg,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
seL4_Word *in_out_mr3, seL4_Word reply)
{
register seL4_Word src_and_badge asm("r0") = src;
register seL4_Word info asm("r1") = info_arg;
/* Load the beginning of the message info registers */
register seL4_Word msg0 asm("r2") = *in_out_mr0;
register seL4_Word msg1 asm("r3") = *in_out_mr1;
register seL4_Word msg2 asm("r4") = *in_out_mr2;
register seL4_Word msg3 asm("r5") = *in_out_mr3;
register seL4_Word reply_reg asm("r6") = reply;
register seL4_Word dest_reg asm("r8") = dest;
/* Perform the system call. */
register seL4_Word scno asm("r7") = sys;
asm volatile(
"swi $0"
: "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
"+r"(src_and_badge), "+r"(info)
: "r"(scno), "r"(reply_reg), "r"(dest_reg)
: "memory"
);
*out_badge = src_and_badge;
*out_info = info;
*in_out_mr0 = msg0;
*in_out_mr1 = msg1;
*in_out_mr2 = msg2;
*in_out_mr3 = msg3;
}
#endif
static inline void arm_sys_null(seL4_Word sys)
{
register seL4_Word scno asm("r7") = sys;

3
libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
View file

@ -126,6 +126,9 @@ enum {
#define seL4_EndpointBits 4
#define seL4_NotificationBits 5
#define seL4_SchedContextBits 8
#ifdef CONFIG_KERNEL_MCS
#define seL4_ReplyBits 5
#endif
#define seL4_PageTableBits 12
#define seL4_PageTableEntryBits 3

62
libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/syscalls.h
View file

@ -17,6 +17,14 @@
#include <sel4/functions.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
#define MCS_PARAM_DECL(r) register seL4_Word reply_reg asm(r) = reply
#define MCS_PARAM , "r"(reply_reg)
#else
#define MCS_PARAM_DECL(r)
#define MCS_PARAM
#endif
/*
* To simplify the definition of the various seL4 syscalls/syscall-wrappers we define
* some helper assembly functions. These functions are designed to cover the different
@ -44,6 +52,10 @@
* to be filled on return by the kernel. Used for directed send+receives
* where data flows both directions (e.g. seL4_Call, seL4_ReplyWait)
*
* arm_sys_nbsend_recv: Fills all registers into the kernel and expects all of them
* to be filled on return by the kernel. Used for directed send+receives
* where data flows both directions on separate caps (e.g. seL4_NBSendRecv)
*
* arm_sys_null: Does not send any registers to the kernel or expect anything to
* be returned from the kernel. Used to trigger implicit kernel actions without
* any data (e.g. seL4_Yield)
@ -71,6 +83,7 @@ static inline void arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_ar
);
}
#ifndef CONFIG_KERNEL_MCS
static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2,
seL4_Word mr3)
{
@ -91,6 +104,7 @@ static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr
: "r"(scno)
);
}
#endif
static inline void arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg)
{
@ -107,7 +121,7 @@ static inline void arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word inf
}
static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3)
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3, LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word src_and_badge asm("x0") = src;
register seL4_Word info asm("x1");
@ -117,6 +131,7 @@ static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
register seL4_Word msg1 asm("x3");
register seL4_Word msg2 asm("x4");
register seL4_Word msg3 asm("x5");
MCS_PARAM_DECL("x6");
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
@ -124,7 +139,7 @@ static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
"svc #0"
: "=r"(msg0), "=r"(msg1), "=r"(msg2), "=r"(msg3),
"=r"(info), "+r"(src_and_badge)
: "r"(scno)
: "r"(scno) MCS_PARAM
: "memory"
);
*out_badge = src_and_badge;
@ -136,7 +151,8 @@ static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
}
static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info_arg,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3)
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3,
LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word destptr asm("x0") = dest;
register seL4_Word info asm("x1") = info_arg;
@ -146,6 +162,7 @@ static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
register seL4_Word msg1 asm("x3") = *in_out_mr1;
register seL4_Word msg2 asm("x4") = *in_out_mr2;
register seL4_Word msg3 asm("x5") = *in_out_mr3;
MCS_PARAM_DECL("x6");
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
@ -153,7 +170,7 @@ static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
"svc #0"
: "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
"+r"(info), "+r"(destptr)
: "r"(scno)
: "r"(scno) MCS_PARAM
: "memory"
);
*out_info = info;
@ -164,6 +181,43 @@ static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
*in_out_mr3 = msg3;
}
#ifdef CONFIG_KERNEL_MCS
static inline void arm_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_badge,
seL4_Word info_arg,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
seL4_Word *in_out_mr3, seL4_Word reply)
{
register seL4_Word src_and_badge asm("x0") = src;
register seL4_Word info asm("x1") = info_arg;
/* Load the beginning of the message info registers */
register seL4_Word msg0 asm("x2") = *in_out_mr0;
register seL4_Word msg1 asm("x3") = *in_out_mr1;
register seL4_Word msg2 asm("x4") = *in_out_mr2;
register seL4_Word msg3 asm("x5") = *in_out_mr3;
register seL4_Word reply_reg asm("x6") = reply;
register seL4_Word dest_reg asm("x8") = dest;
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
"+r"(src_and_badge), "+r"(info)
: "r"(scno), "r"(reply_reg), "r"(dest_reg)
: "memory"
);
*out_badge = src_and_badge;
*out_info = info;
*in_out_mr0 = msg0;
*in_out_mr1 = msg1;
*in_out_mr2 = msg2;
*in_out_mr3 = msg3;
}
#endif
static inline void arm_sys_null(seL4_Word sys)
{
register seL4_Word scno asm("x7") = sys;

7
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
View file

@ -47,6 +47,9 @@
#define seL4_ASIDPoolIndexBits 10
#define seL4_WordSizeBits 2
#define seL4_SchedContextBits 8
#ifdef CONFIG_KERNEL_MCS
#define seL4_ReplyBits 4
#endif
#define seL4_HugePageBits 30 /* 1GB */
#define seL4_PDPTBits 0
@ -111,7 +114,11 @@ enum {
} seL4_UserException_Msg;
#endif /* __ASSEMBLER__ */
#ifdef CONFIG_KERNEL_MCS
#define seL4_FastMessageRegisters 1
#else
#define seL4_FastMessageRegisters 2
#endif
/* IPC buffer is 512 bytes, giving size bits of 9 */
#define seL4_IPCBufferSizeBits 9

448
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
View file

@ -27,14 +27,23 @@
* and juggle the contents of EBX as the kernel ABI uses EBX
*/
#ifdef CONFIG_KERNEL_MCS
#define MCS_COND(a,b) a
#else
#define MCS_COND(a,b) b
#endif
#if defined(__pic__)
static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, seL4_Word mr2)
/* mr2 doesn't get used on CONFIG_KERNEL_MCS */
static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1,
LIBSEL4_UNUSED seL4_Word mr2)
{
asm volatile(
"pushl %%ebp \n"
"pushl %%ebx \n"
"movl %%ecx, %%ebp \n"
MCS_COND(, "movl %%ecx, %%ebp \n")
"movl %%esp, %%ecx \n"
"movl %%edx, %%ebx \n"
"leal 1f, %%edx \n"
@ -45,11 +54,16 @@ static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, s
: "+d"(dest)
: "a"(sys),
"S"(info),
"D"(mr1),
"c"(mr2)
"D"(mr1)
#ifdef CONFIG_KERNEL_MCS
: "%ecx"
#else
, "c"(mr2)
#endif
);
}
#ifndef CONFIG_KERNEL_MCS
static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2)
{
asm volatile(
@ -70,6 +84,7 @@ static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, s
: "%edx"
);
}
#endif /* !CONFIG_KERNEL_MCS */
static inline void x86_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info)
{
@ -91,11 +106,12 @@ static inline void x86_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word inf
}
static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
seL4_Word *out_mr1, seL4_Word *out_mr2)
seL4_Word *out_mr1, MCS_COND(seL4_Word reply, seL4_Word *out_mr2))
{
asm volatile(
"pushl %%ebp \n"
"pushl %%ebx \n"
MCS_COND("movl %%ecx, %%ebp \n",)
"movl %%esp, %%ecx \n"
"movl %%edx, %%ebx \n"
"leal 1f, %%edx \n"
@ -109,7 +125,7 @@ static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
"=d"(*out_badge),
"=S"(*out_info),
"=D"(*out_mr1),
"=c"(*out_mr2)
MCS_COND("+c"(reply), "=c"(*out_mr2))
: "a"(sys),
"d"(src)
: "memory"
@ -117,7 +133,40 @@ static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
}
static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info,
seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2)
seL4_Word *out_info, seL4_Word *in_out_mr1, MCS_COND(seL4_Word reply, seL4_Word *in_out_mr2))
{
asm volatile(
"pushl %%ebp \n"
"pushl %%ebx \n"
MCS_COND("movl %%ecx, %%ebp \n",)
"movl %%esp, %%ecx \n"
"movl %%edx, %%ebx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebx, %%edx \n"
"popl %%ebx \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=S"(*out_info),
"=D"(*in_out_mr1),
"=d"(*out_badge)
MCS_COND("+c"(reply), "=c"(*in_out_mr2))
: "a"(sys),
"S"(info),
"D"(*in_out_mr1),
#ifndef CONFIG_KERNEL_MCS
"c"(*in_out_mr2),
#endif
"d"(dest)
: "memory"
);
}
#ifdef CONFIG_KERNEL_MCS
static inline void x86_sys_nbsend_wait(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word info,
seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word reply)
{
asm volatile(
"pushl %%ebp \n"
@ -135,16 +184,18 @@ static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
:
"=S"(*out_info),
"=D"(*in_out_mr1),
"=c"(*in_out_mr2),
"=d"(*out_badge)
, "+c"(reply)
: "a"(sys),
"S"(info),
"D"(*in_out_mr1),
"c"(*in_out_mr2),
"d"(dest)
"d"(src)
: "memory"
);
}
#endif /* CONFIG_KERNEL_MCS */
static inline void x86_sys_null(seL4_Word sys)
{
@ -169,7 +220,9 @@ static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, s
{
asm volatile(
"pushl %%ebp \n"
#ifndef CONFIG_KERNEL_MCS
"movl %%ecx, %%ebp \n"
#endif
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
@ -179,12 +232,17 @@ static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, s
: "a"(sys),
"b"(dest),
"S"(info),
"D"(mr1),
"c"(mr2)
: "%edx"
"D"(mr1)
#ifdef CONFIG_KERNEL_MCS
: "%ecx",
#else
, "c"(mr2):
#endif
"%edx"
);
}
#ifndef CONFIG_KERNEL_MCS
static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2)
{
asm volatile(
@ -203,6 +261,7 @@ static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, s
: "%ebx", "%edx"
);
}
#endif
static inline void x86_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info)
{
@ -222,10 +281,11 @@ static inline void x86_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word in
}
static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
seL4_Word *out_mr1, seL4_Word *out_mr2)
seL4_Word *out_mr1, MCS_COND(seL4_Word reply, seL4_Word *out_mr2))
{
asm volatile(\
"pushl %%ebp \n"
MCS_COND("movl %%ecx, %%ebp \n",)
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
@ -235,7 +295,7 @@ static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
: "=b"(*out_badge),
"=S"(*out_info),
"=D"(*out_mr1),
"=c"(*out_mr2)
MCS_COND("+c"(reply), "=c"(*out_mr2))
: "a"(sys),
"b"(src)
: "%edx", "memory"
@ -243,7 +303,7 @@ static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
}
static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info,
seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2)
seL4_Word *out_info, seL4_Word *in_out_mr1, MCS_COND(seL4_Word reply, seL4_Word *in_out_mr2))
{
asm volatile(
"pushl %%ebp \n"
@ -256,17 +316,45 @@ static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
"popl %%ebp \n"
: "=S"(*out_info),
"=D"(*in_out_mr1),
"=c"(*in_out_mr2),
"=b"(*out_badge)
"=b"(*out_badge),
MCS_COND("+c"(reply), "=c"(*in_out_mr2))
: "a"(sys),
"S"(info),
"D"(*in_out_mr1),
#ifndef CONFIG_KERNEL_MCS
"c"(*in_out_mr2),
#endif
"b"(dest)
: "%edx", "memory"
);
}
#ifdef CONFIG_KERNEL_MCS
static inline void x86_sys_nbsend_wait(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word info,
seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word reply)
{
asm volatile(
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
: "=S"(*out_info),
"=D"(*in_out_mr1),
"=b"(*out_badge),
"+c"(reply)
: "a"(sys),
"S"(info),
"D"(*in_out_mr1),
"b"(src)
: "%edx", "memory"
);
}
#endif /* CONFIG_KERNEL_MCS */
static inline void x86_sys_null(seL4_Word sys)
{
asm volatile(
@ -283,29 +371,50 @@ static inline void x86_sys_null(seL4_Word sys)
}
#endif /* defined(__pic__) */
#ifdef CONFIG_KERNEL_MCS
#define GET_MRS seL4_GetMR(0), 0
#define MAYBE_GET_MRS mr0 != seL4_Null ? *mr0 : 0
#define MR_ARGS seL4_Word *mr0
#define RECV_MRS &mr0
#define REPLY &mr0
#else
#define MCS_MAYBE_GET_MR1 seL4_GetMR(1)
#define MAYBE_GET_MRS mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0
#define MR_ARGS
#define RECV_MRS &mr0, &mr1
#endif
LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1)));
}
LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0)
#else
LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1)
#endif
{
x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0);
x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, MCS_COND(0,
mr1 != seL4_Null ? *mr1 : 0));
}
LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1)));
}
LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0)
#else
LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1)
#endif
{
x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0);
x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, MCS_COND(0,
mr1 != seL4_Null ? *mr1 : 0));
}
#ifndef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo)
{
x86_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
@ -316,24 +425,30 @@ LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
{
x86_sys_reply(seL4_SysReply, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0);
}
#endif /* !CONFIG_KERNEL_MCS */
LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest)
{
x86_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
LIBSEL4_UNUSED seL4_Word mr1;
x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, &mr1);
x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1));
seL4_SetMR(0, mr0);
#ifndef CONFIG_KERNEL_MCS
seL4_SetMR(1, mr1);
#endif
if (sender) {
*sender = badge;
}
@ -341,22 +456,30 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sende
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
LIBSEL4_UNUSED seL4_Word msg1 = 0;
x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1);
x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, MCS_COND(reply, &msg1));
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
#ifndef CONFIG_KERNEL_MCS
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
#endif
if (sender) {
*sender = badge;
@ -365,17 +488,23 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
LIBSEL4_UNUSED seL4_Word mr1;
x86_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, &mr1);
x86_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1));
seL4_SetMR(0, mr0);
#ifndef CONFIG_KERNEL_MCS
seL4_SetMR(1, mr1);
#endif
if (sender) {
*sender = badge;
@ -384,57 +513,133 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sen
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &mr0, 0);
seL4_SetMR(0, mr0);
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, 0);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
x86_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &mr0, 0);
seL4_SetMR(0, mr0);
if (sender) {
*sender = badge;
}
return info;
}
#endif /* CONFIG_KERNEL_MCS */
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
seL4_MessageInfo_t info;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1));
x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, &mr1);
x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, MCS_COND(0, &mr1));
seL4_SetMR(0, mr0);
#ifndef CONFIG_KERNEL_MCS
seL4_SetMR(1, mr1);
#endif
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
#endif
{
seL4_MessageInfo_t info;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
LIBSEL4_UNUSED seL4_Word msg1 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
#ifndef CONFIG_KERNEL_MCS
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
#endif
x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1);
x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, MCS_COND(0, &msg1));
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
#ifndef CONFIG_KERNEL_MCS
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
#endif
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1));
x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0, &mr1);
x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0,
MCS_COND(reply, &mr1));
seL4_SetMR(0, mr0);
#ifndef CONFIG_KERNEL_MCS
seL4_SetMR(1, mr1);
#endif
if (sender) {
*sender = badge;
@ -443,30 +648,90 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_Messa
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
LIBSEL4_UNUSED seL4_Word msg1 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
#ifndef CONFIG_KERNEL_MCS
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1);
#endif
x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, MCS_COND(0, &msg1));
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
#ifndef CONFIG_KERNEL_MCS
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
#endif
if (sender) {
*sender = badge;
}
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src,
seL4_Word *sender, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
/* no spare registers on ia32 -> must use ipc buffer */
seL4_SetUserData(dest);
x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &mr0, reply);
seL4_SetMR(0, mr0);
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src,
seL4_Word *sender,
seL4_Word *mr0, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
/* no spare registers on ia32 -> must use ipc buffer */
seL4_SetUserData(dest);
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, reply);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (sender) {
*sender = badge;
@ -475,6 +740,50 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src,
seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
x86_sys_nbsend_wait(seL4_SysNBSendWait, src, &badge, msgInfo.words[0], &info.words[0], &mr0, dest);
seL4_SetMR(0, mr0);
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src,
seL4_Word *sender,
seL4_Word *mr0)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
x86_sys_nbsend_wait(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, dest);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (sender) {
*sender = badge;
}
return info;
}
#endif /* CONFIG_KERNEL_MCS */
LIBSEL4_INLINE_FUNC void seL4_Yield(void)
{
x86_sys_null(seL4_SysYield);
@ -487,12 +796,14 @@ LIBSEL4_INLINE_FUNC seL4_Word seL4_VMEnter(seL4_Word *sender)
seL4_Word fault;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1));
x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1);
x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, MCS_COND(0, &mr1));
seL4_SetMR(0, mr0);
#ifndef CONFIG_KERNEL_MCS
seL4_SetMR(1, mr1);
#endif
if (!fault && sender) {
*sender = badge;
}
@ -506,9 +817,9 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
LIBSEL4_UNUSED seL4_Word unused3 = 0;
x86_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3);
x86_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3));
}
LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
@ -516,9 +827,9 @@ LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
LIBSEL4_UNUSED seL4_Word unused3 = 0;
x86_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3);
x86_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3));
}
#endif
@ -543,9 +854,9 @@ LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
LIBSEL4_UNUSED seL4_Word unused2 = 0;
x86_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2);
x86_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, MCS_COND(0, &unused2));
return (seL4_Uint32)cap;
}
@ -557,9 +868,9 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
LIBSEL4_UNUSED seL4_Word unused3 = 0;
x86_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3);
x86_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3));
}
#endif
@ -576,6 +887,10 @@ LIBSEL4_INLINE_FUNC void seL4_X86DangerousWRMSR(seL4_Uint32 msr, seL4_Uint64 val
{
seL4_Uint32 value_low = value & 0xffffffff;
seL4_Uint32 value_high = value >> 32;
#ifdef CONFIG_KERNEL_MCS
/* MR1 doesn't get passed through MRs on CONFIG_KERNEL_MCS */
seL4_SetMR(1, value_high);
#endif
x86_sys_send(seL4_SysX86DangerousWRMSR, msr, 0, value_low, value_high);
}
LIBSEL4_INLINE_FUNC seL4_Uint64 seL4_X86DangerousRDMSR(seL4_Word msr)
@ -583,7 +898,12 @@ LIBSEL4_INLINE_FUNC seL4_Uint64 seL4_X86DangerousRDMSR(seL4_Word msr)
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word low, high;
x86_sys_recv(seL4_SysX86DangerousRDMSR, msr, &unused0, &unused1, &low, &high);
x86_sys_recv(seL4_SysX86DangerousRDMSR, msr, &unused0, &unused1, &low, MCS_COND(0, &high));
#ifdef CONFIG_KERNEL_MCS
/* MR1 doesn't get passed through MRs on CONFIG_KERNEL_MCS */
*high = seL4_GetMR(1);
#endif
return ((seL4_Uint64)low) | ((seL4_Uint64)high << 32);
}
#endif
@ -593,11 +913,11 @@ LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
LIBSEL4_UNUSED seL4_Word unused2 = 0;
seL4_Word ret;
x86_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2);
x86_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, MCS_COND(0, &unused2));
return (seL4_Error)ret;
}
@ -606,9 +926,9 @@ LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
LIBSEL4_UNUSED seL4_Word unused2 = 0;
seL4_Word index_ret;
x86_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2);
x86_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, MCS_COND(0, &unused2));
return (seL4_Word)index_ret;
}
@ -617,9 +937,9 @@ LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
LIBSEL4_UNUSED seL4_Word unused2 = 0;
x86_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2);
x86_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, MCS_COND(0, &unused2));
return (seL4_Error) frame_cptr;
}
@ -643,9 +963,10 @@ LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
LIBSEL4_UNUSED seL4_Word unused3 = 0;
x86_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3);
x86_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, MCS_COND(0,
&unused3));
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
@ -653,9 +974,10 @@ LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
LIBSEL4_UNUSED seL4_Word unused3 = 0;
x86_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3);
x86_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, MCS_COND(0,
&unused3));
}
#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
#endif /* CONFIG_ENABLE_BENCHMARKS */

3
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
View file

@ -61,6 +61,9 @@
#define seL4_ASIDPoolBits 12
#define seL4_ASIDPoolIndexBits 9
#define seL4_SchedContextBits 8
#ifdef CONFIG_KERNEL_MCS
#define seL4_ReplyBits 5
#endif
/* Untyped size limits */
#define seL4_MinUntypedBits 4

305
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
View file

@ -14,6 +14,11 @@
#define __LIBSEL4_SEL4_SEL4_ARCH_SYSCALLS_H_
#include <autoconf.h>
#ifdef CONFIG_KERNEL_MCS
#define LIBSEL4_MCS_REPLY reply
#else
#define LIBSEL4_MCS_REPLY 0
#endif
#if defined(CONFIG_SYSENTER)
#include <sel4/sel4_arch/syscalls_sysenter.h>
@ -55,6 +60,7 @@ LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t m
);
}
#ifndef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo)
{
x64_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
@ -70,13 +76,18 @@ LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
(mr3 != seL4_Null) ? *mr3 : 0
);
}
#endif
LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest)
{
x64_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 1).words[0]);
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -85,7 +96,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sende
seL4_Word mr2;
seL4_Word mr3;
x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3);
x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3, LIBSEL4_MCS_REPLY);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
@ -99,8 +110,13 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sende
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -109,7 +125,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word
seL4_Word msg2;
seL4_Word msg3;
x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
if (mr0 != seL4_Null) {
*mr0 = msg0;
@ -131,7 +147,11 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -140,7 +160,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sen
seL4_Word mr2;
seL4_Word mr3;
x64_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3);
x64_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3, LIBSEL4_MCS_REPLY);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
@ -154,6 +174,86 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sen
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
seL4_Word mr2;
seL4_Word mr3;
x64_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3, 0);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
seL4_SetMR(2, mr2);
seL4_SetMR(3, mr3);
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
x64_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
seL4_Word mr2;
seL4_Word mr3;
x64_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &mr0, &mr1, &mr2, &mr3, 0);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
seL4_SetMR(2, mr2);
seL4_SetMR(3, mr3);
if (sender) {
*sender = badge;
}
return info;
}
#endif
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
@ -163,7 +263,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInf
seL4_Word mr2 = seL4_GetMR(2);
seL4_Word mr3 = seL4_GetMR(3);
x64_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, &mr1, &mr2, &mr3);
x64_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, &mr1, &mr2, &mr3, 0);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
@ -195,7 +295,7 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_Mes
msg3 = *mr3;
}
x64_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
x64_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
if (mr0 != seL4_Null) {
*mr0 = msg0;
@ -213,7 +313,12 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_Mes
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -222,7 +327,8 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_Messa
seL4_Word mr2 = seL4_GetMR(2);
seL4_Word mr3 = seL4_GetMR(3);
x64_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0, &mr1, &mr2, &mr3);
x64_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0, &mr1, &mr2, &mr3,
LIBSEL4_MCS_REPLY);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
@ -236,9 +342,15 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_Messa
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
@ -260,7 +372,8 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL
msg3 = *mr3;
}
x64_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
x64_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
LIBSEL4_MCS_REPLY);
if (mr0 != seL4_Null) {
*mr0 = msg0;
@ -282,6 +395,164 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
seL4_Word mr2 = seL4_GetMR(2);
seL4_Word mr3 = seL4_GetMR(3);
x64_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &mr0, &mr1, &mr2, &mr3,
reply);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
seL4_SetMR(2, mr2);
seL4_SetMR(3, mr3);
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
x64_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
reply);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
seL4_Word mr2 = seL4_GetMR(2);
seL4_Word mr3 = seL4_GetMR(3);
/* NBSendWait sends to the supplied reply cap, not to a supplied
* notification object. So the "dest" argument to x64_sys_nbsend_recv is 0.
*
* See handleSyscall() in the kernel, especially the differences between
* SysNBSendRecv and SysNBSendWait.
*/
x64_sys_nbsend_recv(seL4_SysNBSendWait, 0, src, &badge, msgInfo.words[0], &info.words[0], &mr0, &mr1, &mr2, &mr3, dest);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
seL4_SetMR(2, mr2);
seL4_SetMR(3, mr3);
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
/* See handleSyscall, specifically `SysReplyRecv`.
*
* This syscall (SysReplyRecv) sends to the reply cap passed in the replyRegister, and then
* performs a receive on the capability in the capRegister, so this "src" argument is not
* used.
*/
(void)src;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
x64_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, dest);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
if (sender) {
*sender = badge;
}
return info;
}
#endif
LIBSEL4_INLINE_FUNC void seL4_Yield(void)
{
x64_sys_null(seL4_SysYield);
@ -298,7 +569,7 @@ LIBSEL4_INLINE_FUNC seL4_Word seL4_VMEnter(seL4_Word *sender)
seL4_Word mr2 = seL4_GetMR(2);
seL4_Word mr3 = seL4_GetMR(3);
x64_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1, &mr2, &mr3);
x64_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1, &mr2, &mr3, 0);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
@ -321,7 +592,7 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
x64_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
x64_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
@ -333,7 +604,7 @@ LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
x64_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
x64_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
#endif
@ -380,7 +651,7 @@ LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
x64_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
x64_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Uint32)cap;
}
#endif
@ -399,7 +670,7 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
x64_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
x64_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
#endif
@ -422,7 +693,7 @@ LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void)
seL4_Word ret;
x64_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
x64_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Error)ret;
}
@ -435,7 +706,7 @@ LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void)
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word index_ret;
x64_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
x64_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Word)index_ret;
}
@ -449,7 +720,7 @@ LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
seL4_Word unused4 = 0;
x64_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3,
&unused4);
&unused4, 0);
return (seL4_Error) frame_cptr;
}
@ -477,7 +748,7 @@ LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
seL4_Word unused5 = 0;
x64_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
&unused5);
&unused5, 0);
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
@ -490,7 +761,7 @@ LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr
seL4_Word unused5 = 0;
x64_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3,
&unused4, &unused5);
&unused4, &unused5, 0);
}
#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
#endif /* CONFIG_ENABLE_BENCHMARKS */

62
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_syscall.h
View file

@ -17,6 +17,14 @@
#include <sel4/functions.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
#define MCS_REPLY_DECL register seL4_Word reply_reg asm("r12") = reply
#define MCS_REPLY ,"r"(reply_reg)
#else
#define MCS_REPLY_DECL
#define MCS_REPLY
#endif
static inline void x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word msg0, seL4_Word msg1,
seL4_Word msg2, seL4_Word msg3)
{
@ -37,10 +45,11 @@ static inline void x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, s
"r"(mr1),
"r"(mr2),
"r"(mr3)
: "%rcx", "%rbx", "r11"
: "%rbx", "%rcx", "%r11"
);
}
#ifndef CONFIG_KERNEL_MCS
static inline void x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0, seL4_Word msg1, seL4_Word msg2,
seL4_Word msg3)
{
@ -63,6 +72,7 @@ static inline void x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0,
: "%rbx", "%rcx", "%r11"
);
}
#endif /* CONFIG_KERNEL_MCS */
static inline void x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info)
{
@ -79,12 +89,14 @@ static inline void x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word in
}
static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3)
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3,
LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word mr0 asm("r10");
register seL4_Word mr1 asm("r8");
register seL4_Word mr2 asm("r9");
register seL4_Word mr3 asm("r15");
MCS_REPLY_DECL;
asm volatile(
"movq %%rsp, %%rbx \n"
@ -98,6 +110,7 @@ static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
"=r"(mr3)
: "d"(sys),
"D"(src)
MCS_REPLY
: "%rcx", "%rbx", "r11", "memory"
);
*out_mr0 = mr0;
@ -107,12 +120,14 @@ static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
}
static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_dest, seL4_Word info,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3)
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3,
LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word mr0 asm("r10") = *in_out_mr0;
register seL4_Word mr1 asm("r8") = *in_out_mr1;
register seL4_Word mr2 asm("r9") = *in_out_mr2;
register seL4_Word mr3 asm("r15") = *in_out_mr3;
MCS_REPLY_DECL;
asm volatile(
"movq %%rsp, %%rbx \n"
@ -131,6 +146,7 @@ static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
"r"(mr1),
"r"(mr2),
"r"(mr3)
MCS_REPLY
: "%rcx", "%rbx", "r11", "memory"
);
*in_out_mr0 = mr0;
@ -139,6 +155,46 @@ static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
*in_out_mr3 = mr3;
}
#ifdef CONFIG_KERNEL_MCS
static inline void x64_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_dest,
seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
seL4_Word *in_out_mr3, seL4_Word reply)
{
register seL4_Word mr0 asm("r10") = *in_out_mr0;
register seL4_Word mr1 asm("r8") = *in_out_mr1;
register seL4_Word mr2 asm("r9") = *in_out_mr2;
register seL4_Word mr3 asm("r15") = *in_out_mr3;
register seL4_Word reply_reg asm("r12") = reply;
register seL4_Word dest_reg asm("r13") = dest;
asm volatile(
"movq %%rsp, %%rbx \n"
"syscall \n"
"movq %%rbx, %%rsp \n"
: "=S"(*out_info),
"=r"(mr0),
"=r"(mr1),
"=r"(mr2),
"=r"(mr3),
"=D"(*out_dest)
: "d"(sys),
"D"(src),
"S"(info),
"r"(mr0),
"r"(mr1),
"r"(mr2),
"r"(mr3),
"r"(reply_reg),
"r"(dest_reg)
: "%rcx", "%rbx", "r11", "memory"
);
*in_out_mr0 = mr0;
*in_out_mr1 = mr1;
*in_out_mr2 = mr2;
*in_out_mr3 = mr3;
}
#endif /* CONFIG_KERNEL_MCS */
static inline void x64_sys_null(seL4_Word sys)
{
asm volatile(

62
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_sysenter.h
View file

@ -17,6 +17,15 @@
#include <sel4/functions.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
#define MCS_PARAM_DECL(r) register seL4_Word reply_reg asm(r) = reply;
#define MCS_PARAM , "r"(reply_reg)
#else
#define MCS_PARAM_DECL(r)
#define MCS_PARAM
#endif
static inline void x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word msg0, seL4_Word msg1,
seL4_Word msg2, seL4_Word msg3)
{
@ -42,6 +51,7 @@ static inline void x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, s
);
}
#ifndef CONFIG_KERNEL_MCS
static inline void x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0, seL4_Word msg1, seL4_Word msg2,
seL4_Word msg3)
{
@ -65,6 +75,7 @@ static inline void x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0,
: "%rdx", "%rcx"
);
}
#endif
static inline void x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info)
{
@ -82,12 +93,13 @@ static inline void x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word in
}
static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3)
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3, LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word mr0 asm("r10");
register seL4_Word mr1 asm("r8");
register seL4_Word mr2 asm("r9");
register seL4_Word mr3 asm("r15");
MCS_PARAM_DECL("r12");
asm volatile(
"movq %%rsp, %%rcx \n"
@ -101,7 +113,8 @@ static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
"=r"(mr2),
"=r"(mr3)
: "a"(sys),
"D"(src)
"D"(src),
MCS_PARAM
: "%rcx", "%rdx", "memory"
);
@ -112,12 +125,14 @@ static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_bad
}
static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_dest, seL4_Word info,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3)
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3,
LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word mr0 asm("r10") = *in_out_mr0;
register seL4_Word mr1 asm("r8") = *in_out_mr1;
register seL4_Word mr2 asm("r9") = *in_out_mr2;
register seL4_Word mr3 asm("r15") = *in_out_mr3;
MCS_PARAM_DECL("r12");
asm volatile(
"movq %%rsp, %%rcx \n"
@ -136,7 +151,8 @@ static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
"r"(mr0),
"r"(mr1),
"r"(mr2),
"r"(mr3)
"r"(mr3),
MCS_PARAM
: "%rcx", "%rdx", "memory"
);
@ -146,6 +162,44 @@ static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *o
*in_out_mr3 = mr3;
}
#ifdef CONFIG_KERNEL_MCS
static inline void x64_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_dest,
seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
seL4_Word *in_out_mr3, seL4_Word reply)
{
register seL4_Word mr0 asm("r10") = *in_out_mr0;
register seL4_Word mr1 asm("r8") = *in_out_mr1;
register seL4_Word mr2 asm("r9") = *in_out_mr2;
register seL4_Word mr3 asm("r15") = *in_out_mr3;
register seL4_Word reply_reg asm("r12") = reply;
register seL4_Word dest_reg asm("r13") = dest;
asm volatile(
"movq %%rsp, %%rcx \n"
"leaq 1f, %%rdx \n"
"1: \n"
"sysenter \n"
: "=S"(*out_info),
"=r"(mr0),
"=r"(mr1),
"=D"(*out_dest)
: "a"(sys),
"D"(src),
"S"(info),
"r"(mr0),
"r"(mr1),
"r"(reply_reg),
"r"(dest_reg)
: "%rcx", "%rdx", "memory"
);
*in_out_mr0 = mr0;
*in_out_mr1 = mr1;
*in_out_mr2 = mr2;
*in_out_mr3 = mr3;
}
#endif
static inline void x64_sys_null(seL4_Word sys)
{
asm volatile(

16
libsel4/tools/syscall_stub_gen.py
View file

@ -66,6 +66,7 @@ MESSAGE_REGISTERS_FOR_ARCH = {
"aarch32": 4,
"aarch64": 4,
"ia32": 2,
"ia32-mcs": 1,
"x86_64": 4,
"arm_hyp": 4,
"riscv32": 4,
@ -591,13 +592,16 @@ def generate_result_struct(interface_name, method_name, output_params):
return "\n".join(result)
def generate_stub(arch, wordsize, interface_name, method_name, method_id, input_params, output_params, structs, use_only_ipc_buffer, comment):
def generate_stub(arch, wordsize, interface_name, method_name, method_id, input_params, output_params, structs, use_only_ipc_buffer, comment, mcs):
result = []
if use_only_ipc_buffer:
num_mrs = 0
else:
num_mrs = MESSAGE_REGISTERS_FOR_ARCH[arch]
if mcs and "%s-mcs" % arch in MESSAGE_REGISTERS_FOR_ARCH:
num_mrs = MESSAGE_REGISTERS_FOR_ARCH["%s-mcs" % arch]
else:
num_mrs = MESSAGE_REGISTERS_FOR_ARCH[arch]
# Split out cap parameters and standard parameters
standard_params = []
@ -933,7 +937,7 @@ def parse_xml_file(input_file, valid_types):
return (methods, structs, api)
def generate_stub_file(arch, wordsize, input_files, output_file, use_only_ipc_buffer):
def generate_stub_file(arch, wordsize, input_files, output_file, use_only_ipc_buffer, mcs):
"""
Generate a header file containing system call stubs for seL4.
"""
@ -1011,7 +1015,7 @@ def generate_stub_file(arch, wordsize, input_files, output_file, use_only_ipc_bu
if condition != "":
result.append("#if %s" % condition)
result.append(generate_stub(arch, wordsize, interface_name, method_name,
method_id, inputs, outputs, structs, use_only_ipc_buffer, comment))
method_id, inputs, outputs, structs, use_only_ipc_buffer, comment, mcs))
if condition != "":
result.append("#endif")
@ -1040,6 +1044,8 @@ def process_args():
help="Use IPC buffer exclusively, i.e. do not pass syscall arguments by registers. (default: %(default)s)")
parser.add_argument("-a", "--arch", dest="arch", required=True, choices=WORD_SIZE_BITS_ARCH,
help="Architecture to generate stubs for.")
parser.add_argument("--mcs", dest="mcs", action="store_true",
help="Generate MCS api.")
wsizegroup = parser.add_mutually_exclusive_group()
wsizegroup.add_argument("-w", "--word-size", dest="wsize",
@ -1082,7 +1088,7 @@ def main():
sys.exit(2)
# Generate the stubs.
generate_stub_file(args.arch, wordsize, args.files, args.output, args.buffer)
generate_stub_file(args.arch, wordsize, args.files, args.output, args.buffer, args.mcs)
if __name__ == "__main__":

9
manual/Makefile
View file

@ -111,8 +111,13 @@ endif
.PHONY: doxygen generated-headers generated-latex generated-markdown
# We call doxygen twice below while excluding either syscalls_master.h or syscalls_mcs.h.
# Without excluding one of the two files, the doc strings get merged in inconsistent ways
# and lead to bad output in the manual. If there is a better way to support duplicates
# then it could be used instead.
doxygen: generated-headers
${Q}$(doxygen)
( cat Doxyfile ; echo "EXCLUDE = ./../libsel4/include/sel4/syscalls_master.h" ) | $(doxygen) -
( cat Doxyfile ; echo "EXCLUDE = ./../libsel4/include/sel4/syscalls_mcs.h" ) | $(doxygen) -
# Xml files generated by doxygen
${DoxygenXml}/%.xml: doxygen
@ -129,6 +134,7 @@ ${GeneratedLatexDir}/%.tex: ${DoxygenXml}/group__%.xml
# Collect generated latex files into single rule
generated-latex: ${GeneratedLatexDir}/GeneralSystemCalls.tex \
${GeneratedLatexDir}/MCSSystemCalls.tex \
${GeneratedLatexDir}/DebuggingSystemCalls.tex \
${GeneratedLatexDir}/BenchmarkingSystemCalls.tex \
${GeneratedLatexDir}/X86SystemCalls.tex \
@ -148,6 +154,7 @@ ${GeneratedMarkdownDir}/%.md: ${DoxygenXml}/group__%.xml Makefile
# Collect generated markdown files into single rule
generated-markdown: ${GeneratedMarkdownDir}/GeneralSystemCalls.md \
${GeneratedMarkdownDir}/MCSSystemCalls.md \
${GeneratedMarkdownDir}/DebuggingSystemCalls.md \
${GeneratedMarkdownDir}/BenchmarkingSystemCalls.md \
${GeneratedMarkdownDir}/X86SystemCalls.md \

5
manual/parts/api.tex
View file

@ -258,8 +258,13 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request.
\section{System Calls}
\subsection{General System Calls}
This section provides the system call API for non-MCS kernel configurations.
\inputgeneratedapidoc{GeneralSystemCalls}
\clearpage
\subsection{General System Calls (MCS) }
This section provides the system call API for MCS kernel configurations.
\inputgeneratedapidoc{MCSSystemCalls}
\clearpage
\subsection{Debugging System Calls}
\inputgeneratedapidoc{DebuggingSystemCalls}

122
src/api/syscall.c
View file

@ -290,10 +290,13 @@ exception_t handleVMFaultEvent(vm_fault_type_t vm_faultType)
}
#ifdef CONFIG_KERNEL_MCS
static exception_t handleInvocation(bool_t isCall, bool_t isBlocking, bool_t canDonate, cptr_t cptr)
#else
static exception_t handleInvocation(bool_t isCall, bool_t isBlocking)
#endif
{
seL4_MessageInfo_t info;
cptr_t cptr;
lookupCapAndSlot_ret_t lu_ret;
word_t *buffer;
exception_t status;
@ -303,7 +306,9 @@ static exception_t handleInvocation(bool_t isCall, bool_t isBlocking)
thread = NODE_STATE(ksCurThread);
info = messageInfoFromWord(getRegister(thread, msgInfoRegister));
cptr = getRegister(thread, capRegister);
#ifndef CONFIG_KERNEL_MCS
cptr_t cptr = getRegister(thread, capRegister);
#endif
/* faulting section */
lu_ret = lookupCapAndSlot(thread, cptr);
@ -336,10 +341,17 @@ static exception_t handleInvocation(bool_t isCall, bool_t isBlocking)
if (unlikely(length > n_msgRegisters && !buffer)) {
length = n_msgRegisters;
}
#ifdef CONFIG_KERNEL_MCS
status = decodeInvocation(seL4_MessageInfo_get_label(info), length,
cptr, lu_ret.slot, lu_ret.cap,
current_extra_caps, isBlocking, isCall,
canDonate, buffer);
#else
status = decodeInvocation(seL4_MessageInfo_get_label(info), length,
cptr, lu_ret.slot, lu_ret.cap,
current_extra_caps, isBlocking, isCall,
buffer);
#endif
if (unlikely(status == EXCEPTION_PREEMPTED)) {
return status;
@ -363,6 +375,29 @@ static exception_t handleInvocation(bool_t isCall, bool_t isBlocking)
return EXCEPTION_NONE;
}
#ifdef CONFIG_KERNEL_MCS
static inline lookupCap_ret_t lookupReply(void)
{
word_t replyCPtr = getRegister(NODE_STATE(ksCurThread), replyRegister);
lookupCap_ret_t lu_ret = lookupCap(NODE_STATE(ksCurThread), replyCPtr);
if (unlikely(lu_ret.status != EXCEPTION_NONE)) {
userError("Reply cap lookup failed");
current_fault = seL4_Fault_CapFault_new(replyCPtr, true);
handleFault(NODE_STATE(ksCurThread));
return lu_ret;
}
if (unlikely(cap_get_capType(lu_ret.cap) != cap_reply_cap)) {
userError("Cap in reply slot is not a reply");
current_fault = seL4_Fault_CapFault_new(replyCPtr, true);
handleFault(NODE_STATE(ksCurThread));
lu_ret.status = EXCEPTION_FAULT;
return lu_ret;
}
return lu_ret;
}
#else
static void handleReply(void)
{
cte_t *callerSlot;
@ -397,8 +432,13 @@ static void handleReply(void)
fail("handleReply: invalid caller cap");
}
#endif
#ifdef CONFIG_KERNEL_MCS
static void handleRecv(bool_t isBlocking, bool_t canReply)
#else
static void handleRecv(bool_t isBlocking)
#endif
{
word_t epCPtr;
lookupCap_ret_t lu_ret;
@ -423,8 +463,22 @@ static void handleRecv(bool_t isBlocking)
break;
}
#ifdef CONFIG_KERNEL_MCS
cap_t ep_cap = lu_ret.cap;
cap_t reply_cap = cap_null_cap_new();
if (canReply) {
lu_ret = lookupReply();
if (lu_ret.status != EXCEPTION_NONE) {
return;
} else {
reply_cap = lu_ret.cap;
}
}
receiveIPC(NODE_STATE(ksCurThread), ep_cap, isBlocking, reply_cap);
#else
deleteCallerCap(NODE_STATE(ksCurThread));
receiveIPC(NODE_STATE(ksCurThread), lu_ret.cap, isBlocking);
#endif
break;
case cap_notification_cap: {
@ -459,7 +513,9 @@ static inline void mcsIRQ(irq_t irq)
}
}
#else
#define handleRecv(isBlocking, canReply) handleRecv(isBlocking)
#define mcsIRQ(irq)
#define handleInvocation(isCall, isBlocking, canDonate, cptr) handleInvocation(isCall, isBlocking)
#endif
@ -473,6 +529,7 @@ static void handleYield(void)
/* we just charged all of the time to the yielding thread */
NODE_STATE(ksConsumed) = 0;
endTimeslice();
rescheduleRequired();
#else
tcbSchedDequeue(NODE_STATE(ksCurThread));
SCHED_APPEND_CURRENT_TCB;
@ -488,7 +545,7 @@ exception_t handleSyscall(syscall_t syscall)
switch (syscall)
{
case SysSend:
ret = handleInvocation(false, true);
ret = handleInvocation(false, true, false, getRegister(NODE_STATE(ksCurThread), capRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
if (irq != irqInvalid) {
@ -501,7 +558,7 @@ exception_t handleSyscall(syscall_t syscall)
break;
case SysNBSend:
ret = handleInvocation(false, false);
ret = handleInvocation(false, false, false, getRegister(NODE_STATE(ksCurThread), capRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
if (irq != irqInvalid) {
@ -513,7 +570,7 @@ exception_t handleSyscall(syscall_t syscall)
break;
case SysCall:
ret = handleInvocation(true, true);
ret = handleInvocation(true, true, true, getRegister(NODE_STATE(ksCurThread), capRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
if (irq != irqInvalid) {
@ -525,20 +582,67 @@ exception_t handleSyscall(syscall_t syscall)
break;
case SysRecv:
handleRecv(true);
handleRecv(true, true);
break;
#ifndef CONFIG_KERNEL_MCS
case SysReply:
handleReply();
break;
case SysReplyRecv:
handleReply();
handleRecv(true);
handleRecv(true, true);
break;
#else /* CONFIG_KERNEL_MCS */
case SysWait:
handleRecv(true, false);
break;
case SysNBWait:
handleRecv(false, false);
break;
case SysReplyRecv: {
cptr_t reply = getRegister(NODE_STATE(ksCurThread), replyRegister);
ret = handleInvocation(false, false, true, reply);
/* reply cannot error and is not preemptible */
assert(ret == EXCEPTION_NONE);
handleRecv(true, true);
break;
}
case SysNBSendRecv: {
cptr_t dest = getNBSendRecvDest();
ret = handleInvocation(false, false, true, dest);
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
if (irq != irqInvalid) {
mcsIRQ(irq);
handleInterrupt(irq);
Arch_finaliseInterrupt();
}
break;
}
handleRecv(true, true);
break;
}
case SysNBSendWait:
ret = handleInvocation(false, false, true, getRegister(NODE_STATE(ksCurThread), replyRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
if (irq != irqInvalid) {
mcsIRQ(irq);
handleInterrupt(irq);
Arch_finaliseInterrupt();
}
break;
}
handleRecv(true, false);
break;
#endif
case SysNBRecv:
handleRecv(false);
handleRecv(false, true);
break;
case SysYield:

6
src/arch/arm/32/machine/registerset.c
View file

@ -37,3 +37,9 @@ compile_assert(
sizeof(gpRegisters) / sizeof(gpRegisters[0]) == n_gpRegisters
);
#ifdef CONFIG_KERNEL_MCS
word_t getNBSendRecvDest(void)
{
return getRegister(NODE_STATE(ksCurThread), nbsendRecvDest);
}
#endif

6
src/arch/arm/32/traps.S
View file

@ -85,9 +85,13 @@ BEGIN_FUNC(arm_swi_syscall)
#endif /* CONFIG_ARCH_ARM_V6 */
/* Load system call number as a c_handle_syscall argument. r0 and r1 are passed
* unmodified (cptr and msgInfo) respectively.
* unmodified (cptr and msgInfo) respectively. On MCS configurations we also
* pass the reply cptr in r3.
*/
mov r2, r7
#ifdef CONFIG_KERNEL_MCS
mov r3, r6
#endif
b c_handle_syscall
END_FUNC(arm_swi_syscall)

7
src/arch/arm/64/machine/registerset.c
View file

@ -39,3 +39,10 @@ compile_assert(
consistent_gp_registers,
sizeof(gpRegisters) / sizeof(gpRegisters[0]) == n_gpRegisters
);
#ifdef CONFIG_KERNEL_MCS
word_t getNBSendRecvDest(void)
{
return getRegister(NODE_STATE(ksCurThread), nbsendRecvDest);
}
#endif

3
src/arch/arm/64/traps.S
View file

@ -203,6 +203,9 @@ lel_syscall:
lsp_i x19
mov x2, x7
#ifdef CONFIG_KERNEL_MCS
mov x3, x6
#endif
b c_handle_syscall
el0_enfp:

8
src/arch/arm/c_traps.c
View file

@ -121,7 +121,11 @@ void NORETURN slowpath(syscall_t syscall)
UNREACHABLE();
}
#ifdef CONFIG_KERNEL_MCS
void VISIBLE c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall, word_t reply)
#else
void VISIBLE c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
#endif
{
NODE_LOCK_SYS;
@ -136,7 +140,11 @@ void VISIBLE c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
fastpath_call(cptr, msgInfo);
UNREACHABLE();
} else if (syscall == SysReplyRecv) {
#ifdef CONFIG_KERNEL_MCS
fastpath_reply_recv(cptr, msgInfo, reply);
#else
fastpath_reply_recv(cptr, msgInfo);
#endif
UNREACHABLE();
}
#endif /* CONFIG_FASTPATH */

17
src/arch/x86/32/machine/registerset.c
View file

@ -17,7 +17,10 @@
#include <machine/debug.h>
const register_t msgRegisters[] = {
EDI, EBP
EDI,
#ifndef CONFIG_KERNEL_MCS
EBP
#endif
};
compile_assert(
consistent_message_registers,
@ -56,3 +59,15 @@ word_t Mode_sanitiseRegister(register_t reg, word_t v)
{
return v;
}
#ifdef CONFIG_KERNEL_MCS
word_t getNBSendRecvDest(void)
{
seL4_IPCBuffer *buffer = (seL4_IPCBuffer *) lookupIPCBuffer(false, NODE_STATE(ksCurThread));
if (buffer != NULL) {
return buffer->userData;
} else {
return 0;
}
}
#endif

5
src/arch/x86/32/traps.S
View file

@ -532,7 +532,7 @@ BEGIN_FUNC(handle_syscall)
pushl %edx # NextIP := EDX
pushl $-1 # save Error (-1 means we entered via syscall)
pushl %edx # save FaultIP (passed in EDX)
pushl %ebp # save EBP (message register)
pushl %ebp # save EBP (reply register)
pushl %edi # save EDI (message register)
pushl %esi # save ESI (msgInfo register)
pushl %edx # save EDX (contains FaultIP)
@ -548,6 +548,9 @@ BEGIN_FUNC(handle_syscall)
SET_KERNEL_STACK
# Push all the arguments for c_handle_syscall
#ifdef CONFIG_KERNEL_MCS
pushl %ebp # reply
#endif
pushl %eax # syscall number
pushl %esi # msgInfo
pushl %ebx # cptr

7
src/arch/x86/64/machine/registerset.c
View file

@ -71,3 +71,10 @@ word_t Mode_sanitiseRegister(register_t reg, word_t v)
}
return v;
}
#ifdef CONFIG_KERNEL_MCS
word_t getNBSendRecvDest(void)
{
return getRegister(NODE_STATE(ksCurThread), nbsendRecvDest);
}
#endif

8
src/arch/x86/64/traps.S
View file

@ -620,6 +620,10 @@ BEGIN_FUNC(handle_fastsyscall)
# RSI, RDI and RDX are already correct for calling c_handle_syscall
# gtfo to C land, we will not return
#ifdef CONFIG_KERNEL_MCS
# mov reply to correct register for calling c_handle_syscall
movq %r12, %rcx
#endif
jmp c_handle_syscall
END_FUNC(handle_fastsyscall)
@ -661,6 +665,10 @@ BEGIN_FUNC(handle_syscall)
# RSI, RDI are already correct for calling c_handle_syscall
movq %rax, %rdx
# gtfo to C land, we will not return
#ifdef CONFIG_KERNEL_MCS
# mov reply to correct register for calling c_handle_syscall
movq %r12, %rcx
#endif
call c_handle_syscall
END_FUNC(handle_syscall)

8
src/arch/x86/c_traps.c
View file

@ -142,7 +142,11 @@ void NORETURN slowpath(syscall_t syscall)
UNREACHABLE();
}
#ifdef CONFIG_KERNEL_MCS
void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall, word_t reply)
#else
void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
#endif
{
/* need to run this first as the NODE_LOCK code might end up as a function call
* with a return, and we need to make sure returns are not exploitable yet */
@ -172,7 +176,11 @@ void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t sy
fastpath_call(cptr, msgInfo);
UNREACHABLE();
} else if (syscall == (syscall_t)SysReplyRecv) {
#ifdef CONFIG_KERNEL_MCS
fastpath_reply_recv(cptr, msgInfo, reply);
#else
fastpath_reply_recv(cptr, msgInfo);
#endif
UNREACHABLE();
}
#endif /* CONFIG_FASTPATH */

6
src/config.cmake
View file

@ -46,5 +46,9 @@ add_sources(
)
add_sources(
DEP KernelIsMCS
CFILES src/object/schedcontext.c src/object/schedcontrol.c src/kernel/sporadic.c
CFILES
src/object/reply.c
src/object/schedcontext.c
src/object/schedcontrol.c
src/kernel/sporadic.c
)

116
src/fastpath/fastpath.c
View file

@ -10,6 +10,9 @@
#include <config.h>
#include <fastpath/fastpath.h>
#ifdef CONFIG_KERNEL_MCS
#include <object/reply.h>
#endif
#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
#include <benchmark/benchmark_track.h>
@ -28,13 +31,11 @@ fastpath_call(word_t cptr, word_t msgInfo)
word_t length;
tcb_t *dest;
word_t badge;
cte_t *replySlot, *callerSlot;
cap_t newVTable;
vspace_root_t *cap_pd;
pde_t stored_hw_asid;
word_t fault_type;
dom_t dom;
word_t replyCanGrant;
/* Get message info, length, and fault type. */
info = messageInfoFromWord_raw(msgInfo);
@ -132,6 +133,17 @@ fastpath_call(word_t cptr, word_t msgInfo)
slowpath(SysCall);
}
#ifdef CONFIG_KERNEL_MCS
if (unlikely(dest->tcbSchedContext != NULL)) {
slowpath(SysCall);
}
reply_t *reply = thread_state_get_replyObject_np(dest->tcbState);
if (unlikely(reply == NULL)) {
slowpath(SysCall);
}
#endif
#ifdef ENABLE_SMP_SUPPORT
/* Ensure both threads have the same affinity */
if (unlikely(NODE_STATE(ksCurThread)->tcbAffinity != dest->tcbAffinity)) {
@ -145,6 +157,11 @@ fastpath_call(word_t cptr, word_t msgInfo)
* At this stage, we have committed to performing the IPC.
*/
#ifdef CONFIG_KERNEL_MCS
/* consume reply state */
thread_state_ptr_set_replyObject_np(&dest->tcbState, 0);
#endif
#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
ksKernelEntry.is_fastpath = true;
#endif
@ -163,19 +180,37 @@ fastpath_call(word_t cptr, word_t msgInfo)
thread_state_ptr_set_tsType_np(&NODE_STATE(ksCurThread)->tcbState,
ThreadState_BlockedOnReply);
#ifdef CONFIG_KERNEL_MCS
reply->replyCaller = NODE_STATE(ksCurThread);
NODE_STATE(ksCurThread)->tcbReply = reply;
sched_context_t *sc = NODE_STATE(ksCurThread)->tcbSchedContext;
sc->scTcb = dest;
dest->tcbSchedContext = sc;
NODE_STATE(ksCurThread)->tcbSchedContext = NULL;
reply_t *old_caller = sc->scReply;
reply->replyPrev = call_stack_new(REPLY_REF(sc->scReply), false);
if (unlikely(old_caller)) {
old_caller->replyNext = call_stack_new(REPLY_REF(reply), false);
}
reply->replyNext = call_stack_new(SC_REF(sc), true);
sc->scReply = reply;
#else
/* Get sender reply slot */
replySlot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbReply);
cte_t *replySlot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbReply);
/* Get dest caller slot */
callerSlot = TCB_PTR_CTE_PTR(dest, tcbCaller);
cte_t *callerSlot = TCB_PTR_CTE_PTR(dest, tcbCaller);
/* Insert reply cap */
replyCanGrant = thread_state_ptr_get_blockingIPCCanGrant(&dest->tcbState);;
word_t replyCanGrant = thread_state_ptr_get_blockingIPCCanGrant(&dest->tcbState);;
cap_reply_cap_ptr_new_np(&callerSlot->cap, replyCanGrant, 0,
TCB_REF(NODE_STATE(ksCurThread)));
mdb_node_ptr_set_mdbPrev_np(&callerSlot->cteMDBNode, CTE_REF(replySlot));
mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged(
&replySlot->cteMDBNode, CTE_REF(callerSlot), 1, 1);
#endif
fastpath_copy_mrs(length, NODE_STATE(ksCurThread), dest);
@ -189,14 +224,16 @@ fastpath_call(word_t cptr, word_t msgInfo)
fastpath_restore(badge, msgInfo, NODE_STATE(ksCurThread));
}
#ifdef CONFIG_KERNEL_MCS
void fastpath_reply_recv(word_t cptr, word_t msgInfo, word_t reply)
#else
void fastpath_reply_recv(word_t cptr, word_t msgInfo)
#endif
{
seL4_MessageInfo_t info;
cap_t ep_cap;
endpoint_t *ep_ptr;
word_t length;
cte_t *callerSlot;
cap_t callerCap;
tcb_t *caller;
word_t badge;
tcb_t *endpointTail;
@ -229,6 +266,16 @@ void fastpath_reply_recv(word_t cptr, word_t msgInfo)
slowpath(SysReplyRecv);
}
#ifdef CONFIG_KERNEL_MCS
/* lookup the reply object */
cap_t reply_cap = lookup_fp(TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbCTable)->cap, reply);
/* check it's a reply object */
if (unlikely(!cap_capType_equals(reply_cap, cap_reply_cap))) {
slowpath(SysReplyRecv);
}
#endif
/* Check there is nothing waiting on the notification */
if (NODE_STATE(ksCurThread)->tcbBoundNotification &&
notification_ptr_get_state(NODE_STATE(ksCurThread)->tcbBoundNotification) == NtfnState_Active) {
@ -243,15 +290,28 @@ void fastpath_reply_recv(word_t cptr, word_t msgInfo)
slowpath(SysReplyRecv);
}
#ifdef CONFIG_KERNEL_MCS
/* Get the reply address */
reply_t *reply_ptr = REPLY_PTR(cap_reply_cap_get_capReplyPtr(reply_cap));
/* check that its valid and at the head of the call chain */
if (unlikely(reply_ptr->replyCaller == NULL ||
reply_ptr->replyNext.words[0] == 0)) {
slowpath(SysReplyRecv);
}
/* Determine who the caller is. */
caller = reply_ptr->replyCaller;
#else
/* Only reply if the reply cap is valid. */
callerSlot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbCaller);
callerCap = callerSlot->cap;
cte_t *callerSlot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbCaller);
cap_t callerCap = callerSlot->cap;
if (unlikely(!fastpath_reply_cap_check(callerCap))) {
slowpath(SysReplyRecv);
}
/* Determine who the caller is. */
caller = TCB_PTR(cap_reply_cap_get_capTCBPtr(callerCap));
#endif
/* ensure we are not single stepping the caller in ia32 */
#if defined(CONFIG_HARDWARE_DEBUG_API) && defined(CONFIG_ARCH_IA32)
@ -313,6 +373,12 @@ void fastpath_reply_recv(word_t cptr, word_t msgInfo)
slowpath(SysReplyRecv);
}
#ifdef CONFIG_KERNEL_MCS
if (unlikely(caller->tcbSchedContext != NULL)) {
slowpath(SysReplyRecv);
}
#endif
#ifdef ENABLE_SMP_SUPPORT
/* Ensure both threads have the same affinity */
if (unlikely(NODE_STATE(ksCurThread)->tcbAffinity != caller->tcbAffinity)) {
@ -320,12 +386,22 @@ void fastpath_reply_recv(word_t cptr, word_t msgInfo)
}
#endif /* ENABLE_SMP_SUPPORT */
#ifdef CONFIG_KERNEL_MCS
/* not possible to set reply object and not be blocked */
assert(thread_state_get_replyObject(NODE_STATE(ksCurThread)->tcbState) == 0);
#endif
/*
* --- POINT OF NO RETURN ---
*
* At this stage, we have committed to performing the IPC.
*/
#ifdef CONFIG_KERNEL_MCS
/* set the reply object */
thread_state_ptr_set_replyObject_np(&NODE_STATE(ksCurThread)->tcbState, REPLY_REF(reply_ptr));
#endif
#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
ksKernelEntry.is_fastpath = true;
#endif
@ -364,12 +440,34 @@ void fastpath_reply_recv(word_t cptr, word_t msgInfo)
#endif
}
#ifdef CONFIG_KERNEL_MCS
/* Clear the reply cap. */
caller->tcbReply = NULL;
reply_ptr->replyCaller = NULL;
word_t prev_ptr = call_stack_get_callStackPtr(reply_ptr->replyPrev);
sched_context_t *sc = NODE_STATE(ksCurThread)->tcbSchedContext;
NODE_STATE(ksCurThread)->tcbSchedContext = NULL;
caller->tcbSchedContext = sc;
sc->scTcb = caller;
sc->scReply = REPLY_PTR(prev_ptr);
if (unlikely(REPLY_PTR(prev_ptr) != NULL)) {
sc->scReply->replyNext = reply_ptr->replyNext;
}
/* TODO neccessary? */
reply_ptr->replyPrev.words[0] = 0;
reply_ptr->replyNext.words[0] = 0;
#else
/* Delete the reply cap. */
mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged(
&CTE_PTR(mdb_node_get_mdbPrev(callerSlot->cteMDBNode))->cteMDBNode,
0, 1, 1);
callerSlot->cap = cap_null_cap_new();
callerSlot->cteMDBNode = nullMDBNode;
#endif
/* I know there's no fault, so straight to the transfer. */

2
src/kernel/boot.c
View file

@ -434,7 +434,9 @@ BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vp
tcb->tcbPriority = seL4_MaxPrio;
tcb->tcbMCP = seL4_MaxPrio;
#ifndef CONFIG_KERNEL_MCS
setupReplyMaster(tcb);
#endif
setThreadState(tcb, ThreadState_Running);
ksCurDomain = ksDomSchedule[ksDomScheduleIdx].domain;

9
src/kernel/faulthandler.c
View file

@ -51,11 +51,18 @@ exception_t sendFaultIPC(tcb_t *tptr)
if (seL4_Fault_get_seL4_FaultType(current_fault) == seL4_Fault_CapFault) {
tptr->tcbLookupFailure = original_lookup_fault;
}
#ifdef CONFIG_KERNEL_MCS
sendIPC(true, true,
cap_endpoint_cap_get_capEPBadge(handlerCap),
cap_endpoint_cap_get_capCanGrant(handlerCap),
true, true, tptr,
EP_PTR(cap_endpoint_cap_get_capEPPtr(handlerCap)));
#else
sendIPC(true, true,
cap_endpoint_cap_get_capEPBadge(handlerCap),
cap_endpoint_cap_get_capCanGrant(handlerCap), true, tptr,
EP_PTR(cap_endpoint_cap_get_capEPPtr(handlerCap)));
#endif
return EXCEPTION_NONE;
} else {
current_fault = seL4_Fault_CapFault_new(handlerCPtr, false);

27
src/kernel/thread.c
View file

@ -112,13 +112,14 @@ void restart(tcb_t *target)
{
if (isBlocked(target)) {
cancelIPC(target);
setupReplyMaster(target);
setThreadState(target, ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
setThreadState(target, ThreadState_Restart);
if (likely(target->tcbSchedContext != NULL)) {
schedContext_resume(target->tcbSchedContext);
}
#else
setupReplyMaster(target);
setThreadState(target, ThreadState_Restart);
SCHED_ENQUEUE(target);
possibleSwitchTo(target);
#endif
@ -141,22 +142,43 @@ void doIPCTransfer(tcb_t *sender, endpoint_t *endpoint, word_t badge,
}
}
#ifdef CONFIG_KERNEL_MCS
void doReplyTransfer(tcb_t *sender, reply_t *reply, bool_t grant)
#else
void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot, bool_t grant)
#endif
{
#ifdef CONFIG_KERNEL_MCS
if (unlikely(reply->replyCaller == NULL)) {
return;
}
assert(thread_state_get_tsType(reply->replyCaller->tcbState) ==
ThreadState_BlockedOnReply);
tcb_t *receiver = reply->replyCaller;
reply_remove(reply);
thread_state_ptr_set_replyObject(&receiver->tcbState, REPLY_REF(0));
#else
assert(thread_state_get_tsType(receiver->tcbState) ==
ThreadState_BlockedOnReply);
#endif
if (likely(seL4_Fault_get_seL4_FaultType(receiver->tcbFault) == seL4_Fault_NullFault)) {
doIPCTransfer(sender, NULL, 0, grant, receiver);
#ifndef CONFIG_KERNEL_MCS
/** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
cteDeleteOne(slot);
#endif
setThreadState(receiver, ThreadState_Running);
possibleSwitchTo(receiver);
} else {
bool_t restart;
#ifndef CONFIG_KERNEL_MCS
/** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
cteDeleteOne(slot);
#endif
restart = handleFaultReply(receiver, sender);
receiver->tcbFault = seL4_Fault_NullFault_new();
if (restart) {
@ -568,7 +590,6 @@ void endTimeslice(void)
/* postpone until ready */
postpone(NODE_STATE(ksCurSC));
}
rescheduleRequired();
}
#else

14
src/object/cnode.c
View file

@ -37,6 +37,12 @@ static finaliseSlot_ret_t finaliseSlot(cte_t *slot, bool_t exposed);
static void emptySlot(cte_t *slot, cap_t cleanupInfo);
static exception_t reduceZombie(cte_t *slot, bool_t exposed);
#ifdef CONFIG_KERNEL_MCS
#define CNODE_LAST_INVOCATION CNodeRotate
#else
#define CNODE_LAST_INVOCATION CNodeSaveCaller
#endif
exception_t decodeCNodeInvocation(word_t invLabel, word_t length, cap_t cap,
extra_caps_t excaps, word_t *buffer)
{
@ -48,7 +54,7 @@ exception_t decodeCNodeInvocation(word_t invLabel, word_t length, cap_t cap,
/* Haskell error: "decodeCNodeInvocation: invalid cap" */
assert(cap_get_capType(cap) == cap_cnode_cap);
if (invLabel < CNodeRevoke || invLabel > CNodeSaveCaller) {
if (invLabel < CNodeRevoke || invLabel > CNODE_LAST_INVOCATION) {
userError("CNodeCap: Illegal Operation attempted.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
@ -200,6 +206,7 @@ exception_t decodeCNodeInvocation(word_t invLabel, word_t length, cap_t cap,
return invokeCNodeDelete(destSlot);
}
#ifndef CONFIG_KERNEL_MCS
if (invLabel == CNodeSaveCaller) {
status = ensureEmptySlot(destSlot);
if (status != EXCEPTION_NONE) {
@ -210,6 +217,7 @@ exception_t decodeCNodeInvocation(word_t invLabel, word_t length, cap_t cap,
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeCNodeSaveCaller(destSlot);
}
#endif
if (invLabel == CNodeCancelBadgedSends) {
cap_t destCap;
@ -356,6 +364,7 @@ exception_t invokeCNodeRotate(cap_t cap1, cap_t cap2, cte_t *slot1,
return EXCEPTION_NONE;
}
#ifndef CONFIG_KERNEL_MCS
exception_t invokeCNodeSaveCaller(cte_t *destSlot)
{
cap_t cap;
@ -382,6 +391,7 @@ exception_t invokeCNodeSaveCaller(cte_t *destSlot)
return EXCEPTION_NONE;
}
#endif
/*
* If creating a child UntypedCap, don't allow new objects to be created in the
@ -749,6 +759,7 @@ void insertNewCap(cte_t *parent, cte_t *slot, cap_t cap)
mdb_node_ptr_set_mdbNext(&parent->cteMDBNode, CTE_REF(slot));
}
#ifndef CONFIG_KERNEL_MCS
void setupReplyMaster(tcb_t *thread)
{
cte_t *slot;
@ -763,6 +774,7 @@ void setupReplyMaster(tcb_t *thread)
mdb_node_ptr_set_mdbFirstBadged(&slot->cteMDBNode, true);
}
}
#endif
bool_t PURE isMDBParentOf(cte_t *cte_a, cte_t *cte_b)
{

104
src/object/endpoint.c
View file

@ -24,8 +24,13 @@ static inline void ep_ptr_set_queue(endpoint_t *epptr, tcb_queue_t queue)
endpoint_ptr_set_epQueue_tail(epptr, (word_t)queue.end);
}
#ifdef CONFIG_KERNEL_MCS
void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
bool_t canGrant, bool_t canGrantReply, bool_t canDonate, tcb_t *thread, endpoint_t *epptr)
#else
void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
bool_t canGrant, bool_t canGrantReply, tcb_t *thread, endpoint_t *epptr)
#endif
{
switch (endpoint_ptr_get_state(epptr)) {
case EPState_Idle:
@ -60,7 +65,6 @@ void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
case EPState_Recv: {
tcb_queue_t queue;
tcb_t *dest;
bool_t replyCanGrant;
/* Get the head of the endpoint queue. */
queue = ep_ptr_get_queue(epptr);
@ -80,7 +84,28 @@ void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
/* Do the transfer */
doIPCTransfer(thread, epptr, badge, canGrant, dest);
replyCanGrant = thread_state_ptr_get_blockingIPCCanGrant(&dest->tcbState);;
#ifdef CONFIG_KERNEL_MCS
if (do_call ||
seL4_Fault_ptr_get_seL4_FaultType(&thread->tcbFault) != seL4_Fault_NullFault) {
reply_t *reply = REPLY_PTR(thread_state_get_replyObject(dest->tcbState));
if (reply != NULL && (canGrant || canGrantReply)) {
reply_push(thread, dest, reply, canDonate);
} else {
setThreadState(thread, ThreadState_Inactive);
}
} else if (canDonate && dest->tcbSchedContext == NULL) {
schedContext_donate(thread->tcbSchedContext, dest);
}
/* blocked threads should have enough budget to get out of the kernel */
assert(dest->tcbSchedContext == NULL || refill_sufficient(dest->tcbSchedContext, 0));
assert(dest->tcbSchedContext == NULL || refill_ready(dest->tcbSchedContext));
thread_state_ptr_set_replyObject(&dest->tcbState, REPLY_REF(0));
setThreadState(dest, ThreadState_Running);
possibleSwitchTo(dest);
#else
bool_t replyCanGrant = thread_state_ptr_get_blockingIPCCanGrant(&dest->tcbState);;
setThreadState(dest, ThreadState_Running);
possibleSwitchTo(dest);
@ -92,18 +117,18 @@ void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
setThreadState(thread, ThreadState_Inactive);
}
}
#ifdef CONFIG_KERNEL_MCS
/* blocked threads should have enough budget to get out of the kernel */
assert(dest->tcbSchedContext == NULL || refill_sufficient(dest->tcbSchedContext, 0));
assert(dest->tcbSchedContext == NULL || refill_ready(dest->tcbSchedContext));
#endif
break;
}
}
}
#ifdef CONFIG_KERNEL_MCS
void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking, cap_t replyCap)
#else
void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
#endif
{
endpoint_t *epptr;
notification_t *ntfnPtr;
@ -113,6 +138,13 @@ void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
epptr = EP_PTR(cap_endpoint_cap_get_capEPPtr(cap));
#ifdef CONFIG_KERNEL_MCS
reply_t *replyPtr = NULL;
if (cap_get_capType(replyCap) == cap_reply_cap) {
replyPtr = REPLY_PTR(cap_reply_cap_get_capReplyPtr(replyCap));
}
#endif
/* Check for anything waiting in the notification */
ntfnPtr = thread->tcbBoundNotification;
if (ntfnPtr && notification_ptr_get_state(ntfnPtr) == NtfnState_Active) {
@ -129,8 +161,12 @@ void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
ThreadState_BlockedOnReceive);
thread_state_ptr_set_blockingObject(
&thread->tcbState, EP_REF(epptr));
#ifdef CONFIG_KERNEL_MCS
thread_state_ptr_set_replyObject(&thread->tcbState, REPLY_REF(replyPtr));
#else
thread_state_ptr_set_blockingIPCCanGrant(
&thread->tcbState, cap_endpoint_cap_get_capCanGrant(cap));
#endif
scheduleTCB(thread);
@ -181,6 +217,20 @@ void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
do_call = thread_state_ptr_get_blockingIPCIsCall(&sender->tcbState);
#ifdef CONFIG_KERNEL_MCS
if (do_call ||
seL4_Fault_get_seL4_FaultType(sender->tcbFault) != seL4_Fault_NullFault) {
if ((canGrant || canGrantReply) && replyPtr != NULL) {
reply_push(sender, thread, replyPtr, sender->tcbSchedContext != NULL);
} else {
setThreadState(sender, ThreadState_Inactive);
}
} else {
setThreadState(sender, ThreadState_Running);
possibleSwitchTo(sender);
assert(sender->tcbSchedContext == NULL || refill_sufficient(sender->tcbSchedContext, 0));
}
#else
if (do_call) {
if (canGrant || canGrantReply) {
setupCallerCap(sender, thread, cap_endpoint_cap_get_capCanGrant(cap));
@ -190,11 +240,8 @@ void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
} else {
setThreadState(sender, ThreadState_Running);
possibleSwitchTo(sender);
#ifdef CONFIG_KERNEL_MCS
assert(sender->tcbSchedContext == NULL || refill_sufficient(sender->tcbSchedContext, 0));
#endif
}
#endif
break;
}
}
@ -245,6 +292,14 @@ void cancelIPC(tcb_t *tptr)
endpoint_ptr_set_state(epptr, EPState_Idle);
}
#ifdef CONFIG_KERNEL_MCS
reply_t *reply = REPLY_PTR(thread_state_get_replyObject(tptr->tcbState));
if (reply != NULL) {
reply_remove(reply);
thread_state_ptr_set_replyObject(&tptr->tcbState, REPLY_REF(0));
}
#endif
setThreadState(tptr, ThreadState_Inactive);
break;
}
@ -255,6 +310,12 @@ void cancelIPC(tcb_t *tptr)
break;
case ThreadState_BlockedOnReply: {
#ifdef CONFIG_KERNEL_MCS
seL4_Fault_NullFault_ptr_new(&tptr->tcbFault);
if (tptr->tcbReply) {
reply_remove(tptr->tcbReply);
}
#else
cte_t *slot, *callerCap;
tptr->tcbFault = seL4_Fault_NullFault_new();
@ -268,6 +329,7 @@ void cancelIPC(tcb_t *tptr)
gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
cteDeleteOne(callerCap);
}
#endif
break;
}
@ -290,8 +352,18 @@ void cancelAllIPC(endpoint_t *epptr)
/* Set all blocked threads to restart */
for (; thread; thread = thread->tcbEPNext) {
#ifdef CONFIG_KERNEL_MCS
setThreadState(thread, ThreadState_Restart);
reply_t *reply = REPLY_PTR(thread_state_get_replyObject(thread->tcbState));
if (reply != NULL) {
reply_remove(reply);
thread_state_ptr_set_replyObject(&thread->tcbState, REPLY_REF(0));
}
possibleSwitchTo(thread);
#else
setThreadState(thread, ThreadState_Restart);
SCHED_ENQUEUE(thread);
#endif
}
rescheduleRequired();
@ -322,11 +394,21 @@ void cancelBadgedSends(endpoint_t *epptr, word_t badge)
word_t b = thread_state_ptr_get_blockingIPCBadge(
&thread->tcbState);
next = thread->tcbEPNext;
#ifdef CONFIG_KERNEL_MCS
/* senders do not have reply objects in their state, and we are only cancelling sends */
assert(REPLY_PTR(thread_state_get_replyObject(thread->tcbState)) == NULL);
if (b == badge) {
setThreadState(thread, ThreadState_Restart);
possibleSwitchTo(thread);
queue = tcbEPDequeue(thread, queue);
}
#else
if (b == badge) {
setThreadState(thread, ThreadState_Restart);
SCHED_ENQUEUE(thread);
queue = tcbEPDequeue(thread, queue);
}
#endif
}
ep_ptr_set_queue(epptr, queue);

4
src/object/notification.c
View file

@ -176,7 +176,11 @@ void cancelAllSignals(notification_t *ntfnPtr)
/* Set all waiting threads to Restart */
for (; thread; thread = thread->tcbEPNext) {
setThreadState(thread, ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
possibleSwitchTo(thread);
#else
SCHED_ENQUEUE(thread);
#endif
}
rescheduleRequired();
}

78
src/object/objecttype.c
View file

@ -53,6 +53,8 @@ word_t getObjectSize(word_t t, word_t userObjSize)
#ifdef CONFIG_KERNEL_MCS
case seL4_SchedContextObject:
return seL4_SchedContextBits;
case seL4_ReplyObject:
return seL4_ReplyBits;
#endif
default:
fail("Invalid object type");
@ -89,11 +91,12 @@ deriveCap_ret_t deriveCap(cte_t *slot, cap_t cap)
}
break;
#ifndef CONFIG_KERNEL_MCS
case cap_reply_cap:
ret.status = EXCEPTION_NONE;
ret.cap = cap_null_cap_new();
break;
#endif
default:
ret.status = EXCEPTION_NONE;
ret.cap = cap;
@ -132,6 +135,18 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
return fc_ret;
case cap_reply_cap:
#ifdef CONFIG_KERNEL_MCS
if (final) {
reply_t *reply = REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap));
if (reply && reply->replyCaller) {
reply_remove(reply);
}
}
fc_ret.remainder = cap_null_cap_new();
fc_ret.cleanupInfo = cap_null_cap_new();
return fc_ret;
#endif
case cap_null_cap:
case cap_domain_cap:
fc_ret.remainder = cap_null_cap_new();
@ -171,6 +186,9 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
if (tcb->tcbSchedContext) {
schedContext_unbindTCB(tcb->tcbSchedContext, tcb);
}
if (tcb->tcbReply) {
reply_remove(tcb->tcbReply);
}
#endif
suspend(tcb);
#ifdef CONFIG_DEBUG_BUILD
@ -194,6 +212,11 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
if (final) {
sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
schedContext_unbindAllTCBs(sc);
if (sc->scReply) {
assert(call_stack_get_isHead(sc->scReply->replyNext));
sc->scReply->replyNext = call_stack_new(0, false);
sc->scReply = NULL;
}
fc_ret.remainder = cap_null_cap_new();
fc_ret.cleanupInfo = cap_null_cap_new();
return fc_ret;
@ -287,8 +310,13 @@ bool_t CONST sameRegionAs(cap_t cap_a, cap_t cap_b)
case cap_reply_cap:
if (cap_get_capType(cap_b) == cap_reply_cap) {
#ifdef CONFIG_KERNEL_MCS
return cap_reply_cap_get_capReplyPtr(cap_a) ==
cap_reply_cap_get_capReplyPtr(cap_b);
#else
return cap_reply_cap_get_capTCBPtr(cap_a) ==
cap_reply_cap_get_capTCBPtr(cap_b);
#endif
}
break;
@ -532,6 +560,10 @@ cap_t createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceM
case seL4_SchedContextObject:
memzero(regionBase, 1UL << seL4_SchedContextBits);
return cap_sched_context_cap_new(SC_REF(regionBase));
case seL4_ReplyObject:
memzero(regionBase, 1UL << seL4_ReplyBits);
return cap_reply_cap_new(REPLY_REF(regionBase), true);
#endif
default:
@ -567,10 +599,17 @@ void createNewObjects(object_t t, cte_t *parent, slot_range_t slots,
}
}
#ifdef CONFIG_KERNEL_MCS
exception_t decodeInvocation(word_t invLabel, word_t length,
cptr_t capIndex, cte_t *slot, cap_t cap,
extra_caps_t excaps, bool_t block, bool_t call,
bool_t canDonate, word_t *buffer)
#else
exception_t decodeInvocation(word_t invLabel, word_t length,
cptr_t capIndex, cte_t *slot, cap_t cap,
extra_caps_t excaps, bool_t block, bool_t call,
word_t *buffer)
#endif
{
if (isArchCap(cap)) {
return Arch_decodeInvocation(invLabel, length, capIndex,
@ -600,11 +639,19 @@ exception_t decodeInvocation(word_t invLabel, word_t length,
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
return performInvocation_Endpoint(
EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)),
cap_endpoint_cap_get_capEPBadge(cap),
cap_endpoint_cap_get_capCanGrant(cap),
cap_endpoint_cap_get_capCanGrantReply(cap), block, call, canDonate);
#else
return performInvocation_Endpoint(
EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)),
cap_endpoint_cap_get_capEPBadge(cap),
cap_endpoint_cap_get_capCanGrant(cap),
cap_endpoint_cap_get_capCanGrantReply(cap), block, call);
#endif
case cap_notification_cap: {
if (unlikely(!cap_notification_cap_get_capNtfnCanSend(cap))) {
@ -621,6 +668,14 @@ exception_t decodeInvocation(word_t invLabel, word_t length,
cap_notification_cap_get_capNtfnBadge(cap));
}
#ifdef CONFIG_KERNEL_MCS
case cap_reply_cap:
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return performInvocation_Reply(
NODE_STATE(ksCurThread),
REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap)),
cap_reply_cap_get_capReplyCanGrant(cap));
#else
case cap_reply_cap:
if (unlikely(cap_reply_cap_get_capReplyMaster(cap))) {
userError("Attempted to invoke an invalid reply cap #%lu.",
@ -635,6 +690,8 @@ exception_t decodeInvocation(word_t invLabel, word_t length,
TCB_PTR(cap_reply_cap_get_capTCBPtr(cap)), slot,
cap_reply_cap_get_capReplyCanGrant(cap));
#endif
case cap_thread_cap:
return decodeTCBInvocation(invLabel, length, cap,
slot, excaps, call, buffer);
@ -669,6 +726,16 @@ exception_t decodeInvocation(word_t invLabel, word_t length,
}
}
#ifdef CONFIG_KERNEL_MCS
exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
bool_t canGrant, bool_t canGrantReply,
bool_t block, bool_t call, bool_t canDonate)
{
sendIPC(block, call, badge, canGrant, canGrantReply, canDonate, NODE_STATE(ksCurThread), ep);
return EXCEPTION_NONE;
}
#else
exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
bool_t canGrant, bool_t canGrantReply,
bool_t block, bool_t call)
@ -677,6 +744,7 @@ exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
return EXCEPTION_NONE;
}
#endif
exception_t performInvocation_Notification(notification_t *ntfn, word_t badge)
{
@ -685,8 +753,16 @@ exception_t performInvocation_Notification(notification_t *ntfn, word_t badge)
return EXCEPTION_NONE;
}
#ifdef CONFIG_KERNEL_MCS
exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply, bool_t canGrant)
{
doReplyTransfer(thread, reply, canGrant);
return EXCEPTION_NONE;
}
#else
exception_t performInvocation_Reply(tcb_t *thread, cte_t *slot, bool_t canGrant)
{
doReplyTransfer(NODE_STATE(ksCurThread), thread, slot, canGrant);
return EXCEPTION_NONE;
}
#endif

130
src/object/reply.c Normal file
View file

@ -0,0 +1,130 @@
/*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(DATA61_GPL)
*/
#include <object/reply.h>
void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t canDonate)
{
sched_context_t *sc_donated = tcb_caller->tcbSchedContext;
assert(tcb_caller != NULL);
assert(reply != NULL);
if (unlikely(reply->replyCaller)) {
/* this reply should not be in an existing call stack - but it is
* this could be intentional but warn the user in debug mode anyway */
userError("Reply object already has unexecuted reply! Invoke first.");
reply_remove(reply);
}
if (tcb_callee->tcbSchedContext) {
/* receiver already has sc */
canDonate = false;
}
assert(call_stack_get_callStackPtr(reply->replyPrev) == 0);
assert(call_stack_get_callStackPtr(reply->replyNext) == 0);
assert(reply->replyCaller == NULL);
/* tcb caller should not be in a existing call stack */
assert(tcb_caller->tcbReply == NULL);
/* link tcb and reply */
reply->replyCaller = tcb_caller;
tcb_caller->tcbReply = reply;
setThreadState(tcb_caller, ThreadState_BlockedOnReply);
if (sc_donated != NULL && canDonate) {
assert(tcb_callee->tcbSchedContext == NULL);
reply_t *old_caller = sc_donated->scReply;
/* check stack integrity */
assert(old_caller == NULL ||
SC_PTR(call_stack_get_callStackPtr(old_caller->replyNext)) == sc_donated);
/* push on to stack */
reply->replyPrev = call_stack_new(REPLY_REF(old_caller), false);
if (old_caller) {
old_caller->replyNext = call_stack_new(REPLY_REF(reply), false);
}
reply->replyNext = call_stack_new(SC_REF(sc_donated), true);
sc_donated->scReply = reply;
/* now do the actual donation */
schedContext_donate(sc_donated, tcb_callee);
}
}
/* Pop the head reply from the call stack */
void reply_pop(reply_t *reply)
{
assert(reply != NULL);
assert(reply->replyCaller != NULL);
/* unlink tcb and reply */
tcb_t *tcb = reply->replyCaller;
reply->replyCaller = NULL;
tcb->tcbReply = NULL;
word_t next_ptr = call_stack_get_callStackPtr(reply->replyNext);
word_t prev_ptr = call_stack_get_callStackPtr(reply->replyPrev);
if (likely(next_ptr != 0)) {
assert(call_stack_get_isHead(reply->replyNext));
/* give it back */
schedContext_donate(SC_PTR(next_ptr), tcb);
SC_PTR(next_ptr)->scReply = REPLY_PTR(prev_ptr);
if (prev_ptr != 0) {
REPLY_PTR(prev_ptr)->replyNext = reply->replyNext;
}
reply->replyPrev = call_stack_new(0, false);
reply->replyNext = call_stack_new(0, false);
}
}
/* Remove a reply from the middle of the call stack */
void reply_remove(reply_t *reply)
{
word_t next_ptr = call_stack_get_callStackPtr(reply->replyNext);
word_t prev_ptr = call_stack_get_callStackPtr(reply->replyPrev);
if (likely(next_ptr)) {
if (likely(call_stack_get_isHead(reply->replyNext))) {
/* head of the call stack -> just pop */
reply_pop(reply);
return;
}
/* not the head, remove from middle */
REPLY_PTR(next_ptr)->replyPrev = reply->replyPrev;
REPLY_PTR(next_ptr)->replyCaller = reply->replyCaller;
if (reply->replyCaller) {
/* to maintain the call chain, we remove this caller and
* replaced them with the next */
reply->replyCaller->tcbReply = REPLY_PTR(next_ptr);
reply->replyCaller = NULL;
}
} else if (reply->replyCaller) {
/* removing start of call chain */
reply->replyCaller->tcbReply = NULL;
reply->replyCaller = NULL;
}
if (prev_ptr) {
REPLY_PTR(prev_ptr)->replyNext = reply->replyNext;
}
reply->replyPrev = call_stack_new(0, false);
reply->replyNext = call_stack_new(0, false);
}

34
src/object/schedcontext.c
View file

@ -87,6 +87,10 @@ static exception_t decodeSchedContext_Bind(sched_context_t *sc, extra_caps_t ext
static exception_t invokeSchedContext_Unbind(sched_context_t *sc)
{
schedContext_unbindAllTCBs(sc);
if (sc->scReply) {
sc->scReply->replyNext = call_stack_new(0, false);
sc->scReply = NULL;
}
return EXCEPTION_NONE;
}
@ -148,6 +152,9 @@ void schedContext_bindTCB(sched_context_t *sc, tcb_t *tcb)
}
#endif
schedContext_resume(sc);
if (isSchedulable(tcb)) {
possibleSwitchTo(tcb);
}
}
void schedContext_unbindTCB(sched_context_t *sc, tcb_t *tcb)
@ -176,3 +183,30 @@ void schedContext_unbindAllTCBs(sched_context_t *sc)
schedContext_unbindTCB(sc, sc->scTcb);
}
}
void schedContext_donate(sched_context_t *sc, tcb_t *to)
{
assert(sc != NULL);
assert(to != NULL);
assert(to->tcbSchedContext == NULL);
tcb_t *from = sc->scTcb;
if (from) {
from->tcbSchedContext = NULL;
if (from == NODE_STATE(ksCurThread) || from == NODE_STATE(ksSchedulerAction)) {
rescheduleRequired();
} else if (isRunnable(from)) {
SMP_COND_STATEMENT(remoteTCBStall(from));
tcbSchedDequeue(from);
}
}
sc->scTcb = to;
to->tcbSchedContext = sc;
#if CONFIG_MAX_NUM_NODES > 1
if (to->tcbAffinity != sc->scCore) {
migrateTCB(to);
to->tcbAffinity = sc->scCore;
}
#endif
}

1
src/object/schedcontrol.c
View file

@ -51,6 +51,7 @@ static exception_t invokeSchedControl_Configure(sched_context_t *target, word_t
if (target->scTcb && isRunnable(target->scTcb) && target->scRefillMax > 0) {
schedContext_resume(target);
possibleSwitchTo(target->scTcb);
}
return EXCEPTION_NONE;

4
src/object/tcb.c
View file

@ -222,6 +222,7 @@ void tcbDebugRemove(tcb_t *tcb)
}
#endif /* CONFIG_DEBUG_BUILD */
#ifndef CONFIG_KERNEL_MCS
/* Add TCB to the end of an endpoint queue */
tcb_queue_t tcbEPAppend(tcb_t *tcb, tcb_queue_t queue)
{
@ -236,6 +237,7 @@ tcb_queue_t tcbEPAppend(tcb_t *tcb, tcb_queue_t queue)
return queue;
}
#endif
/* Remove TCB from an endpoint queue */
tcb_queue_t tcbEPDequeue(tcb_t *tcb, tcb_queue_t queue)
@ -345,6 +347,7 @@ void setExtraBadge(word_t *bufferPtr, word_t badge,
bufferPtr[seL4_MsgMaxLength + 2 + i] = badge;
}
#ifndef CONFIG_KERNEL_MCS
void setupCallerCap(tcb_t *sender, tcb_t *receiver, bool_t canGrant)
{
cte_t *replySlot, *callerSlot;
@ -374,6 +377,7 @@ void deleteCallerCap(tcb_t *receiver)
/** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
cteDeleteOne(callerSlot);
}
#endif
extra_caps_t current_extra_caps;

9
tools/syscall_header_gen.py
View file

@ -149,6 +149,8 @@ def parse_args():
help='Name of file to generate for kernel')
parser.add_argument('--libsel4_header', type=argparse.FileType('w'),
help='Name of file to generate for libsel4')
parser.add_argument('--mcs', action='store_true',
help='Generate MCS api')
result = parser.parse_args()
@ -177,7 +179,7 @@ def parse_syscall_list(element):
return syscalls
def parse_xml(xml_file):
def parse_xml(xml_file, mcs):
# first check if the file is valid xml
try:
doc = xml.dom.minidom.parse(xml_file)
@ -185,7 +187,8 @@ def parse_xml(xml_file):
print("Error: invalid xml file.", file=sys.stderr)
sys.exit(-1)
api = doc.getElementsByTagName("api")
tag = "api-mcs" if mcs else "api-master"
api = doc.getElementsByTagName(tag)
if len(api) != 1:
print("Error: malformed xml. Only one api element allowed",
file=sys.stderr)
@ -238,7 +241,7 @@ def generate_libsel4_file(libsel4_header, syscalls):
if __name__ == "__main__":
args = parse_args()
(api, debug) = parse_xml(args.xml)
(api, debug) = parse_xml(args.xml, args.mcs)
args.xml.close()
if (args.kernel_header is not None):