"When multiple threads need to share a resource, they can pass ownership through channels. However, as we discuss in the rest of this paper, it does not work well in systems that use non threadbased concurrency models and when resources must be shared [...]
While hardware interrupts are asynchronous, and therefore run concurrently with other kernel code, in our operating system interrupt handlers enqueue tasks to be run in the main scheduler loop, which is single-threaded. As a result, on_receive and send can never run concurrently and no data race is possible. We overcome both issues by declaring most resources as static variables and borrowing them with ’static lifetime. [...]
Being able to mutably borrow static variables multiple times means our operating system can allow multiple drivers to reference hardware resources or each other. However, doing so means we lose the ability to detect real data races at compile time, for example, if the kernel passes a shared resource to an interrupt handler that may run concurrently. Instead, we resort to an overly conservative convention in which interrupt handlers perform no work except posting to the main scheduler’s task queue. An ideal mechanism would, instead, allow for shared state between components that will never run concurrently, but disallow sharing when they may."