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
