Hi Eric, Thank you for your interest in it. For a dynamic detection solution, then the answer is yes. Lockdep, which should be enabled by CONFIG_DEBUG_SPINLOCK, has the ability to detect such deadlocks. But the problem is that the detection requires input and exact thread interleaving to trigger the bug, otherwise the bugs would be buried and cannot be detected. For static analysis, I think the answer is no. Smatch, like other static deadlock detection algorithms in CBMC[1] and Infer[2], should be designed to reason thread interaction but not interrupts, which requires new algorithms that I am working on. Besides, may I ask a question that I have sent some patches[3][4] weeks ago, but have not yet got a reply. Would reviewers check the patches later or should I ping them again? [1] http://www.cprover.org/deadlock-detection/ [2] https://github.com/facebook/infer [3] https://lore.kernel.org/lkml/20230726062313.77121-1-dg573847474@xxxxxxxxx/ [4] https://lore.kernel.org/lkml/20230726051727.64088-1-dg573847474@xxxxxxxxx/ Thanks, Chengfeng
