State of cache coloring support

seL4 kernel
1

I’ve read about and watched talks that mentioned cache coloring support on seL4. The most detailed of these sources was this PhD thesis which also describes a kernel image cloning feature to move the kernel image to user supplied (colored) pages.

Looking for some reference to either “cache colouring” or “kernel image object”, all I could find are a couple of enums in the vka library which only seem to be used in a couple of utility functions, .e.g.:

static inline unsigned long
vka_get_object_size(seL4_Word objectType, seL4_Word objectSize)
{
...
#ifdef CONFIG_CACHE_COLORING
    case seL4_KernelImageObject:
        return seL4_KernelImageBits;
#endif
...
}

I’d like to know which is the state of this functionality in the upstream kernel and surrounding userspace libraries. Specifically, is it possible to specify cache partitions in the CAmkES framework? If not, is it in the project’s roadmap?

Thanks,
José

2

The current mainline kernel does not yet contain the kernel image cloning features and corresponding cache colouring code. Some of the user-level libraries may already have configuration options for it, but it’s a work in progress.

There is a research project in progress that is aiming to mature the features enough to bring them into the verified kernel. Hopefully we will see first merges from that into the official repo in the next year.

With the current seL4 features, you can already do cache colouring for user-level memory and code and also for dynamically created kernel objects by partitioning untyped capabilities according to cache colour. What is missing is the same for kernel code and kernel-global data structures.

Cheers,
Gerwin

1 Like
3

Hello Gerwin, thank you for your reply!

The current mainline kernel does not yet contain the kernel image cloning features and corresponding cache colouring code. Some of the user-level libraries may already have configuration options for it, but it’s a work in progress.

There is a research project in progress that is aiming to mature the features enough to bring them into the verified kernel. Hopefully we will see first merges from that into the official repo in the next year.

Even if not finished, I’d still be interested in taking a look at what is there. Is this WIP repo public? If so, can you point me to it?

Also, I’d be mostly interested in using such a feature in the camkes-vm. Are there plans to extend support for coloring and automating it in the context of the camkes framework? Ideally, one would be able to specify which colors would be used to allocate memory for a VMM/VM combination in the VM .camkes configuration file.