Sessions Types for Microkernel Message Passing

I want to propose sessions types to whoever designs the message passing for Redox. As near as I can tell, Redox does not yet have its message passing system laid out (after a quick check of the code, forum, and book). I think there is a strong case to be made for leveraging session types in a microkernel, the biggest of which is to prevent deadlocks at compile time. I think it’s important to introduce session types early into the design process, because it would be infeasible to add later to an established kernel.

Here are some resources for researching the topic:

I hate to come to any project as an “ideas guy”; I’d much rather contribute with RFCs and PRs, but this has been bugging me for weeks. It will be at least a year before I will have time to contribute to Redox.

2 Likes

Looking at this again, it looks like a really good idea