3 ms·
What makes you think this kind of proof work hasn’t already been done for this core C code in the kernel?
by nicoburns 5y ago
What makes you think this kind of proof work hasn’t already been done for this core C code in the kernel?
- volta83 5y agoI'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.