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

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.

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.

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).

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...

> 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..

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?