I've look at the literature every couple of years, and to the best of my knowledge, there is no paper proving that a subset of the Linux kernel RCU apis are sou

I've look at the literature every couple of years, and to the best of my knowledge, there is no paper proving that a subset of the Linux kernel RCU apis are sound. If you are aware of one, I am intrinsically interested in this topic.