Tim Retout: seL4 repo relationships
The seL4 organisation on GitHub uses git-repo to manage multiple source repositories, and so there are a large number of projects to get your head around when figuring out the ecosystem.
As an experiment, I have taken the various manifest files across the org, and constructed a graph based on how frequently each pair of repositories is mentioned in a manifest together. See below:
[This may render badly when syndicated outside of my blog; and also on small screens. And probably large screens. Iβve attempted to make sure thereβs a non-JS fallback β on my site with JS enabled, if you hover over a node, it should highlight connected nodes.]
The colouring of the nodes is mostly manual; I experimented with graph clustering algorithms but have not found a satisfactory result so far. Still, some clusters are obvious:
-
Kernel β the
seL4microkernel proper. This often but not always co-exists with the main cluster of core libraries, but it is pulled away slightly by the verification and microkit manifests. -
Verification β the verification repositories (
l4v,HOL,graph-refine,polyml,isabelle) form a very distinct group. These are connected only to the seL4 microkernel itself, which is the only component formally verified. -
Microkit β
microkitis a newer operating system framework that does not use CAmkES, so stands apart from the rest of the pack. I chose to scope this work to the seL4 org, so the LionsOS ecosystem and sDDF which are maintained by Trustworthy Systems are not shown. Also not linked isrust-sel4, because this modern world isnβt using git-repo in the main to manage its repositories. -
RefOS β Iβd not come across
refosbefore, but it appears to be an example OS from 2021 built on the seL4 kernel.
Itβs quite hard to pull apart the CAmkES framework and the core
libraries; there are definitely some which are more associated with VM
management, but the overall shape of this co-occurence data is a messy
ball in the middle with some outliers in orbit. One observation is
that camkes is correctly identified as more peripheral than
camkes-tool, which contains the actual core CAmkES code.
Reflecting on this approach, in hindsight Iβm surprised that using co-occurences worked as well as it did β there was no attempt to actually inspect the code and find direct mentions of other code e.g. library header dependencies. As the newer microkit effort largely eschews git-repo, better results might be found by actually taking that more detailed approach, so that graph edges could represent real dependencies between two packages. Additionally, this could allow diving into the various libraries held in the different βlibsβ repos, to get a more granular graph of relationships between them.
However, I think I spent more time on making it possible to render graphviz graphs easily on my blog than actually gaining any insight into the codebase!
Note: MacRumors is an affiliate partner with some of these vendors. When you click a link and make a purchase, we may receive a small payment, which helps us keep the site running.
