[PATCH] D102026: Thread safety analysis: Allow exlusive/shared joins for managed and asserted capabilities

[Aaron Puchert via Phabricator via cfe-commits]

aaronpuchert added a comment.

In D102026#2785243 <https://reviews.llvm.org/D102026#2785243>, @delesley wrote:

> Assert_capability is not a back door.  It is supposed to be used only on a function which does a run-time check:  if (!mu_.is_locked()) fail().

Right, although assertions can turn into no-ops depending on the build profile. We discussed this on D87629 <https://reviews.llvm.org/D87629>.

That's why it's more like stating an assumption. We don't really know if/how that assumption is being enforced.

> There are places in the code where you cannot statically prove that a property holds at compile-time, so you insert a run-time check into the code, and then propagate that property to the static analysis on the branch where the check succeeds.

That's exactly what I meant with “back door”: if you can't prove that a capability is held, you can still assert it. That shifts the burden of checking to the runtime, so in that sense it is a backdoor for static analysis.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D102026