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

mcs: Add a scheduling context object

Browse source 
This is the first part of the seL4 MCS. This commit:

    * adds a scheduling context object. Threads without scheduling
      context objects cannot be scheduled.
    * replaces tcbTimeSlice with the scheduling context object
    * adds seL4_SchedControl caps for each core
    * adds seL4_SchedControl_Configure which allows users to configure
      amount of ticks a scheduling context has, and set a core for the
      scheduling context.
    * adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
      a tcb to be bound to a scheduling context.
This commit is contained in:
Anna Lyons 2016-10-28 14:58:54 +11:00 committed by Kent Mcleod
parent caad010a09
commit 952134d1b8
39 changed files with 1014 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
config.cmake
View file

@ -206,11 +206,23 @@ config_string(
UNQUOTE
)
config_string(KernelTimerTickMS TIMER_TICK_MS "Timer tick period in milliseconds" DEFAULT 2 UNQUOTE)
config_string(
KernelTimerTickMS TIMER_TICK_MS "Timer tick period in milliseconds"
DEFAULT 2
UNQUOTE UNDEF_DISABLED
)
config_string(
KernelTimeSlice TIME_SLICE "Number of timer ticks until a thread is preempted."
DEFAULT 5
UNQUOTE
DEPENDS "NOT KernelIsMCS" UNDEF_DISABLED
)
config_string(
KernelBootThreadTimeSlice BOOT_THREAD_TIME_SLICE
"Number of milliseconds until the boot thread is preempted."
DEFAULT 5
UNQUOTE
DEPENDS "KernelIsMCS" UNDEF_DISABLED
)
config_string(
KernelRetypeFanOutLimit RETYPE_FAN_OUT_LIMIT

4
configs/seL4Config.cmake
View file

@ -171,6 +171,10 @@ config_set(KernelArchArmV6 ARCH_ARM_V6 "${KernelArchArmV6}")
config_set(KernelArchArmV7a ARCH_ARM_V7A "${KernelArchArmV7a}")
config_set(KernelArchArmV7ve ARCH_ARM_V7VE "${KernelArchArmV7ve}")
config_set(KernelArchArmV8a ARCH_ARM_V8A "${KernelArchArmV8a}")
if(KernelArchRiscV)
# MCS is not supported on RISC-V yet.
set(KernelPlatformSupportsMCS OFF)
endif()
set(KernelPlatformSupportsMCS "${KernelPlatformSupportsMCS}" CACHE INTERNAL "" FORCE)
# Check for v7ve before v7a as v7ve is a superset and we want to set the

24
include/32/mode/api/ipc_buffer.h Normal file
View file

@ -0,0 +1,24 @@
/*
* 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 __IPC_BUFFER_H
#define __IPC_BUFFER_H
#include <types.h>
#include <api/syscall.h>
static inline ticks_t mode_parseTimeArg(word_t i, word_t *buffer)
{
return (((ticks_t) getSyscallArg(i + 1, buffer) << 32llu) + getSyscallArg(i, buffer));
}
#endif /* __IPC_BUFFER_H */

24
include/64/mode/api/ipc_buffer.h Normal file
View file

@ -0,0 +1,24 @@
/*
* 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 __IPC_BUFFER_H
#define __IPC_BUFFER_H
#include <types.h>
#include <api/syscall.h>
static inline ticks_t mode_parseTimeArg(word_t i, word_t *buffer)
{
return getSyscallArg(i, buffer);
}
#endif /* __IPC_BUFFER_H */

2
include/api/syscall.h
View file

@ -19,6 +19,8 @@
#include <arch/api/syscall.h>
#include <api/debug.h>
#define TIME_ARG_SIZE (sizeof(ticks_t) / sizeof(word_t))
exception_t handleSyscall(syscall_t syscall);
exception_t handleInterruptEntry(void);
exception_t handleUnknownSyscall(word_t w);

1
include/api/types.h
View file

@ -25,6 +25,7 @@
/* seL4_CapRights_t defined in mode/api/shared_types.bf */
typedef word_t prio_t;
typedef uint64_t ticks_t;
enum domainConstants {
minDom = 0,

4
include/arch/arm/arch/32/mode/object/structures.bf
View file

@ -168,6 +168,10 @@ tagged_union cap capType {
tag irq_handler_cap 0x1e
tag zombie_cap 0x2e
tag domain_cap 0x3e
#ifdef CONFIG_KERNEL_MCS
tag sched_context_cap 0x4e
tag sched_control_cap 0x5e
#endif
-- 8-bit tag arch caps
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

4
include/arch/arm/arch/64/mode/object/structures.bf
View file

@ -125,6 +125,10 @@ tagged_union cap capType {
tag irq_handler_cap 16
tag zombie_cap 18
tag domain_cap 20
#ifdef CONFIG_KERNEL_MCS
tag sched_context_cap 22
tag sched_control_cap 24
#endif
-- 5-bit tag arch caps
tag frame_cap 1

4
include/arch/x86/arch/32/mode/object/structures.bf
View file

@ -220,6 +220,10 @@ tagged_union cap capType {
tag irq_handler_cap 0x1e
tag zombie_cap 0x2e
tag domain_cap 0x3e
#ifdef CONFIG_KERNEL_MCS
tag sched_context_cap 0x4e
tag sched_control_cap 0x5e
#endif
-- 8-bit tag arch caps
#ifdef CONFIG_IOMMU

4
include/arch/x86/arch/64/mode/object/structures.bf
View file

@ -233,6 +233,10 @@ tagged_union cap capType {
tag irq_handler_cap 16
tag zombie_cap 18
tag domain_cap 20
#ifdef CONFIG_KERNEL_MCS
tag sched_context_cap 22
tag sched_control_cap 24
#endif
-- 5-bit tag arch caps
tag frame_cap 1

8
include/config.h
View file

@ -23,9 +23,17 @@
#endif
/* number of timer ticks until a thread is preempted */
#ifndef CONFIG_KERNEL_MCS
#ifndef CONFIG_TIME_SLICE
#define CONFIG_TIME_SLICE 5
#endif
#endif
#ifdef CONFIG_KERNEL_MCS
#ifndef CONFIG_BOOT_THREAD_TIME_SLICE
#define CONFIG_BOOT_THREAD_TIME_SLICE 5
#endif
#endif
/* the number of scheduler domains */
#ifndef CONFIG_NUM_DOMAINS

7
include/kernel/boot.h
View file

@ -72,6 +72,10 @@ void populate_bi_frame(node_id_t node_id, word_t num_nodes, vptr_t ipcbuf_vptr,
word_t extra_bi_size_bits);
void create_bi_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr);
#ifdef CONFIG_KERNEL_MCS
bool_t init_sched_control(cap_t root_cnode_cap, word_t num_nodes);
#endif
typedef struct create_frames_of_region_ret {
seL4_SlotRegion region;
bool_t success;
@ -115,6 +119,9 @@ typedef struct {
pptr_t boot_info;
pptr_t extra_bi;
pptr_t tcb;
#ifdef CONFIG_KERNEL_MCS
pptr_t sc;
#endif
region_t paging;
} rootserver_mem_t;

4
include/model/statedata.h
View file

@ -102,6 +102,10 @@ extern word_t tlbLockCount VISIBLE;
extern char ksIdleThreadTCB[CONFIG_MAX_NUM_NODES][BIT(seL4_TCBBits)];
#ifdef CONFIG_KERNEL_MCS
extern char ksIdleThreadSC[CONFIG_MAX_NUM_NODES][BIT(seL4_SchedContextBits)];
#endif
#ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER
extern paddr_t ksUserLogBuffer;
#endif /* CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER */

62
include/object/schedcontext.h Normal file
View file

@ -0,0 +1,62 @@
/*
* 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_SCHED_CONTEXT_H
#define __OBJECT_SCHED_CONTEXT_H
#include <types.h>
#include <api/failures.h>
#include <object/structures.h>
exception_t decodeSchedContextInvocation(word_t label, cap_t cap, extra_caps_t extraCaps);
/* Bind a tcb and a scheduling context. This allows a tcb to enter the scheduler.
* If the tcb is runnable, insert into scheduler
*
* @param sc the scheduling context to bind
* @param tcb the tcb to bind
*
* @pre the scheduling context must not already be bound to a tcb,
* tcb->tcbSchedContext == NULL && sc->scTcb == NULL
* @post tcb->tcbSchedContext == sc && sc->scTcb == tcb
*/
void schedContext_bindTCB(sched_context_t *sc, tcb_t *tcb);
/* Unbind a specific tcb from a scheduling context. If the tcb is runnable,
* remove from the scheduler.
*
* @param sc scheduling context to unbind
* @param tcb the tcb to unbind
*
* @pre the tcb is bound to the sc,
* (sc->scTcb == tcb && tcb->tcbSchedContext == sc);
* @post (tcb->tcbSchedContext == NULL && sc->scTcb == NULL)
*/
void schedContext_unbindTCB(sched_context_t *sc, tcb_t *tcb);
/*
* Unbind any tcb from a scheduling context. If the tcb bound to the scheduling
* context is runnable, remove from the scheduler.
*
* @param sc the scheduling context to unbind
* @post (sc->scTcb == NULL)
*/
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
*
* @pre (sc != NULL)
*/
void schedContext_resume(sched_context_t *sc);
#endif /* __OBJECT_SCHED_CONTEXT_H */

23
include/object/schedcontrol.h Normal file
View file

@ -0,0 +1,23 @@
/*
* 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_SCHED_CONTROL_H
#define __OBJECT_SCHED_CONTROL_H
#include <types.h>
#include <api/failures.h>
#include <object/structures.h>
exception_t decodeSchedControlInvocation(word_t label, cap_t cap, word_t length, extra_caps_t extra_caps,
word_t *buffer);
#endif /* __OBJECT_SCHED_CONTROL_H */

54
include/object/structures.h
View file

@ -89,6 +89,9 @@ typedef word_t notification_state_t;
#define TCB_PTR_CTE_PTR(p,i) \
(((cte_t *)((word_t)(p)&~MASK(seL4_TCBBits)))+(i))
#define SC_REF(p) ((word_t) (p))
#define SC_PTR(r) ((sched_context_t *) (r))
#define WORD_PTR(r) ((word_t *)(r))
#define WORD_REF(p) ((word_t)(p))
@ -213,6 +216,9 @@ static inline vm_attributes_t CONST vmAttributesFromWord(word_t w)
return attr;
}
#ifdef CONFIG_KERNEL_MCS
typedef struct sched_context sched_context_t;
#endif
/* TCB: size >= 18 words + sizeof(arch_tcb_t) (aligned to nearest power of 2) */
struct tcb {
/* arch specific tcb state (including context)*/
@ -241,8 +247,14 @@ struct tcb {
/* Priority, 1 byte (padded to 1 word) */
prio_t tcbPriority;
#ifdef CONFIG_KERNEL_MCS
/* scheduling context that this tcb is running on, if it is NULL the tcb cannot
* be in the scheduler queues, 1 word */
sched_context_t *tcbSchedContext;
#else
/* Timeslice remaining, 1 word */
word_t tcbTimeSlice;
#endif
/* Capability pointer to thread fault handler, 1 word */
cptr_t tcbFaultHandler;
@ -278,6 +290,22 @@ struct tcb {
};
typedef struct tcb tcb_t;
#ifdef CONFIG_KERNEL_MCS
struct sched_context {
/* budget for this sc -- remaining is refilled from this value */
ticks_t scBudget;
/* core this scheduling context provides time for - 0 if uniprocessor */
word_t scCore;
/* current budget for this tcb (timeslice) -- refilled from budget */
ticks_t scRemaining;
/* thread that this scheduling context is bound to */
tcb_t *scTcb;
};
#endif
/* Ensure object sizes are sane */
compile_assert(cte_size_sane, sizeof(cte_t) <= BIT(seL4_SlotBits))
compile_assert(tcb_cte_size_sane, TCB_CNODE_SIZE_BITS <= TCB_SIZE_BITS)
@ -290,6 +318,9 @@ compile_assert(notification_size_sane, sizeof(notification_t) <= BIT(seL4_Notifi
/* Check the IPC buffer is the right size */
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))
#endif
/* helper functions */
@ -340,11 +371,19 @@ static inline word_t CONST cap_get_capSizeBits(cap_t cap)
return 0;
case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
case cap_sched_control_cap:
#endif
return 0;
case cap_irq_handler_cap:
return 0;
#ifdef CONFIG_KERNEL_MCS
case cap_sched_context_cap:
return seL4_SchedContextBits;
#endif
default:
return cap_get_archCapSizeBits(cap);
}
@ -374,6 +413,9 @@ static inline bool_t CONST cap_get_capIsPhysical(cap_t cap)
return true;
case cap_thread_cap:
#ifdef CONFIG_KERNEL_MCS
case cap_sched_context_cap:
#endif
return true;
case cap_zombie_cap:
@ -386,6 +428,9 @@ static inline bool_t CONST cap_get_capIsPhysical(cap_t cap)
return false;
case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
case cap_sched_control_cap:
#endif
return false;
case cap_irq_handler_cap:
@ -428,10 +473,19 @@ static inline void *CONST cap_get_capPtr(cap_t cap)
return NULL;
case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
case cap_sched_control_cap:
#endif
return NULL;
case cap_irq_handler_cap:
return NULL;
#ifdef CONFIG_KERNEL_MCS
case cap_sched_context_cap:
return SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
#endif
default:
return cap_get_archCapPtr(cap);

16
include/object/structures_32.bf
View file

@ -114,6 +114,22 @@ block domain_cap {
field capType 8
}
#ifdef CONFIG_KERNEL_MCS
block sched_context_cap {
field_high capSCPtr 28
padding 4
padding 24
field capType 8
}
block sched_control_cap {
field core 32
padding 24
field capType 8
}
#endif
---- Arch-independent object types
-- Endpoint: size = 16 bytes

17
include/object/structures_64.bf
View file

@ -156,6 +156,23 @@ block domain_cap {
padding 59
}
#ifdef CONFIG_KERNEL_MCS
block sched_context_cap {
padding 64
field capType 5
padding 11
field_high capSCPtr 48
}
block sched_control_cap {
field core 64
field capType 5
padding 59
}
#endif
---- Arch-independent object types
-- Endpoint: size = 16 bytes

14
include/object/tcb.h
View file

@ -112,18 +112,32 @@ enum thread_control_flag {
thread_control_update_ipc_buffer = 0x2,
thread_control_update_space = 0x4,
thread_control_update_mcp = 0x8,
#ifdef CONFIG_KERNEL_MCS
thread_control_update_sc = 0x10,
thread_control_update_all = 0x1F,
#endif
};
typedef word_t thread_control_flag_t;
exception_t invokeTCB_Suspend(tcb_t *thread);
exception_t invokeTCB_Resume(tcb_t *thread);
#ifdef CONFIG_KERNEL_MCS
exception_t invokeTCB_ThreadControl(tcb_t *target, cte_t *slot, cptr_t faultep,
prio_t mcp, prio_t priority, cap_t cRoot_newCap,
cte_t *cRoot_srcSlot, cap_t vRoot_newCap,
cte_t *vRoot_srcSlot, word_t bufferAddr,
cap_t bufferCap, cte_t *bufferSrcSlot,
sched_context_t *sched_context,
thread_control_flag_t updateFlags);
#else
exception_t invokeTCB_ThreadControl(tcb_t *target, cte_t *slot, cptr_t faultep,
prio_t mcp, prio_t priority, cap_t cRoot_newCap,
cte_t *cRoot_srcSlot, cap_t vRoot_newCap,
cte_t *vRoot_srcSlot, word_t bufferAddr,
cap_t bufferCap, cte_t *bufferSrcSlot,
thread_control_flag_t updateFlags);
#endif
exception_t invokeTCB_CopyRegisters(tcb_t *dest, tcb_t *src,
bool_t suspendSource, bool_t resumeTarget,
bool_t transferFrame, bool_t transferInteger,

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

@ -165,7 +165,7 @@
description="The thread's new maximum controlled priority."/>
</method>
<method id="TCBSetSchedParams" name="SetSchedParams" manual_name="Set Sched Params" manual_label="tcb_setschedparams">
<method id="TCBSetSchedParams" name="SetSchedParams" manual_name="Set Sched Params" manual_label="tcb_setschedparams" condition="!defined(CONFIG_KERNEL_MCS)">
<brief>
Change a thread's priority and maximum controlled priority.
</brief>
@ -179,6 +179,22 @@
<param dir="in" name="priority" type="seL4_Word"
description="The thread's new priority."/>
</method>
<method id="TCBSetSchedParams" name="SetSchedParams" manual_name="Set Sched Params (MCS)" manual_label="tcb_setschedparams_mcs" condition="defined(CONFIG_KERNEL_MCS)">
<brief>
Change a thread's priority, maximum controlled priority, and scheduling context.
</brief>
<description>
<docref>See <autoref label="sec:sched"/></docref>
</description>
<param dir="in" name="authority" type="seL4_TCB"
description="Capability to the TCB to use the MCP from when setting the priority and MCP."/>
<param dir="in" name="mcp" type="seL4_Word"
description="The thread's new maximum controlled priority."/>
<param dir="in" name="priority" type="seL4_Word"
description="The thread's new priority."/>
<param dir="in" name="sched_context" type="seL4_CPtr"
description="Capability to the scheduling context that the TCB should run on. If the scheduling context is already bound to a notification or TCB that is not this TCB this operation will fail. Similarly, if this TCB is already bound to a scheduling context that is not this scheduling context, this will also fail."/>
</method>
<method id="TCBSetIPCBuffer" name="SetIPCBuffer" manual_name="Set IPC Buffer" manual_label="tcb_setipcbuffer">
<brief>
@ -249,7 +265,7 @@
</description>
</method>
<method id="TCBSetAffinity" name="SetAffinity" condition="CONFIG_MAX_NUM_NODES > 1" manual_name="Set CPU Affinity" manual_label="tcb_setaffinity">
<method id="TCBSetAffinity" name="SetAffinity" condition="(!defined CONFIG_KERNEL_MCS) &amp;&amp; CONFIG_MAX_NUM_NODES > 1" manual_name="Set CPU Affinity" manual_label="tcb_setaffinity">
<brief>
Change a thread's current CPU in multicore machine
</brief>
@ -577,6 +593,86 @@
<param dir="in" name="domain" type="seL4_Uint8" description="The thread's new domain."/>
<param dir="in" name="thread" type="seL4_TCB" description="Capability to the TCB which is being operated on."/>
</method>
</interface>
<interface name="seL4_SchedControl">
<method id="SchedControlConfigure" name="Configure" manual_name="Configure" manual_label="schedcontrol_configure" condition="defined(CONFIG_KERNEL_MCS)">
<brief>
Set the parameters of a scheduling context by invoking the scheduling control capability. If the scheduling context is bound to a currently running thread, the parameters will take effect immediately: that is the current budget will be increased or reduced by the difference between the new and previous budget and the replenishment time will be updated according to any difference in the period. This can result in active threads being post-poned or released depending on the nature of the parameter change and the state of the thread. Additionally, if the scheduling context was previously empty (no budget) but bound to a runnable thread, this can result in a thread running for the first time since it now has access to CPU time. This call will return seL4 Invalid Argument if the parameters are too small (smaller than the kernel WCET for this platform) or too large (will overflow the timer).
</brief>
<description>
See <autoref sec="threads"/>
</description>
<return><errornumdesc/></return>
<param dir="in" name="schedcontext" type="seL4_SchedContext"
description="Capability to the scheduling context which is being operated on."/>
<param dir="in" name="budget" type="seL4_Time"
description="Timeslice in microseconds, when the budget expires the thread will be pre-empted."/>
<param dir="in" name="period" type="seL4_Time"
description="Period in microseconds, the budget is replenished every time the period expires."/>
</method>
</interface>
<interface name="seL4_SchedContext">
<method id="SchedContextBind" name="Bind"
manual_name="Bind" manual_label="schedcontext_bind" condition="defined(CONFIG_KERNEL_MCS)">
<brief>
Bind an object to a scheduling context. The object can be a notification object or a
thread.
If the object is a thread and the thread is in a runnable state and the scheduling
context has available budget, this will start the thread running.
If the object is a notification, when passive threads wait on the notification object and
a signal arrives, the passive thread will receive the scheduling context and possess it
until it waits on the notification object again.
This operation will fail if the scheduling context is already bound to a thread or
notification object.
</brief>
<description>
See <autoref sec="threads"/>
</description>
<return><errornumdesc/></return>
<param dir="in" name="cap" type="seL4_CPtr"
description="Capability to a TCB or a notification object"/>
</method>
<method id="SchedContextUnbind" name="Unbind"
manual_name="Unbind" manual_label="schedcontext_unbind" condition="defined(CONFIG_KERNEL_MCS)">
<brief>
Unbind any objects (threads or notification objects) from a scheduling context. This
will render the bound thread passive, see Section 6.1.5.
</brief>
<description>
See <autoref sec="threads"/>
</description>
<return><errornumdesc/></return>
</method>
<method id="SchedContextUnbindObject" name="UnbindObject"
manual_name="UnbindObject" manual_label="schedcontext_unbindobject" condition="defined(CONFIG_KERNEL_MCS)">
<brief>
Unbind an object from a scheduling context. The object can be either a thread or a
notification.
If the thread being unbound is the thread that is bound to this scheduling context,
this will render the thread passive, see Section 6.1.5. However if the thread being
unbound received the scheduling context via scheduling context donation over IPC,
the scheduling context will be returned to the thread that it was originally bound to.
If the object is a notification and it is bound to the scheduling context, unbind it.
</brief>
<description>
See <autoref sec="threads"/>
</description>
<return><errornumdesc/></return>
<param dir="in" name="cap" type="seL4_CPtr"
description="Capability to a notification that is bound to the scheduling context or capability to a tcb that is bound to this scheduling context or has received it through scheduling context donation."/>
</method>
</interface>

12
libsel4/include/sel4/bootinfo_types.h
View file

@ -13,6 +13,10 @@
#ifndef __LIBSEL4_BOOTINFO_TYPES_H
#define __LIBSEL4_BOOTINFO_TYPES_H
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
/* caps with fixed slot positions in the root CNode */
enum {
@ -28,7 +32,12 @@ enum {
seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
seL4_CapDomain = 11, /* global domain controller cap */
#ifdef CONFIG_KERNEL_MCS
seL4_CapInitThreadSC = 12, /* initial thread's scheduling context cap */
seL4_NumInitialCaps = 13
#else /* CONFIG_KERNEL_MCS */
seL4_NumInitialCaps = 12
#endif /* !CONFIG_KERNEL_MCS */
};
/* Legacy code will have assumptions on the vspace root being a Page Directory
@ -65,6 +74,9 @@ typedef struct {
seL4_SlotRegion extraBIPages; /* caps for any pages used to back the additional bootinfo information */
seL4_Word initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
seL4_Domain initThreadDomain; /* Initial thread's domain ID */
#ifdef CONFIG_KERNEL_MCS
seL4_SlotRegion schedcontrol; /* Caps to sched_control for each node */
#endif
seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
seL4_UntypedDesc untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* information about each untyped */
/* the untypedList should be the last entry in this struct, in order

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

@ -19,6 +19,9 @@ typedef enum api_object {
seL4_EndpointObject,
seL4_NotificationObject,
seL4_CapTableObject,
#ifdef CONFIG_KERNEL_MCS
seL4_SchedContextObject,
#endif
seL4_NonArchObjectTypeCount,
} seL4_ObjectType;

3
libsel4/include/sel4/types.h
View file

@ -39,6 +39,9 @@ typedef seL4_CPtr seL4_IRQControl;
typedef seL4_CPtr seL4_TCB;
typedef seL4_CPtr seL4_Untyped;
typedef seL4_CPtr seL4_DomainSet;
typedef seL4_CPtr seL4_SchedContext;
typedef seL4_CPtr seL4_SchedControl;
typedef seL4_Uint64 seL4_Time;
#define seL4_NilData 0

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

@ -152,6 +152,7 @@ enum {
#define seL4_EndpointBits 4
#define seL4_NotificationBits 4
#define seL4_SchedContextBits 5
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
#define seL4_PageTableBits 12

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

@ -125,6 +125,7 @@ enum {
#define seL4_TCBBits 11
#define seL4_EndpointBits 4
#define seL4_NotificationBits 5
#define seL4_SchedContextBits 5
#define seL4_PageTableBits 12
#define seL4_PageTableEntryBits 3

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

@ -46,6 +46,7 @@
#define seL4_ASIDPoolBits 12
#define seL4_ASIDPoolIndexBits 10
#define seL4_WordSizeBits 2
#define seL4_SchedContextBits 5
#define seL4_HugePageBits 30 /* 1GB */
#define seL4_PDPTBits 0

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

@ -60,6 +60,7 @@
#define seL4_NumASIDPoolsBits 3
#define seL4_ASIDPoolBits 12
#define seL4_ASIDPoolIndexBits 9
#define seL4_SchedContextBits 5
/* Untyped size limits */
#define seL4_MinUntypedBits 4

3
libsel4/tools/syscall_stub_gen.py
View file

@ -242,6 +242,7 @@ def init_data_types(wordsize):
Type("seL4_Uint16", 16, wordsize),
Type("seL4_Uint32", 32, wordsize),
Type("seL4_Uint64", 64, wordsize, double_word=(wordsize == 32)),
Type("seL4_Time", 64, wordsize, double_word=(wordsize == 32)),
Type("seL4_Word", wordsize, wordsize),
Type("seL4_Bool", 1, wordsize, native_size_bits=8),
@ -256,6 +257,8 @@ def init_data_types(wordsize):
CapType("seL4_TCB", wordsize),
CapType("seL4_Untyped", wordsize),
CapType("seL4_DomainSet", wordsize),
CapType("seL4_SchedContext", wordsize),
CapType("seL4_SchedControl", wordsize),
]
return types

14
manual/parts/threads.tex
View file

@ -39,9 +39,17 @@ or \apifunc{seL4\_TCB\_Configure}{tcb_configure} methods and then calling
\apifunc{seL4\_TCB\_WriteRegisters}{tcb_writeregisters} with an initial stack pointer and instruction
pointer. The thread can then be activated either by setting the
\texttt{resume\_target} parameter in the \apifunc{seL4\_TCB\_WriteRegisters}{tcb_writeregisters} invocation to true
or by seperately calling the \apifunc{seL4\_TCB\_Resume}{tcb_resume} method. In multicore machines, the thread
would be running on the same CPU which originally created the \obj{TCB}. However, it could be migrated to other CPUs
by calling \apifunc{seL4\_TCB\_SetAffinity}{tcb_setaffinity}.
or by seperately calling the \apifunc{seL4\_TCB\_Resume}{tcb_resume} method. Both of these methods
place the thread in a runnable state.
On the master kernel, this will result in the thread immediately being added to
the scheduler. On the MCS kernel, the thread will only begin running if it has a
scheduling context object.
In a SMP configuration of the kernel, the thread will resume on the core
corresponding to the affinity of the thread. For master, this is set using
\apifunc{seL4\_TCB\_SetAffinity}{tcb_setaffinity}, while on the MCS kernel the affinity is
derived from the scheduling context object.
\subsection{Thread Deactivation}
\label{sec:thread_deactivation}

4
src/arch/arm/kernel/boot.c
View file

@ -456,6 +456,10 @@ static BOOT_CODE bool_t try_init_kernel(
ndks_boot.bi_frame->extraBIPages = extra_bi_ret.region;
}
#ifdef CONFIG_KERNEL_MCS
init_sched_control(root_cnode_cap, CONFIG_MAX_NUM_NODES);
#endif
/* create the initial thread's IPC buffer */
ipcbuf_cap = create_ipcbuf_frame_cap(root_cnode_cap, it_pd_cap, ipcbuf_vptr);
if (cap_get_capType(ipcbuf_cap) == cap_null_cap) {

5
src/arch/x86/kernel/boot.c
View file

@ -370,6 +370,11 @@ BOOT_CODE bool_t init_sys_state(
padding_header.len = (extra_bi_region.end - extra_bi_region.start) - extra_bi_offset;
*(seL4_BootInfoHeader *)(extra_bi_region.start + extra_bi_offset) = padding_header;
#ifdef CONFIG_KERNEL_MCS
/* set up sched control for each core */
init_sched_control(root_cnode_cap, CONFIG_MAX_NUM_NODES);
#endif
/* Construct an initial address space with enough virtual addresses
* to cover the user image + ipc buffer and bootinfo frames */
it_vspace_cap = create_it_address_space(root_cnode_cap, it_v_reg);

1
src/config.cmake
View file

@ -44,3 +44,4 @@ add_sources(
src/smp/lock.c
src/smp/ipi.c
)
add_sources(DEP KernelIsMCS CFILES src/object/schedcontext.c src/object/schedcontrol.c)

66
src/kernel/boot.c
View file

@ -85,6 +85,9 @@ BOOT_CODE static word_t calculate_rootserver_size(v_region_t v_reg, word_t extra
size += BIT(seL4_ASIDPoolBits);
size += extra_bi_size_bits > 0 ? BIT(extra_bi_size_bits) : 0;
size += BIT(seL4_VSpaceBits); // root vspace
#ifdef CONFIG_KERNEL_MCS
size += BIT(seL4_SchedContextBits); // root sched context
#endif
/* for all archs, seL4_PageTable Bits is the size of all non top-level paging structures */
return size + arch_get_n_paging(v_reg) * BIT(seL4_PageTableBits);
}
@ -140,6 +143,10 @@ BOOT_CODE void create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t
#if seL4_TCBBits < seL4_PageTableBits
rootserver.tcb = alloc_rootserver_obj(seL4_TCBBits, 1);
#endif
#ifdef CONFIG_KERNEL_MCS
rootserver.sc = alloc_rootserver_obj(seL4_SchedContextBits, 1);
#endif
/* we should have allocated all our memory */
assert(rootserver_mem.start == rootserver_mem.end);
}
@ -313,6 +320,40 @@ BOOT_CODE cap_t create_it_asid_pool(cap_t root_cnode_cap)
return ap_cap;
}
#ifdef CONFIG_KERNEL_MCS
BOOT_CODE static bool_t configure_sched_context(tcb_t *tcb, sched_context_t *sc_pptr, ticks_t timeslice)
{
tcb->tcbSchedContext = sc_pptr;
tcb->tcbSchedContext->scBudget = timeslice;
tcb->tcbSchedContext->scRemaining = timeslice;
tcb->tcbSchedContext->scTcb = tcb;
return true;
}
BOOT_CODE bool_t init_sched_control(cap_t root_cnode_cap, word_t num_nodes)
{
bool_t ret = true;
seL4_SlotPos slot_pos_before = ndks_boot.slot_pos_cur;
/* create a sched control cap for each core */
for (int i = 0; i < num_nodes && ret; i++) {
ret = provide_cap(root_cnode_cap, cap_sched_control_cap_new(i));
}
if (!ret) {
return false;
}
/* update boot info with slot region for sched control caps */
ndks_boot.bi_frame->schedcontrol = (seL4_SlotRegion) {
.start = slot_pos_before,
.end = ndks_boot.slot_pos_cur
};
return true;
}
#endif
BOOT_CODE bool_t create_idle_thread(void)
{
pptr_t pptr;
@ -327,6 +368,16 @@ BOOT_CODE bool_t create_idle_thread(void)
setThreadName(NODE_STATE_ON_CORE(ksIdleThread, i), "idle_thread");
#endif
SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbAffinity = i);
#ifdef CONFIG_KERNEL_MCS
bool_t result = configure_sched_context(NODE_STATE_ON_CORE(ksIdleThread, i),
SC_PTR(&ksIdleThreadSC[SMP_TERNARY(i, 0)]),
CONFIG_BOOT_THREAD_TIME_SLICE);
SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbSchedContext->scCore = i;)
if (!result) {
printf("Kernel init failed: Unable to allocate sc for idle thread\n");
return false;
}
#endif
#ifdef ENABLE_SMP_SUPPORT
}
#endif /* ENABLE_SMP_SUPPORT */
@ -337,7 +388,10 @@ BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vp
vptr_t ipcbuf_vptr, cap_t ipcbuf_cap)
{
tcb_t *tcb = TCB_PTR(rootserver.tcb + TCB_OFFSET);
#ifndef CONFIG_KERNEL_MCS
tcb->tcbTimeSlice = CONFIG_TIME_SLICE;
#endif
Arch_initContext(&tcb->tcbArch.tcbContext);
/* derive a copy of the IPC buffer cap for inserting */
@ -369,6 +423,12 @@ BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vp
setNextPC(tcb, ui_v_entry);
/* initialise TCB */
#ifdef CONFIG_KERNEL_MCS
if (!configure_sched_context(tcb, SC_PTR(rootserver.sc), CONFIG_BOOT_THREAD_TIME_SLICE)) {
return NULL;
}
#endif
tcb->tcbPriority = seL4_MaxPrio;
tcb->tcbMCP = seL4_MaxPrio;
setupReplyMaster(tcb);
@ -378,12 +438,18 @@ BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vp
ksDomainTime = ksDomSchedule[ksDomScheduleIdx].length;
assert(ksCurDomain < CONFIG_NUM_DOMAINS && ksDomainTime > 0);
#ifndef CONFIG_KERNEL_MCS
SMP_COND_STATEMENT(tcb->tcbAffinity = 0);
#endif
/* create initial thread's TCB cap */
cap_t cap = cap_thread_cap_new(TCB_REF(tcb));
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadTCB), cap);
#ifdef CONFIG_KERNEL_MCS
cap = cap_sched_context_cap_new(SC_REF(tcb->tcbSchedContext));
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadSC), cap);
#endif
#ifdef CONFIG_DEBUG_BUILD
setThreadName(tcb, "rootserver");
#endif

92
src/kernel/thread.c
View file

@ -16,6 +16,9 @@
#include <kernel/cspace.h>
#include <kernel/thread.h>
#include <kernel/vspace.h>
#ifdef CONFIG_KERNEL_MCS
#include <object/schedcontext.h>
#endif
#include <model/statedata.h>
#include <arch/machine.h>
#include <arch/kernel/thread.h>
@ -42,6 +45,17 @@ static inline bool_t PURE isBlocked(const tcb_t *thread)
}
}
#ifdef CONFIG_KERNEL_MCS
static inline bool_t PURE isSchedulable(const tcb_t *thread)
{
return isRunnable(thread) &&
thread->tcbSchedContext != NULL;
}
#else
#define isSchedulable isRunnable
#endif
BOOT_CODE void configureIdleThread(tcb_t *tcb)
{
Arch_configureIdleThread(tcb);
@ -96,8 +110,14 @@ void restart(tcb_t *target)
cancelIPC(target);
setupReplyMaster(target);
setThreadState(target, ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
if (likely(target->tcbSchedContext != NULL)) {
schedContext_resume(target->tcbSchedContext);
}
#else
SCHED_ENQUEUE(target);
possibleSwitchTo(target);
#endif
}
}
@ -274,7 +294,7 @@ void schedule(void)
{
if (NODE_STATE(ksSchedulerAction) != SchedulerAction_ResumeCurrentThread) {
bool_t was_runnable;
if (isRunnable(NODE_STATE(ksCurThread))) {
if (isSchedulable(NODE_STATE(ksCurThread))) {
was_runnable = true;
SCHED_ENQUEUE_CURRENT_TCB;
} else {
@ -285,6 +305,7 @@ void schedule(void)
scheduleChooseNewThread();
} else {
tcb_t *candidate = NODE_STATE(ksSchedulerAction);
assert(isSchedulable(candidate));
/* Avoid checking bitmap when ksCurThread is higher prio, to
* match fast path.
* Don't look at ksCurThread prio when it's idle, to respect
@ -334,7 +355,7 @@ void chooseThread(void)
prio = getHighestPrio(dom);
thread = NODE_STATE(ksReadyQueues)[ready_queues_index(dom, prio)].head;
assert(thread);
assert(isRunnable(thread));
assert(isSchedulable(thread));
switchToThread(thread);
} else {
switchToIdleThread();
@ -364,7 +385,7 @@ void setDomain(tcb_t *tptr, dom_t dom)
{
tcbSchedDequeue(tptr);
tptr->tcbDomain = dom;
if (isRunnable(tptr)) {
if (isSchedulable(tptr)) {
SCHED_ENQUEUE(tptr);
}
if (tptr == NODE_STATE(ksCurThread)) {
@ -376,7 +397,17 @@ void setMCPriority(tcb_t *tptr, prio_t mcp)
{
tptr->tcbMCP = mcp;
}
#ifdef CONFIG_KERNEL_MCS
void setPriority(tcb_t *tptr, prio_t prio)
{
tcbSchedDequeue(tptr);
tptr->tcbPriority = prio;
if (isSchedulable(tptr)) {
SCHED_ENQUEUE(tptr);
rescheduleRequired();
}
}
#else
void setPriority(tcb_t *tptr, prio_t prio)
{
tcbSchedDequeue(tptr);
@ -386,6 +417,7 @@ void setPriority(tcb_t *tptr, prio_t prio)
rescheduleRequired();
}
}
#endif
/* Note that this thread will possibly continue at the end of this kernel
* entry. Do not queue it yet, since a queue+unqueue operation is wasteful
@ -393,16 +425,23 @@ void setPriority(tcb_t *tptr, prio_t prio)
* on which the scheduler will take action. */
void possibleSwitchTo(tcb_t *target)
{
if (ksCurDomain != target->tcbDomain
SMP_COND_STATEMENT( || target->tcbAffinity != getCurrentCPUIndex())) {
SCHED_ENQUEUE(target);
} else if (NODE_STATE(ksSchedulerAction) != SchedulerAction_ResumeCurrentThread) {
/* Too many threads want special treatment, use regular queues. */
rescheduleRequired();
SCHED_ENQUEUE(target);
} else {
NODE_STATE(ksSchedulerAction) = target;
#ifdef CONFIG_KERNEL_MCS
if (target->tcbSchedContext != NULL) {
#endif
if (ksCurDomain != target->tcbDomain
SMP_COND_STATEMENT( || target->tcbAffinity != getCurrentCPUIndex())) {
SCHED_ENQUEUE(target);
} else if (NODE_STATE(ksSchedulerAction) != SchedulerAction_ResumeCurrentThread) {
/* Too many threads want special treatment, use regular queues. */
rescheduleRequired();
SCHED_ENQUEUE(target);
} else {
NODE_STATE(ksSchedulerAction) = target;
}
#ifdef CONFIG_KERNEL_MCS
}
#endif
}
void setThreadState(tcb_t *tptr, _thread_state_t ts)
@ -415,11 +454,19 @@ void scheduleTCB(tcb_t *tptr)
{
if (tptr == NODE_STATE(ksCurThread) &&
NODE_STATE(ksSchedulerAction) == SchedulerAction_ResumeCurrentThread &&
!isRunnable(tptr)) {
!isSchedulable(tptr)) {
rescheduleRequired();
}
}
#ifdef CONFIG_KERNEL_MCS
static void recharge(sched_context_t *sc)
{
sc->scRemaining = sc->scBudget;
assert(sc->scBudget > 0);
}
#endif
void timerTick(void)
{
if (likely(thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState) ==
@ -429,6 +476,16 @@ void timerTick(void)
ThreadState_RunningVM
#endif
) {
#ifdef CONFIG_KERNEL_MCS
assert(NODE_STATE(ksCurThread)->tcbSchedContext != NULL);
if (NODE_STATE(ksCurThread)->tcbSchedContext->scRemaining > 1) {
NODE_STATE(ksCurThread)->tcbSchedContext->scRemaining--;
} else {
recharge(NODE_STATE(ksCurThread)->tcbSchedContext);
SCHED_APPEND_CURRENT_TCB;
rescheduleRequired();
}
#else
if (NODE_STATE(ksCurThread)->tcbTimeSlice > 1) {
NODE_STATE(ksCurThread)->tcbTimeSlice--;
} else {
@ -436,6 +493,7 @@ void timerTick(void)
SCHED_APPEND_CURRENT_TCB;
rescheduleRequired();
}
#endif
}
if (CONFIG_NUM_DOMAINS > 1) {
@ -449,7 +507,11 @@ void timerTick(void)
void rescheduleRequired(void)
{
if (NODE_STATE(ksSchedulerAction) != SchedulerAction_ResumeCurrentThread
&& NODE_STATE(ksSchedulerAction) != SchedulerAction_ChooseNewThread) {
&& NODE_STATE(ksSchedulerAction) != SchedulerAction_ChooseNewThread
#ifdef CONFIG_KERNEL_MCS
&& isSchedulable(NODE_STATE(ksSchedulerAction))
#endif
) {
SCHED_ENQUEUE(NODE_STATE(ksSchedulerAction));
}
NODE_STATE(ksSchedulerAction) = SchedulerAction_ChooseNewThread;

5
src/model/statedata.c
View file

@ -77,6 +77,11 @@ word_t tlbLockCount = 0;
/* Idle thread. */
SECTION("._idle_thread") char ksIdleThreadTCB[CONFIG_MAX_NUM_NODES][BIT(seL4_TCBBits)] ALIGN(BIT(TCB_SIZE_BITS));
#ifdef CONFIG_KERNEL_MCS
/* Idle thread Schedcontexts */
char ksIdleThreadSC[CONFIG_MAX_NUM_NODES][BIT(seL4_SchedContextBits)] ALIGN(BIT(seL4_SchedContextBits));
#endif
#if (defined CONFIG_DEBUG_BUILD || defined CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES)
kernel_entry_t ksKernelEntry;
#endif /* DEBUG */

61
src/object/objecttype.c
View file

@ -21,6 +21,10 @@
#include <object/endpoint.h>
#include <object/cnode.h>
#include <object/interrupt.h>
#ifdef CONFIG_KERNEL_MCS
#include <object/schedcontext.h>
#include <object/schedcontrol.h>
#endif
#include <object/tcb.h>
#include <object/untyped.h>
#include <model/statedata.h>
@ -46,6 +50,10 @@ word_t getObjectSize(word_t t, word_t userObjSize)
return seL4_SlotBits + userObjSize;
case seL4_UntypedObject:
return userObjSize;
#ifdef CONFIG_KERNEL_MCS
case seL4_SchedContextObject:
return seL4_SchedContextBits;
#endif
default:
fail("Invalid object type");
return 0;
@ -159,6 +167,11 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
SMP_COND_STATEMENT(remoteTCBStall(tcb);)
cte_ptr = TCB_PTR_CTE_PTR(tcb, tcbCTable);
unbindNotification(tcb);
#ifdef CONFIG_KERNEL_MCS
if (tcb->tcbSchedContext) {
schedContext_unbindTCB(tcb->tcbSchedContext, tcb);
}
#endif
suspend(tcb);
#ifdef CONFIG_DEBUG_BUILD
tcbDebugRemove(tcb);
@ -176,6 +189,18 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
break;
}
#ifdef CONFIG_KERNEL_MCS
case cap_sched_context_cap:
if (final) {
sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
schedContext_unbindAllTCBs(sc);
fc_ret.remainder = cap_null_cap_new();
fc_ret.cleanupInfo = cap_null_cap_new();
return fc_ret;
}
break;
#endif
case cap_zombie_cap:
fc_ret.remainder = cap;
fc_ret.cleanupInfo = cap_null_cap_new();
@ -287,6 +312,19 @@ bool_t CONST sameRegionAs(cap_t cap_a, cap_t cap_b)
}
break;
#ifdef CONFIG_KERNEL_MCS
case cap_sched_context_cap:
if (cap_get_capType(cap_b) == cap_sched_context_cap) {
return cap_sched_context_cap_get_capSCPtr(cap_a) ==
cap_sched_context_cap_get_capSCPtr(cap_b);
}
break;
case cap_sched_control_cap:
if (cap_get_capType(cap_b) == cap_sched_control_cap) {
return true;
}
break;
#endif
default:
if (isArchCap(cap_a) &&
isArchCap(cap_b)) {
@ -374,6 +412,10 @@ cap_t CONST maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
case cap_irq_handler_cap:
case cap_zombie_cap:
case cap_thread_cap:
#ifdef CONFIG_KERNEL_MCS
case cap_sched_context_cap:
case cap_sched_control_cap:
#endif
return cap;
case cap_endpoint_cap: {
@ -441,12 +483,14 @@ cap_t createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceM
/* Setup non-zero parts of the TCB. */
Arch_initContext(&tcb->tcbArch.tcbContext);
#ifndef CONFIG_KERNEL_MCS
tcb->tcbTimeSlice = CONFIG_TIME_SLICE;
#endif
tcb->tcbDomain = ksCurDomain;
#ifndef CONFIG_KERNEL_MCS
/* Initialize the new TCB to the current core */
SMP_COND_STATEMENT(tcb->tcbAffinity = getCurrentCPUIndex());
#endif
#ifdef CONFIG_DEBUG_BUILD
strlcpy(tcb->tcbName, "child of: '", TCB_NAME_LENGTH);
strlcat(tcb->tcbName, NODE_STATE(ksCurThread)->tcbName, TCB_NAME_LENGTH);
@ -484,6 +528,12 @@ cap_t createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceM
*/
return cap_untyped_cap_new(0, !!deviceMemory, userSize, WORD_REF(regionBase));
#ifdef CONFIG_KERNEL_MCS
case seL4_SchedContextObject:
memzero(regionBase, 1UL << seL4_SchedContextBits);
return cap_sched_context_cap_new(SC_REF(regionBase));
#endif
default:
fail("Invalid object type");
}
@ -607,6 +657,13 @@ exception_t decodeInvocation(word_t invLabel, word_t length,
return decodeIRQHandlerInvocation(invLabel,
cap_irq_handler_cap_get_capIRQ(cap), excaps);
#ifdef CONFIG_KERNEL_MCS
case cap_sched_control_cap:
return decodeSchedControlInvocation(invLabel, cap, length, excaps, buffer);
case cap_sched_context_cap:
return decodeSchedContextInvocation(invLabel, cap, excaps);
#endif
default:
fail("Invalid cap type");
}

166
src/object/schedcontext.c Normal file
View file

@ -0,0 +1,166 @@
/*
* 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 <machine/timer.h>
#include <object/schedcontext.h>
static exception_t invokeSchedContext_UnbindObject(sched_context_t *sc, cap_t cap)
{
schedContext_unbindTCB(sc, TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)));
return EXCEPTION_NONE;
}
static exception_t decodeSchedContext_UnbindObject(sched_context_t *sc, extra_caps_t extraCaps)
{
if (extraCaps.excaprefs[0] == NULL) {
userError("SchedContext_Unbind: Truncated message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
cap_t cap = extraCaps.excaprefs[0]->cap;
if (cap_get_capType(cap) != cap_thread_cap) {
userError("SchedContext_Unbind: invalid cap");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
if (sc->scTcb != TCB_PTR(cap_thread_cap_get_capTCBPtr(cap))) {
userError("SchedContext_Unbind: object not bound to this sc");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeSchedContext_UnbindObject(sc, cap);
}
static exception_t invokeSchedContext_Bind(sched_context_t *sc, cap_t cap)
{
schedContext_bindTCB(sc, TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)));
return EXCEPTION_NONE;
}
static exception_t decodeSchedContext_Bind(sched_context_t *sc, extra_caps_t extraCaps)
{
if (extraCaps.excaprefs[0] == NULL) {
userError("SchedContext_Bind: Truncated Message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
cap_t cap = extraCaps.excaprefs[0]->cap;
if (sc->scTcb != NULL) {
userError("SchedContext_Bind: sched context already bound.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
if (cap_get_capType(cap) != cap_thread_cap) {
userError("SchedContext_Bind: invalid cap.");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
if (TCB_PTR(cap_thread_cap_get_capTCBPtr(cap))->tcbSchedContext != NULL) {
userError("SchedContext_Bind: tcb already bound.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeSchedContext_Bind(sc, cap);
}
static exception_t invokeSchedContext_Unbind(sched_context_t *sc)
{
schedContext_unbindAllTCBs(sc);
return EXCEPTION_NONE;
}
exception_t decodeSchedContextInvocation(word_t label, cap_t cap, extra_caps_t extraCaps)
{
sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
switch (label) {
case SchedContextBind:
return decodeSchedContext_Bind(sc, extraCaps);
case SchedContextUnbindObject:
return decodeSchedContext_UnbindObject(sc, extraCaps);
case SchedContextUnbind:
/* no decode */
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeSchedContext_Unbind(sc);
default:
userError("SchedContext invocation: Illegal operation attempted.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
}
void schedContext_resume(sched_context_t *sc)
{
assert(sc->scTcb != NULL);
#if CONFIG_MAX_NUM_NODES > 1
/* this should NOT be called when migration is possible */
assert(sc->scCore == getCurrentCPUIndex());
#endif
if (isRunnable(sc->scTcb) && sc->scBudget > 0) {
recharge(sc);
possibleSwitchTo(sc->scTcb);
}
}
void schedContext_bindTCB(sched_context_t *sc, tcb_t *tcb)
{
assert(sc->scTcb == NULL);
assert(tcb->tcbSchedContext == NULL);
tcb->tcbSchedContext = sc;
sc->scTcb = tcb;
#if CONFIG_MAX_NUM_NODES > 1
if (thread->tcbAffinity != sc->scCore) {
if (nativeThreadUsingFPU(tcb)) {
switchFPUOwner(NULL, thread->tcbAffinity);
}
tcbSchedDequeue(tcb);
tcb->tcbAffinity = sc->scCore;
}
#endif
schedContext_resume(sc);
}
void schedContext_unbindTCB(sched_context_t *sc, tcb_t *tcb)
{
assert(sc->scTcb == tcb);
tcbSchedDequeue(sc->scTcb);
sc->scTcb->tcbSchedContext = NULL;
if (sc->scTcb == NODE_STATE(ksCurThread)) {
rescheduleRequired();
} else {
SMP_COND_STATEMENT(remoteTCBStall(tcb));
}
sc->scTcb = NULL;
}
void schedContext_unbindAllTCBs(sched_context_t *sc)
{
if (sc->scTcb) {
schedContext_unbindTCB(sc, sc->scTcb);
}
}

76
src/object/schedcontrol.c Normal file
View file

@ -0,0 +1,76 @@
/*
* 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 <mode/api/ipc_buffer.h>
#include <object/schedcontext.h>
#include <object/schedcontrol.h>
static exception_t invokeSchedControl_Configure(sched_context_t *target, ticks_t budget, word_t core)
{
target->scBudget = budget;
target->scCore = core;
recharge(target);
if (target->scTcb != NULL) {
/* target may no longer have budget for this core */
if (!isSchedulable(target->scTcb)) {
tcbSchedDequeue(target->scTcb);
} else {
possibleSwitchTo(target->scTcb);
}
}
return EXCEPTION_NONE;
}
static exception_t decodeSchedControl_Configure(word_t length, cap_t cap, extra_caps_t extraCaps, word_t *buffer)
{
if (extraCaps.excaprefs[0] == NULL) {
userError("SchedControl_Configure: Truncated message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
if (length < TIME_ARG_SIZE) {
userError("SchedControl_configure: truncated message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
ticks_t budget = mode_parseTimeArg(0, buffer);
cap_t targetCap = extraCaps.excaprefs[0]->cap;
if (unlikely(cap_get_capType(targetCap) != cap_sched_context_cap)) {
userError("SchedControl_Configure: target cap not a scheduling context cap");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 1;
return EXCEPTION_SYSCALL_ERROR;
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeSchedControl_Configure(SC_PTR(cap_sched_context_cap_get_capSCPtr(targetCap)),
budget,
cap_sched_control_cap_get_core(cap));
}
exception_t decodeSchedControlInvocation(word_t label, cap_t cap, word_t length, extra_caps_t extraCaps,
word_t *buffer)
{
switch (label) {
case SchedControlConfigure:
return decodeSchedControl_Configure(length, cap, extraCaps, buffer);
default:
userError("SchedControl invocation: Illegal operation attempted.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
}

133
src/object/tcb.c
View file

@ -18,6 +18,9 @@
#include <object/structures.h>
#include <object/objecttype.h>
#include <object/cnode.h>
#ifdef CONFIG_KERNEL_MCS
#include <object/schedcontext.h>
#endif
#include <object/tcb.h>
#include <kernel/cspace.h>
#include <kernel/thread.h>
@ -82,6 +85,10 @@ static inline void removeFromBitmap(word_t cpu, word_t dom, word_t prio)
/* Add TCB to the head of a scheduler queue */
void tcbSchedEnqueue(tcb_t *tcb)
{
#ifdef CONFIG_KERNEL_MCS
assert(isSchedulable(tcb));
#endif
if (!thread_state_get_tcbQueued(tcb->tcbState)) {
tcb_queue_t queue;
dom_t dom;
@ -112,6 +119,9 @@ void tcbSchedEnqueue(tcb_t *tcb)
/* Add TCB to the end of a scheduler queue */
void tcbSchedAppend(tcb_t *tcb)
{
#ifdef CONFIG_KERNEL_MCS
assert(isSchedulable(tcb));
#endif
if (!thread_state_get_tcbQueued(tcb->tcbState)) {
tcb_queue_t queue;
dom_t dom;
@ -369,6 +379,7 @@ void remoteTCBStall(tcb_t *tcb)
}
}
#ifndef CONFIG_KERNEL_MCS
static exception_t invokeTCB_SetAffinity(tcb_t *thread, word_t affinity)
{
/* remove the tcb from scheduler queue in case it is already in one
@ -408,6 +419,7 @@ static exception_t decodeSetAffinity(cap_t cap, word_t length, word_t *buffer)
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return invokeTCB_SetAffinity(tcb, affinity);
}
#endif
#endif /* ENABLE_SMP_SUPPORT */
#ifdef CONFIG_HARDWARE_DEBUG_API
@ -720,10 +732,12 @@ exception_t decodeTCBInvocation(word_t invLabel, word_t length, cap_t cap,
case TCBUnbindNotification:
return decodeUnbindNotification(cap);
#ifndef CONFIG_KERNEL_MCS
#ifdef ENABLE_SMP_SUPPORT
case TCBSetAffinity:
return decodeSetAffinity(cap, length, buffer);
#endif /* ENABLE_SMP_SUPPORT */
#endif
/* There is no notion of arch specific TCB invocations so this needs to go here */
#ifdef CONFIG_VTX
@ -977,6 +991,16 @@ exception_t decodeTCBConfigure(cap_t cap, word_t length, cte_t *slot,
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), slot,
faultEP, NULL_PRIO, NULL_PRIO,
cRootCap, cRootSlot,
vRootCap, vRootSlot,
bufferAddr, bufferCap,
bufferSlot, NULL, thread_control_update_space |
thread_control_update_ipc_buffer);
#else
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), slot,
faultEP, NULL_PRIO, NULL_PRIO,
@ -985,6 +1009,7 @@ exception_t decodeTCBConfigure(cap_t cap, word_t length, cte_t *slot,
bufferAddr, bufferCap,
bufferSlot, thread_control_update_space |
thread_control_update_ipc_buffer);
#endif
}
exception_t decodeSetPriority(cap_t cap, word_t length, extra_caps_t excaps, word_t *buffer)
@ -1014,6 +1039,15 @@ exception_t decodeSetPriority(cap_t cap, word_t length, extra_caps_t excaps, wor
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), NULL,
0, NULL_PRIO, newPrio,
cap_null_cap_new(), NULL,
cap_null_cap_new(), NULL,
0, cap_null_cap_new(),
NULL, NULL, thread_control_update_priority);
#else
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), NULL,
0, NULL_PRIO, newPrio,
@ -1021,6 +1055,7 @@ exception_t decodeSetPriority(cap_t cap, word_t length, extra_caps_t excaps, wor
cap_null_cap_new(), NULL,
0, cap_null_cap_new(),
NULL, thread_control_update_priority);
#endif
}
exception_t decodeSetMCPriority(cap_t cap, word_t length, extra_caps_t excaps, word_t *buffer)
@ -1050,6 +1085,15 @@ exception_t decodeSetMCPriority(cap_t cap, word_t length, extra_caps_t excaps, w
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), NULL,
0, newMcp, NULL_PRIO,
cap_null_cap_new(), NULL,
cap_null_cap_new(), NULL,
0, cap_null_cap_new(),
NULL, NULL, thread_control_update_mcp);
#else
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), NULL,
0, newMcp, NULL_PRIO,
@ -1057,11 +1101,16 @@ exception_t decodeSetMCPriority(cap_t cap, word_t length, extra_caps_t excaps, w
cap_null_cap_new(), NULL,
0, cap_null_cap_new(),
NULL, thread_control_update_mcp);
#endif
}
exception_t decodeSetSchedParams(cap_t cap, word_t length, extra_caps_t excaps, word_t *buffer)
{
if (length < 2 || excaps.excaprefs[0] == NULL) {
if (length < 2 || excaps.excaprefs[0] == NULL
#ifdef CONFIG_KERNEL_MCS
|| excaps.excaprefs[1] == NULL
#endif
) {
userError("TCB SetSchedParams: Truncated message.");
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
@ -1070,6 +1119,9 @@ exception_t decodeSetSchedParams(cap_t cap, word_t length, extra_caps_t excaps,
prio_t newMcp = getSyscallArg(0, buffer);
prio_t newPrio = getSyscallArg(1, buffer);
cap_t authCap = excaps.excaprefs[0]->cap;
#ifdef CONFIG_KERNEL_MCS
cap_t scCap = excaps.excaprefs[1]->cap;
#endif
if (cap_get_capType(authCap) != cap_thread_cap) {
userError("TCB SetSchedParams: authority cap not a TCB.");
@ -1093,7 +1145,44 @@ exception_t decodeSetSchedParams(cap_t cap, word_t length, extra_caps_t excaps,
return status;
}
#ifdef CONFIG_KERNEL_MCS
tcb_t *tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap));
sched_context_t *sc = NULL;
switch (cap_get_capType(scCap)) {
case cap_sched_context_cap:
sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(scCap));
if (tcb->tcbSchedContext && tcb->tcbSchedContext != sc) {
userError("TCB SetSchedParams: tcb already has a scheduling context.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
if (sc->scTcb && sc->scTcb != tcb) {
userError("TCB SetSchedParams: sched contextext already bound.");
current_syscall_error.type = seL4_IllegalOperation;
return EXCEPTION_SYSCALL_ERROR;
}
break;
case cap_null_cap:
break;
default:
userError("TCB Configure: sched context cap invalid.");
current_syscall_error.type = seL4_InvalidCapability;
current_syscall_error.invalidCapNumber = 2;
return EXCEPTION_SYSCALL_ERROR;
}
#endif
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), NULL,
0, newMcp, newPrio,
cap_null_cap_new(), NULL,
cap_null_cap_new(), NULL,
0, cap_null_cap_new(), NULL,
sc, thread_control_update_mcp |
thread_control_update_priority | thread_control_update_sc);
#else
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), NULL,
0, newMcp, newPrio,
@ -1102,6 +1191,7 @@ exception_t decodeSetSchedParams(cap_t cap, word_t length, extra_caps_t excaps,
0, cap_null_cap_new(),
NULL, thread_control_update_mcp |
thread_control_update_priority);
#endif
}
@ -1140,6 +1230,15 @@ exception_t decodeSetIPCBuffer(cap_t cap, word_t length, cte_t *slot,
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), slot,
0, NULL_PRIO, NULL_PRIO,
cap_null_cap_new(), NULL,
cap_null_cap_new(), NULL,
cptr_bufferPtr, bufferCap,
bufferSlot, NULL, thread_control_update_ipc_buffer);
#else
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), slot,
0, NULL_PRIO, NULL_PRIO,
@ -1147,6 +1246,8 @@ exception_t decodeSetIPCBuffer(cap_t cap, word_t length, cte_t *slot,
cap_null_cap_new(), NULL,
cptr_bufferPtr, bufferCap,
bufferSlot, thread_control_update_ipc_buffer);
#endif
}
exception_t decodeSetSpace(cap_t cap, word_t length, cte_t *slot,
@ -1216,6 +1317,15 @@ exception_t decodeSetSpace(cap_t cap, word_t length, cte_t *slot,
}
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
#ifdef CONFIG_KERNEL_MCS
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), slot,
faultEP,
NULL_PRIO, NULL_PRIO,
cRootCap, cRootSlot,
vRootCap, vRootSlot,
0, cap_null_cap_new(), NULL, NULL, thread_control_update_space);
#else
return invokeTCB_ThreadControl(
TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)), slot,
faultEP,
@ -1223,6 +1333,7 @@ exception_t decodeSetSpace(cap_t cap, word_t length, cte_t *slot,
cRootCap, cRootSlot,
vRootCap, vRootSlot,
0, cap_null_cap_new(), NULL, thread_control_update_space);
#endif
}
exception_t decodeDomainInvocation(word_t invLabel, word_t length, extra_caps_t excaps, word_t *buffer)
@ -1347,6 +1458,15 @@ exception_t invokeTCB_Resume(tcb_t *thread)
return EXCEPTION_NONE;
}
#ifdef CONFIG_KERNEL_MCS
exception_t invokeTCB_ThreadControl(tcb_t *target, cte_t *slot,
cptr_t faultep, prio_t mcp, prio_t priority,
cap_t cRoot_newCap, cte_t *cRoot_srcSlot,
cap_t vRoot_newCap, cte_t *vRoot_srcSlot,
word_t bufferAddr, cap_t bufferCap,
cte_t *bufferSrcSlot, sched_context_t *sc,
thread_control_flag_t updateFlags)
#else
exception_t invokeTCB_ThreadControl(tcb_t *target, cte_t *slot,
cptr_t faultep, prio_t mcp, prio_t priority,
cap_t cRoot_newCap, cte_t *cRoot_srcSlot,
@ -1354,6 +1474,7 @@ exception_t invokeTCB_ThreadControl(tcb_t *target, cte_t *slot,
word_t bufferAddr, cap_t bufferCap,
cte_t *bufferSrcSlot,
thread_control_flag_t updateFlags)
#endif
{
exception_t e;
cap_t tCap = cap_thread_cap_new((word_t)target);
@ -1370,6 +1491,16 @@ exception_t invokeTCB_ThreadControl(tcb_t *target, cte_t *slot,
setPriority(target, priority);
}
#ifdef CONFIG_KERNEL_MCS
if (updateFlags & thread_control_update_sc) {
if (sc != NULL && sc != target->tcbSchedContext) {
schedContext_bindTCB(sc, target);
} else if (sc == NULL && target->tcbSchedContext != NULL) {
schedContext_unbindTCB(target->tcbSchedContext, target);
}
}
#endif
if (updateFlags & thread_control_update_space) {
cte_t *rootSlot;