diff --git a/config.cmake b/config.cmake index a479eb790..4f7d43a79 100644 --- a/config.cmake +++ b/config.cmake @@ -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 diff --git a/configs/seL4Config.cmake b/configs/seL4Config.cmake index 5c0b1bf20..72ea4ed3d 100644 --- a/configs/seL4Config.cmake +++ b/configs/seL4Config.cmake @@ -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 diff --git a/include/32/mode/api/ipc_buffer.h b/include/32/mode/api/ipc_buffer.h new file mode 100644 index 000000000..c0577ad38 --- /dev/null +++ b/include/32/mode/api/ipc_buffer.h @@ -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 +#include + +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 */ diff --git a/include/64/mode/api/ipc_buffer.h b/include/64/mode/api/ipc_buffer.h new file mode 100644 index 000000000..add412fa0 --- /dev/null +++ b/include/64/mode/api/ipc_buffer.h @@ -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 +#include + +static inline ticks_t mode_parseTimeArg(word_t i, word_t *buffer) +{ + return getSyscallArg(i, buffer); +} + +#endif /* __IPC_BUFFER_H */ diff --git a/include/api/syscall.h b/include/api/syscall.h index 49b88dcb3..e947ddb8e 100644 --- a/include/api/syscall.h +++ b/include/api/syscall.h @@ -19,6 +19,8 @@ #include #include +#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); diff --git a/include/api/types.h b/include/api/types.h index c26fe9285..f5033d7e9 100644 --- a/include/api/types.h +++ b/include/api/types.h @@ -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, diff --git a/include/arch/arm/arch/32/mode/object/structures.bf b/include/arch/arm/arch/32/mode/object/structures.bf index 48a46f38d..5ae2ffc9e 100644 --- a/include/arch/arm/arch/32/mode/object/structures.bf +++ b/include/arch/arm/arch/32/mode/object/structures.bf @@ -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 diff --git a/include/arch/arm/arch/64/mode/object/structures.bf b/include/arch/arm/arch/64/mode/object/structures.bf index a6344adef..d089b4bd5 100644 --- a/include/arch/arm/arch/64/mode/object/structures.bf +++ b/include/arch/arm/arch/64/mode/object/structures.bf @@ -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 diff --git a/include/arch/x86/arch/32/mode/object/structures.bf b/include/arch/x86/arch/32/mode/object/structures.bf index 682b95665..f00e3e775 100644 --- a/include/arch/x86/arch/32/mode/object/structures.bf +++ b/include/arch/x86/arch/32/mode/object/structures.bf @@ -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 diff --git a/include/arch/x86/arch/64/mode/object/structures.bf b/include/arch/x86/arch/64/mode/object/structures.bf index cec61e251..04fa39cca 100644 --- a/include/arch/x86/arch/64/mode/object/structures.bf +++ b/include/arch/x86/arch/64/mode/object/structures.bf @@ -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 diff --git a/include/config.h b/include/config.h index 5d737adca..a88d58f29 100644 --- a/include/config.h +++ b/include/config.h @@ -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 diff --git a/include/kernel/boot.h b/include/kernel/boot.h index 0066ab524..f1680ced3 100644 --- a/include/kernel/boot.h +++ b/include/kernel/boot.h @@ -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; diff --git a/include/model/statedata.h b/include/model/statedata.h index 2f3f0ac42..d515e8cdb 100644 --- a/include/model/statedata.h +++ b/include/model/statedata.h @@ -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 */ diff --git a/include/object/schedcontext.h b/include/object/schedcontext.h new file mode 100644 index 000000000..6764d0579 --- /dev/null +++ b/include/object/schedcontext.h @@ -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 +#include +#include + +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 */ diff --git a/include/object/schedcontrol.h b/include/object/schedcontrol.h new file mode 100644 index 000000000..ec8dfa7c8 --- /dev/null +++ b/include/object/schedcontrol.h @@ -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 +#include +#include + +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 */ diff --git a/include/object/structures.h b/include/object/structures.h index 184d42d38..48d681013 100644 --- a/include/object/structures.h +++ b/include/object/structures.h @@ -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); diff --git a/include/object/structures_32.bf b/include/object/structures_32.bf index 77ad3b316..c9e58386e 100644 --- a/include/object/structures_32.bf +++ b/include/object/structures_32.bf @@ -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 diff --git a/include/object/structures_64.bf b/include/object/structures_64.bf index d1de87c19..655b43f4c 100644 --- a/include/object/structures_64.bf +++ b/include/object/structures_64.bf @@ -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 diff --git a/include/object/tcb.h b/include/object/tcb.h index 3a3d7e365..25424b855 100644 --- a/include/object/tcb.h +++ b/include/object/tcb.h @@ -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, diff --git a/libsel4/include/interfaces/sel4.xml b/libsel4/include/interfaces/sel4.xml index ea96af15c..d1649f4fc 100644 --- a/libsel4/include/interfaces/sel4.xml +++ b/libsel4/include/interfaces/sel4.xml @@ -165,7 +165,7 @@ description="The thread's new maximum controlled priority."/> - + Change a thread's priority and maximum controlled priority. @@ -179,6 +179,22 @@ + + + Change a thread's priority, maximum controlled priority, and scheduling context. + + + See + + + + + + @@ -249,7 +265,7 @@ - + Change a thread's current CPU in multicore machine @@ -577,6 +593,86 @@ + + + + + + + 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). + + + See + + + + + + + + + + + + + + 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. + + + See + + + + + + + + Unbind any objects (threads or notification objects) from a scheduling context. This + will render the bound thread passive, see Section 6.1.5. + + + See + + + + + + + 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. + + + See + + + + diff --git a/libsel4/include/sel4/bootinfo_types.h b/libsel4/include/sel4/bootinfo_types.h index 5f4dfe4dc..84ac9f81a 100644 --- a/libsel4/include/sel4/bootinfo_types.h +++ b/libsel4/include/sel4/bootinfo_types.h @@ -13,6 +13,10 @@ #ifndef __LIBSEL4_BOOTINFO_TYPES_H #define __LIBSEL4_BOOTINFO_TYPES_H +#ifdef HAVE_AUTOCONF +#include +#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 diff --git a/libsel4/include/sel4/objecttype.h b/libsel4/include/sel4/objecttype.h index 0499d8e15..bc854fae9 100644 --- a/libsel4/include/sel4/objecttype.h +++ b/libsel4/include/sel4/objecttype.h @@ -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; diff --git a/libsel4/include/sel4/types.h b/libsel4/include/sel4/types.h index 2ff1cf9f9..704a2c8f1 100644 --- a/libsel4/include/sel4/types.h +++ b/libsel4/include/sel4/types.h @@ -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 diff --git a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h index c4d1bd33e..a6d983e8a 100644 --- a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h +++ b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h @@ -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 diff --git a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h index c3cafdb1e..d158a652c 100644 --- a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h +++ b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h @@ -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 diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h index 0409341e5..b0656529d 100644 --- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h +++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h @@ -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 diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h index cb6009993..05d338f35 100644 --- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h +++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h @@ -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 diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py index 460582d97..46ea99998 100644 --- a/libsel4/tools/syscall_stub_gen.py +++ b/libsel4/tools/syscall_stub_gen.py @@ -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 diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex index 1eec71d3b..d48ac01e1 100644 --- a/manual/parts/threads.tex +++ b/manual/parts/threads.tex @@ -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} diff --git a/src/arch/arm/kernel/boot.c b/src/arch/arm/kernel/boot.c index 615833b69..02850890a 100644 --- a/src/arch/arm/kernel/boot.c +++ b/src/arch/arm/kernel/boot.c @@ -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) { diff --git a/src/arch/x86/kernel/boot.c b/src/arch/x86/kernel/boot.c index a355ad877..0386cf723 100644 --- a/src/arch/x86/kernel/boot.c +++ b/src/arch/x86/kernel/boot.c @@ -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); diff --git a/src/config.cmake b/src/config.cmake index 07617387d..7009b7425 100644 --- a/src/config.cmake +++ b/src/config.cmake @@ -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) diff --git a/src/kernel/boot.c b/src/kernel/boot.c index 9619659a3..9e73cab91 100644 --- a/src/kernel/boot.c +++ b/src/kernel/boot.c @@ -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 diff --git a/src/kernel/thread.c b/src/kernel/thread.c index 5b09c0c7e..c59a69c03 100644 --- a/src/kernel/thread.c +++ b/src/kernel/thread.c @@ -16,6 +16,9 @@ #include #include #include +#ifdef CONFIG_KERNEL_MCS +#include +#endif #include #include #include @@ -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; diff --git a/src/model/statedata.c b/src/model/statedata.c index e4e08aa29..3656ec70b 100644 --- a/src/model/statedata.c +++ b/src/model/statedata.c @@ -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 */ diff --git a/src/object/objecttype.c b/src/object/objecttype.c index 0faa35a4f..34e4ce82e 100644 --- a/src/object/objecttype.c +++ b/src/object/objecttype.c @@ -21,6 +21,10 @@ #include #include #include +#ifdef CONFIG_KERNEL_MCS +#include +#include +#endif #include #include #include @@ -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"); } diff --git a/src/object/schedcontext.c b/src/object/schedcontext.c new file mode 100644 index 000000000..24b9b4c0c --- /dev/null +++ b/src/object/schedcontext.c @@ -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 +#include + +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); + } +} diff --git a/src/object/schedcontrol.c b/src/object/schedcontrol.c new file mode 100644 index 000000000..efae416ad --- /dev/null +++ b/src/object/schedcontrol.c @@ -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 +#include +#include + +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; + } +} diff --git a/src/object/tcb.c b/src/object/tcb.c index 784f9f008..436f57afe 100644 --- a/src/object/tcb.c +++ b/src/object/tcb.c @@ -18,6 +18,9 @@ #include #include #include +#ifdef CONFIG_KERNEL_MCS +#include +#endif #include #include #include @@ -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;