On Mon, Nov 11, 2019 at 8:51 AM Linus Torvalds <torvalds@xxxxxxxxxxxxxxxxxxxx> wrote: > > On Mon, Nov 11, 2019 at 7:51 AM Alan Stern <stern@xxxxxxxxxxxxxxxxxxx> wrote: > > > > I dislike the explicit annotation approach, because it shifts the > > burden of proving correctness from the automatic verifier to the > > programmer. > > Yes. > > However, sometimes explicit annotations are very useful as > documentation and as showing of intent even if they might not change > behavior or code generation. > > But they generally should never _replace_ checking - in fact, the > annotations themselves should hopefully be checked for correctness > too. > > So a good annotation would implicitly document intent, but it should > also be something that we can check being true, so that we also have > the check that reality actually _matches_ the intent too. Because > misleading and wrong documentation is worse than no documentation at > all. > > Side note: an example of a dangerous annotation is the one that Eric > pointed out, where a 64-bit read in percpu_counter_read_positive() > could be changed to READ_ONCE(), and we would compile it cleanly, but > on 32-bit it wouldn't actually be atomic. > > We at one time tried to actually verify that READ/WRITE_ONCE() was > done only on types that could actually be accessed atomically (always > ignoring alpha because the pain is not worth it), but it showed too > many problems. > > So now we silently accept things that aren't actually atomic. We do > access them "once" in the sense that we don't allow the compiler to > reload it, but it's not "once" in the LKMM sense of one single value. > > That's ok for some cases. But it's actually a horrid horrid thing from > a documentation standpoint, and I hate it, and it's dangerous. > > Linus I was hoping to cleanup the 'easy cases' before looking at more serious issues. But it looks like even the ' easy cases' are not that easy. Now I wonder what to do with the ~400 KCSAN reports sitting in pre-moderation queue.
