At the seL4 Summit held in Munich, October 2022, there were group discussion sessions on several topics. At a meeting of the seL4 Technical Steering Committee later in the year, it was resolved to form special interest groups around some of these topics. I volunteered to chair a special interest group (SIG) on seL4 multi-core and user-level verification.
This discourse channel (SIG Multicore & User-Level Verification - seL4) will be the home of this special interest group.
Purpose
The SIG seL4 multi-core & user-level verification exists to foster collaboration between people with an interest in extending the seL4 verification story to support:
- Verification of kernel configurations utilising multiple cores, including multi-kernel and symmetric multi-processor (SMP) configurations.
- Verification of user-space components, their interactions with each other and with seL4, and properties of systems of user-space components.
The subtopics are related, because:
- A rigorous treatment of either subtopic requires reasoning about concurrency involving both kernel and user space. Reasoning about concurrency is difficult, so we should try to avoid duplicating effort.
- Proofs about multi-core seL4 will be most useful when they can be connected to proofs about user-space systems, and vice versa.
With this SIG, we hope to:
- Increase awareness of what is currently possible, and what we would like to make possible in future.
- Identify opportunities for collaboration.
- Provide a forum for clarifying goals, co-ordinating efforts, and reporting progress.
Scope
While we are still clarifying our goals, we will consider a broad scope covering anything related the subtopics noted above. Examples of the kinds of posts I’d like to see in this channel:
- Discussions about how businesses and other organisations think about their needs for multi-core and user-level verification.
- Discussion of the applicability of the existing single-core seL4 proofs to multi-kernel configurations.
- Reports on previous work on multi-core seL4 verification, and future plans.
- Reports on experiences verifying code that will run in seL4 user space, or designs for systems that will run on seL4. What are your goals? What is your approach? Is there anything missing?
- Questions about any of these topics, or anything else you think is relevant.
Initial plan
Over the next month or two, I will invite some people to post updates about work they’ve been doing that is relevant to this SIG. We can then look at identifying some common goals.
Of course, you don’t need to wait for my invitation. If you have something to say, then speak up!