We recently developed a userland scheduled for MCS within the CAmKES service framework. In the process, we encountered an obstacle: The scheduling component itself must have access to the TCBs and SCs of the other application components it is designated to manage. The CAmkES infrastructure, however, in its current implementation does not have a mechanism to give the scheduling component such access. Specifically, the CapDL template instantiation support lacks a mechanism that exposes other TCBs and SCs to a component. We extended the CapDL template support with a function that satisfied this need. We present the modification here for further discussion and possible consideration to be included in the CAmkES baseline.
Several userland schedulers have been developed for MCS. As far as we are aware, all have relied upon the native seL4 system calls, instead of using the CAmkES framework. Our use case specifically targets CAmkES, so we extended the CapDL template support. The extension itself is restricted to a single new function in Python. It does not alter any prior existing functions or source code.
The new function is a variation of the “alloc” function used in CapDL templates, called “alloc_ent.” It allocates an object in the CapDL database, and it also exposes the TCBs and SCs of the object via the template.
The specific modification we made is captured in the following patch file:
diff --git a/camkes/runner/Context.py b/camkes/runner/Context.py index a483e25..5a4724d 100644 --- a/camkes/runner/Context.py +++ b/camkes/runner/Context.py @@ -87,6 +87,14 @@ def new_context(entity, assembly, render_state, state_key, outfile_name, (entity.label(), name), type, label, **kwargs), **kwargs)), + # [2021/09/21:JCC] Varient of alloc to alloc for a different entity. + 'alloc_ent': None if cap_space is None else \ + (lambda name, type, label=entity.label(), **kwargs: + alloc_cap((label, cap_space), cap_space, name, + alloc_obj((label, obj_space), obj_space, '%s_%s' % + (label, name), type, label, **kwargs), + **kwargs)), +
We called the python function “alloc_ent.” We are not stuck on the name, feel free to rename.
A poorly designed system could misuse this proposed capability in CapDL, which loosens security somewhat within CAmkES. However, the same basic capability already exists in MCS with the native system calls (by creating and assigning new TCBs and SCs), so the argument can be made that this new function in a CapDL template does not really open a new security concern.
Rationale and alternatives
CAmkES is designed so that special access to kernel data structures is defined through the CapDL and its template framework. Given that, this modest extension to CapDL is likely the best (or at least simplest) approach, assuming it is desireable for CAmkES to support a userland scheduler application.