[llenotre]

A lot of memory and concurrency issues have been eliminated. It is still a pain to debug, but a lot less than it was before though.

As an example, there is not a lot of chances you forget to use a mutex since the compiler would remind it to you by an error.

This is not a silver bullet though, things such as deadlocks are still present. Especially with interruptions.

To give an example, if you decide to lock a mutex, then an interruption happens, the code that locks the mutex will stop running until the interruption is over. If the interruption itself tries to lock the same mutex, then you have a deadlock, and the typing system cannot help you with this kind of problem.

The solution is to disable interruptions handling while the mutex is locked, but the compiler cannot enforce it.

[claytonwramsey]

If you’re willing to implement your own mutex, it actually is possible to enforce! You could make disabling interrupts emit a token and then require the mutex to accept that token as a parameter to its locking behavior.

[epcoa]

But what forces you to declare the correct interrupt policy as it may not be the same for all uses of even the same mutex?

[loeg]

How would you enforce use of (only) the correct kind of mutex in interrupt context?

[colonwqbang]

In Haskell this should be "easy" to do using monads. You would have a process monad and an atomic monad (using Linux terminology). The operation to lock a sleeping mutex would live in the process monad. It would be possible to lift an atomic computation into process context (disabling interrupts) but not the other way around.

I don't think rust has such a concept of different computation contexts (does it?)

Of course Haskell may not be the most suitable kernel implementation language for other reasons...

[RetroTechie]

> Of course Haskell may not be the most suitable kernel implementation language for other reasons...

seL4 microkernel would like to have a word with you..

[smaddox]

You would probably need to pass around a context type that encodes information about the current context and which interrupts are possible. You would then acquire the lock via that context, which would handle disabling those interrupts.

[loeg]

Still need to set the context correctly on entry to your interrupt handlers, I guess, and passing it around is kind of ugly. In C kernels you often stash contexts in CPU-locale variables, maybe you could do something like that instead of passing it around.

[smaddox]

CPU-local could work, but would give up the possibility of static type verification. Agree passing around context can be tedious, but Rust currently doesn't have a way to implicitly pass context (although there have been some proposals along those lines).

[agentultra]

I suspect those sort of liveness properties (and likely some safety properties in unsafe code) cannot be encoded in Rust's type system and you'd have to use a model checker at some point.

Still, it's cool to see such a system used and providing immediate benefits. Happy hacking!