[PATCH] D87629: Thread safety analysis: Improve documentation for ASSERT_CAPABILITY

[Aaron Puchert via Phabricator via cfe-commits]

aaronpuchert added a comment.

You can view it this way: there is a dynamic set and a static set of capabilities. The static set is always the same at any particular point in a function, regardless of the circumstances we're called from. It's what we determine in the analysis. The dynamic set depends on who called us and could be greater. To illustrate the difference:

  void f() {
    // mu is dynamically held when called from g and not held when called from h.
    // It is not held statically.
  }
  void g() REQUIRES(mu) {
    // Here mu is statically and dynamically held.
    f();
  }
  void h() REQUIRES(!mu) {
    // Here mu is statically and dynamically not held.
    f();
  }

Basically `ASSERT_CAPABILITY` is an alternative to propagating `REQUIRES` through the stack. Sometimes that's not feasible for various reasons, so we can't verify at compile-time that a lock is held. Asserting converts a dynamically held capability into a statically held capability. So locks that the programmer is sure should be held can be assumed by the analysis.

In the discussion on the bitcoin repo I got the impression that you want both runtime checks and compile-time checks in parallel, instead of having either of them. Then maybe you shouldn't use `ASSERT_CAPABILITY`. But `EXCLUSIVE_LOCKS_REQUIRED` on the assertion is also strange. If you want the assertion to exist in parallel to the Analysis and not influence it, don't annotate it at all.

We're aware that there are loop holes, especially because the Analysis doesn't integrate into the type system. A deliberate decision, because that would affect things like overloading and other language core features. As a consequence, you can override a function with another function that has additional `REQUIRES` attributes (something we could warn about), or cast away `REQUIRES` from a function type before calling it. (Which we can't warn about, because the attributes aren't allowed on types. They are always attached to a variable or function declaration.)


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D87629/new/

https://reviews.llvm.org/D87629