Hacker News Reader

Comment by awelkie | Hacker News Reader

What kinds of things would you want proven correct about your code's interrupt handling?

Mostly whether the mechanism for passing data to and from the main program is sound; but also whether things like interrupt priority make sense and whether your re-trigger handling or re-entrancy are going to work properly (an interrupt happens while you're in the handler for the same interrupt). It might be sufficient simply to have a good set of primitives for this, rather than an actual proof.

Basically whether it's going to deadlock or miss interrupts. Deadlock is immediate disaster, but at least the JTAG will help you .. if the device hasn't self-destructed. Missing interrupts is worse because it's extremely hard to debug.

Forcing DMA to behave would also be great, although this isn't strictly a microcontroller issue. I've seen a few war stories where people are trying to debug memory corruption where the program is completely correct - but some other device has simply DMA'd over it. I think this was involved in https://googleprojectzero.blogspot.co.uk/2017/04/over-air-ex... too.

I believe rust's safety guarantees are enough to ensure the soundness of passing data to/from interrupt contexts and interrupt handler re-entrancy. See rtfm[0] for an example and a good explanation. I think DMA handling can be made safe by using the right abstractions, and then you'd just need to trust that any piece of code that accesses the memory uses the abstraction instead of accessing it directly.

Checking interrupt priorities sounds like an interesting problem. What is the state of the art in deadlock prevention? It would also be cool if you could tell the compiler "I need this interrupt handler to return in less than n clock cycles." I wonder if someone could write a rust compiler plugin to check that.

[0]: http://blog.japaric.io/fearless-concurrency/

Top 10 Causes of Nasty Firmware Bugs

https://embeddedgurus.com/blog/2010/12/top-10-causes-of-nast...

it would be great if all those would be easy issues, or solved.

Reply on news.ycombinator.com