Add scheduling context support in seL4_libs
Only works if CONFIG_KERNEL_RT is enabled, however most of the code
is compiled no mater what to lighten the maintenance burden
diff --git a/libsel4simple-default/src/libsel4simple-default.c b/libsel4simple-default/src/libsel4simple-default.c
index a3313ee..536c29e 100644
--- a/libsel4simple-default/src/libsel4simple-default.c
+++ b/libsel4simple-default/src/libsel4simple-default.c
@@ -180,6 +180,17 @@
debug_print_bootinfo(data);
}
+seL4_CPtr simple_default_sched_control(void *data, int core)
+{
+ assert(core < simple_default_core_count(data));
+#if CONFIG_KERNEL_RT
+ return ((seL4_BootInfo) data)->schedcontrol.start + core;
+#else
+ ZF_LOGW("not implemented");
+ return seL4_CapNull;
+#endif
+}
+
seL4_Word simple_default_arch_info(void *data) {
if (data == NULL) {
ZF_LOGE("Data is null!");
@@ -251,6 +262,7 @@
simple->core_count = &simple_default_core_count;
simple->nth_userimage = &simple_default_nth_userimage;
simple->print = &simple_default_print;
+ simple->sched_ctrl = &simple_default_sched_control;
simple->arch_info = &simple_default_arch_info;
simple->extended_bootinfo_len = &simple_default_get_extended_bootinfo_size;
simple->extended_bootinfo = &simple_default_get_extended_bootinfo;
diff --git a/libsel4simple/include/simple/simple.h b/libsel4simple/include/simple/simple.h
index 505b544..e73a493 100644
--- a/libsel4simple/include/simple/simple.h
+++ b/libsel4simple/include/simple/simple.h
@@ -178,6 +178,12 @@
typedef seL4_Error (*simple_get_iospace_fn)(void *data, uint16_t domainID, uint16_t deviceID, cspacepath_t *path);
#endif
+/*
+ * Get the sched ctrl for the requested core (0 for uniprocessor).
+ * @return seL4_CapNull if CONFIG_RT is disabled
+ */
+typedef seL4_CPtr (*simple_get_sched_ctrl_fn)(void *data, int core);
+
/**
*
* Get simple to print all the information it has about its environment
@@ -232,6 +238,7 @@
simple_get_nth_userimage_fn nth_userimage;
simple_get_core_count_fn core_count;
simple_print_fn print;
+ simple_get_sched_ctrl_fn sched_ctrl;
simple_get_arch_info_fn arch_info;
simple_get_extended_bootinfo_len_fn extended_bootinfo_len;
simple_get_extended_bootinfo_fn extended_bootinfo;
@@ -409,6 +416,16 @@
}
static inline seL4_CPtr
+simple_get_sc(UNUSED simple_t *simple)
+{
+#ifdef CONFIG_KERNEL_RT
+ return simple_init_cap(simple, seL4_CapInitThreadSC);
+#else
+ return seL4_CapNull;
+#endif
+}
+
+static inline seL4_CPtr
simple_get_pd(simple_t *simple)
{
return simple_init_cap(simple, seL4_CapInitThreadPD);
@@ -576,6 +593,25 @@
simple->print(simple->data);
}
+static inline seL4_CPtr
+simple_get_sched_ctrl(simple_t *simple, int core)
+{
+ if (!simple) {
+ ZF_LOGE("Simple is NULL");
+ return seL4_CapNull;
+ }
+ if (!simple->sched_ctrl) {
+ ZF_LOGE("%s not implemented", __FUNCTION__);
+ return seL4_CapNull;
+ }
+ if (core >= simple_get_core_count(simple)) {
+ ZF_LOGE("invalid core");
+ return seL4_CapNull;
+ }
+
+ return simple->sched_ctrl(simple->data, core);
+}
+
static inline seL4_Word
simple_get_arch_info(simple_t *simple)
{
diff --git a/libsel4utils/include/sel4utils/process.h b/libsel4utils/include/sel4utils/process.h
index 7abe9cd..ec3731c 100644
--- a/libsel4utils/include/sel4utils/process.h
+++ b/libsel4utils/include/sel4utils/process.h
@@ -86,8 +86,11 @@
/* the slot for this processes tcb */
SEL4UTILS_TCB_SLOT = 5,
+ /* the slot for this processes sc */
+ SEL4UTILS_SCHED_CONTEXT_SLOT = 6,
+
/* First free slot in the cspace configured by sel4utils */
- SEL4UTILS_FIRST_FREE = 6
+ SEL4UTILS_FIRST_FREE = 7
};
/**
@@ -148,6 +151,8 @@
* It creates a simple cspace and vspace for you, allocates a fault endpoint and puts
* it into the new cspace. The process will start at priority 0.
*
+ * If CONFIG_RT is enabled, it will not have a scheduling context.
+ *
* It loads the elf file into the new vspace, parses the elf file and stores the entry point
* into process->entry_point.
*
diff --git a/libsel4utils/include/sel4utils/process_config.h b/libsel4utils/include/sel4utils/process_config.h
index 8c6aeee..f60764b 100644
--- a/libsel4utils/include/sel4utils/process_config.h
+++ b/libsel4utils/include/sel4utils/process_config.h
@@ -185,5 +185,13 @@
config = process_config_create_cnode(config, CONFIG_SEL4UTILS_CSPACE_SIZE_BITS);
config = process_config_create_vspace(config, NULL, 0);
config = process_config_create_fault_endpoint(config);
+
+ uint64_t timeslice = 0;
+#ifdef CONFIG_BOOT_THREAD_TIME_SLICE
+ timeslice = CONFIG_BOOT_THREAD_TIME_SLICE;
+#else
+ timeslice = CONFIG_TIMER_TICK_MS;
+#endif
+ config.sched_params = sched_params_round_robin(config.sched_params, simple, 0, timeslice * US_IN_MS);
return process_config_priority(config, prio);
}
diff --git a/libsel4utils/include/sel4utils/thread.h b/libsel4utils/include/sel4utils/thread.h
index 138aba7..e1128e5 100644
--- a/libsel4utils/include/sel4utils/thread.h
+++ b/libsel4utils/include/sel4utils/thread.h
@@ -38,11 +38,13 @@
typedef struct sel4utils_thread {
vka_object_t tcb;
+ vka_object_t sched_context;
void *stack_top;
void *initial_stack_pointer;
size_t stack_size;
seL4_CPtr ipc_buffer;
seL4_Word ipc_buffer_addr;
+ bool own_sc;
} sel4utils_thread_t;
typedef struct sel4utils_checkpoint {
@@ -56,6 +58,8 @@
/**
* Configure a thread, allocating any resources required. The thread will start at priority 0.
*
+ * If CONFIG_RT is enabled, the thread will not have a scheduling context, so it will not be able to run.
+ *
* @param vka initialised vka to allocate objects with
* @param parent vspace structure of the thread calling this function, used for temporary mappings
* @param alloc initialised vspace structure to allocate virtual memory with
@@ -175,6 +179,8 @@
* Start a fault handling thread that will print the name of the thread that faulted
* as well as debugging information. The thread will start at priority 0.
*
+ * If CONFIG_RT it be passive (not have a scheulding context) and will run on the SC of the faulter.
+ *
* @param fault_endpoint the fault_endpoint to wait on
* @param vka allocator
* @param vspace vspace (this library must be mapped into that vspace).
diff --git a/libsel4utils/include/sel4utils/thread_config.h b/libsel4utils/include/sel4utils/thread_config.h
index 169b8ad..62adbef 100644
--- a/libsel4utils/include/sel4utils/thread_config.h
+++ b/libsel4utils/include/sel4utils/thread_config.h
@@ -29,6 +29,17 @@
uint8_t mcp;
/* TCB to derive MCP from when setting priority/mcp (in future API) */
seL4_CPtr auth;
+ /* true if sel4utils should create an sc */
+ bool create_sc;
+ /* sel4 sched control cap for creating sc */
+ seL4_CPtr sched_ctrl;
+ /* scheduling parameters */
+ uint64_t period;
+ uint64_t budget;
+ seL4_Word extra_refills;
+ seL4_Word badge;
+ /* otherwise use this provided sc */
+ seL4_CPtr sched_context;
} sched_params_t;
typedef struct sel4utils_thread_config {
@@ -48,6 +59,36 @@
sched_params_t sched_params;
} sel4utils_thread_config_t;
+static inline sched_params_t
+sched_params_periodic(sched_params_t params, simple_t *simple, seL4_Word core, uint64_t period_us,
+ uint64_t budget_us, seL4_Word extra_refills, seL4_Word badge)
+{
+ if (!config_set(CONFIG_KERNEL_RT)) {
+ ZF_LOGW("Setting sched params on non-RT kernel will have no effect");
+ }
+ params.sched_ctrl = simple_get_sched_ctrl(simple, core);
+ params.period = period_us;
+ params.budget = budget_us;
+ params.extra_refills = extra_refills;
+ params.badge = badge;
+ params.create_sc = true;
+ return params;
+}
+
+static inline sched_params_t
+sched_params_round_robin(sched_params_t params, simple_t *simple, seL4_Word core, uint64_t timeslice_us)
+{
+ return sched_params_periodic(params, simple, core, timeslice_us, timeslice_us, 0, 0);
+}
+
+static inline sel4utils_thread_config_t
+thread_config_sched_context(sel4utils_thread_config_t config, seL4_CPtr sched_context)
+{
+ config.sched_params.create_sc = false;
+ config.sched_params.sched_context = sched_context;
+ return config;
+}
+
static inline sel4utils_thread_config_t
thread_config_cspace(sel4utils_thread_config_t config, seL4_CPtr cspace_root, seL4_CapData_t cspace_root_data)
{
@@ -115,5 +156,13 @@
config = thread_config_cspace(config, cnode, data);
config = thread_config_fault_endpoint(config, fault_ep);
config = thread_config_priority(config, prio);
+ uint64_t timeslice;
+#ifdef CONFIG_BOOT_THREAD_TIME_SLICE
+ timeslice = CONFIG_BOOT_THREAD_TIME_SLICE;
+#else
+ timeslice = CONFIG_TIMER_TICK_MS;
+#endif
+ config.sched_params = sched_params_round_robin(config.sched_params, simple, 0, timeslice * US_IN_MS);
+ config = thread_config_create_reply(config);
return config;
}
diff --git a/libsel4utils/src/process.c b/libsel4utils/src/process.c
index 5f67ecc..4e5d4f4 100644
--- a/libsel4utils/src/process.c
+++ b/libsel4utils/src/process.c
@@ -621,6 +621,11 @@
thread_config.sched_params = config.sched_params;
error = sel4utils_configure_thread_config(vka, spawner_vspace, &process->vspace, thread_config,
&process->thread);
+ if (error) {
+ ZF_LOGE("ERROR: failed to configure thread for new process %d\n", error);
+ goto error;
+ }
+
/* copy tcb cap to cspace */
if (config.create_cspace) {
cspacepath_t src;
@@ -630,11 +635,16 @@
process->dest_tcb_cptr = SEL4UTILS_TCB_SLOT;
} else {
process->dest_tcb_cptr = config.dest_cspace_tcb_cptr;
+ /* skip the tcb slot */
+ allocate_next_slot(process);
}
- if (error) {
- ZF_LOGE("ERROR: failed to configure thread for new process %d\n", error);
- goto error;
+ if (config.create_cspace && config_set(CONFIG_KERNEL_RT)) {
+ slot = sel4utils_copy_cap_to_process(process, vka, process->thread.sched_context.cptr);
+ assert(slot == SEL4UTILS_SCHED_CONTEXT_SLOT);
+ } else {
+ /* skip the sc slot */
+ allocate_next_slot(process);
}
return 0;
@@ -730,6 +740,10 @@
return SEL4UTILS_PD_SLOT;
case seL4_CapInitThreadASIDPool:
return SEL4UTILS_ASID_POOL_SLOT;
+#ifdef CONFIG_KERNEL_RT
+ case seL4_CapInitThreadSC:
+ return SEL4UTILS_SCHED_CONTEXT_SLOT;
+#endif
default:
ZF_LOGE("sel4utils does not copy this cap (%zu) to new processes", cap);
return seL4_CapNull;
@@ -758,4 +772,4 @@
vka, from->objs[i].obj.cptr);
}
return 0;
-}
\ No newline at end of file
+}
diff --git a/libsel4utils/src/thread.c b/libsel4utils/src/thread.c
index 98399ee..7d42149 100644
--- a/libsel4utils/src/thread.c
+++ b/libsel4utils/src/thread.c
@@ -78,9 +78,36 @@
}
}
+ if (config_set(CONFIG_KERNEL_RT) && config.sched_params.create_sc) {
+ /* allocate a scheduling context */
+ if (vka_alloc_sched_context(vka, &res->sched_context)) {
+ ZF_LOGE("Failed to allocate sched context");
+ sel4utils_clean_up_thread(vka, alloc, res);
+ return -1;
+ }
+
+ /* configure the scheduling context */
+#ifdef CONFIG_KERNEL_RT
+ error = seL4_SchedControl_Configure(config.sched_params.sched_ctrl, res->sched_context.cptr,
+ config.sched_params.budget, config.sched_params.period,
+ config.sched_params.extra_refills);
+#endif
+ if (error != seL4_NoError) {
+ ZF_LOGE("Failed to configure sched context");
+ sel4utils_clean_up_thread(vka, alloc, res);
+ return -1;
+ }
+ res->own_sc = true;
+ } else {
+ res->sched_context.cptr = config.sched_params.sched_context;
+ }
seL4_CapData_t null_cap_data = {{0}};
error = seL4_TCB_Configure(res->tcb.cptr, config.fault_endpoint,
- seL4_PrioProps_new(config.sched_params.mcp, config.sched_params.priority), config.cspace,
+ seL4_PrioProps_new(config.sched_params.mcp, config.sched_params.priority),
+#ifdef CONFIG_KERNEL_RT
+ res->sched_context.cptr,
+#endif
+ config.cspace,
config.cspace_root_data, vspace_get_root(alloc), null_cap_data, res->ipc_buffer_addr, res->ipc_buffer);
if (error != seL4_NoError) {
@@ -146,6 +173,10 @@
vspace_free_sized_stack(alloc, thread->stack_top, thread->stack_size);
}
+ if (thread->own_sc && thread->sched_context.cptr != 0) {
+ vka_free_object(vka, &thread->sched_context);
+ }
+
memset(thread, 0, sizeof(sel4utils_thread_t));
}
diff --git a/libsel4vka/include/vka/kobject_t.h b/libsel4vka/include/vka/kobject_t.h
index 4a21499..aa82f7e 100644
--- a/libsel4vka/include/vka/kobject_t.h
+++ b/libsel4vka/include/vka/kobject_t.h
@@ -28,6 +28,7 @@
KOBJECT_UNTYPED,
KOBJECT_ENDPOINT,
KOBJECT_NOTIFICATION,
+ KOBJECT_SCHED_CONTEXT,
#ifdef CONFIG_CACHE_COLORING
KOBJECT_KERNEL_IMAGE,
#endif
@@ -63,6 +64,10 @@
return seL4_PageDirBits;
case KOBJECT_PAGE_TABLE:
return seL4_PageTableBits;
+#ifdef CONFIG_KERNEL_RT
+ case KOBJECT_SCHED_CONTEXT:
+ return objectSize > seL4_MinSchedContextBits ? objectSize : seL4_MinSchedContextBits;
+#endif
#ifdef CONFIG_CACHE_COLORING
case KOBJECT_KERNEL_IMAGE:
return seL4_KernelImageBits;
@@ -89,6 +94,10 @@
return seL4_EndpointObject;
case KOBJECT_NOTIFICATION:
return seL4_NotificationObject;
+#ifdef CONFIG_KERNEL_RT
+ case KOBJECT_SCHED_CONTEXT:
+ return seL4_SchedContextObject;
+#endif
#ifdef CONFIG_CACHE_COLORING
case KOBJECT_KERNEL_IMAGE:
return seL4_KernelImageObject;
diff --git a/libsel4vka/include/vka/object.h b/libsel4vka/include/vka/object.h
index fc3fa8f..d18019f 100644
--- a/libsel4vka/include/vka/object.h
+++ b/libsel4vka/include/vka/object.h
@@ -14,6 +14,7 @@
#define __VKA_OBJECT_H__
#include <assert.h>
+#include <errno.h>
#include <vka/vka.h>
#include <vka/kobject_t.h>
#include <stdio.h>
@@ -143,6 +144,31 @@
{
return vka_alloc_object(vka, seL4_TCBObject, seL4_TCBBits, result);
}
+
+static inline int vka_alloc_sched_context(UNUSED vka_t *vka, UNUSED vka_object_t *result)
+{
+#ifdef CONFIG_KERNEL_RT
+ return vka_alloc_object(vka, seL4_SchedContextObject, seL4_MinSchedContextBits, result);
+#else
+ ZF_LOGW("Allocating sched context on non RT kernel");
+ return ENOSYS;
+#endif
+}
+
+static inline int vka_alloc_sched_context_size(UNUSED vka_t *vka, UNUSED vka_object_t *result, UNUSED uint32_t size_bits)
+{
+#ifdef CONFIG_KERNEL_RT
+ if (size_bits < seL4_MinSchedContextBits) {
+ ZF_LOGE("Invalid size bits for sc");
+ return -1;
+ }
+ return vka_alloc_object(vka, seL4_SchedContextObject, size_bits, result);
+#else
+ ZF_LOGW("Allocating sched context on non RT kernel");
+ return ENOSYS;
+#endif
+}
+
static inline int vka_alloc_endpoint(vka_t *vka, vka_object_t *result)
{
return vka_alloc_object(vka, seL4_EndpointObject, seL4_EndpointBits, result);
@@ -228,6 +254,7 @@
LEAKY(notification)
LEAKY(page_directory)
LEAKY(page_table)
+LEAKY(sched_context)
static inline DEPRECATED("use vka_alloc_notification_leaky") seL4_CPtr
vka_alloc_async_endpoint_leaky(vka_t *vka)
@@ -265,6 +292,10 @@
return objectSize;
case seL4_TCBObject:
return seL4_TCBBits;
+#ifdef CONFIG_KERNEL_RT
+ case seL4_SchedContextObject:
+ return objectSize > seL4_MinSchedContextBits ? objectSize : seL4_MinSchedContextBits;
+#endif
case seL4_EndpointObject:
return seL4_EndpointBits;
case seL4_NotificationObject:
diff --git a/libsel4vmm/include/vmm/vmm.h b/libsel4vmm/include/vmm/vmm.h
index 252002b..597f96b 100644
--- a/libsel4vmm/include/vmm/vmm.h
+++ b/libsel4vmm/include/vmm/vmm.h
@@ -109,6 +109,8 @@
/* TCB of the VMM thread
* TODO: Should eventually have one vmm thread per vcpu */
seL4_CPtr tcb;
+ seL4_CPtr sc;
+ seL4_CPtr sched_ctrl;
/* platform callback functions */
platform_callbacks_t plat_callbacks;
diff --git a/libsel4vmm/src/platform/boot.c b/libsel4vmm/src/platform/boot.c
index 9338eca..1b92d1f 100644
--- a/libsel4vmm/src/platform/boot.c
+++ b/libsel4vmm/src/platform/boot.c
@@ -37,6 +37,8 @@
vmm->host_vspace = vspace;
vmm->plat_callbacks = callbacks;
vmm->tcb = simple_get_tcb(&simple);
+ vmm->sc = simple_get_sc(&simple);
+ vmm->sched_ctrl = simple_get_sched_ctrl(&simple, 0);
// Currently set this to 4k pages by default
vmm->page_size = seL4_PageBits;
err = vmm_pci_init(&vmm->pci);
