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

[Russell Yanofsky via Phabricator via cfe-commits]

ryanofsky marked 4 inline comments as done.
ryanofsky added a comment.

Agree with everything in D87629#2278073 <https://reviews.llvm.org/D87629#2278073>. "Assumed" is the key word, and a wrong assumption doesn't imply UB or generating incorrect code <https://github.com/bitcoin/bitcoin/pull/19929#issuecomment-693722339>. Also comment is good summary of the compile-time and run-time checking tradeoffs.



================
Comment at: clang/docs/ThreadSafetyAnalysis.rst:450
 
-These are attributes on a function or method that does a run-time test to see
-whether the calling thread holds the given capability.  The function is assumed
-to fail (no return) if the capability is not held.  See :ref:`mutexheader`,
-below, for example uses.
+These are attributes on a function or method which asserts the calling thread
+already holds the given capability, for example by performing a run-time test
----------------
aaronpuchert wrote:
> The assertion is just a promise though, so it could only happen in debug builds, for example.
> The assertion is just a promise though, so it could only happen in debug builds, for example.

This is true, but the statements seem compatible to me. I'd be happy to update it if I know what change to make.



================
Comment at: clang/docs/ThreadSafetyAnalysis.rst:452
+already holds the given capability, for example by performing a run-time test
+and terminating or throwing if the capability is not held.  Presence of this
+annotation causes the analysis to assume the capability is held at the point of
----------------
vasild wrote:
> aaronpuchert wrote:
> > That's an interesting point. We currently do assume that the capability is held even when an exception is thrown, although that's primarily because Clang's source-level CFG doesn't really model exception handling that well:
> > 
> > ```
> > Mutex mu;
> > bool a GUARDED_BY(mu);
> > 
> > void except() {
> >   try {
> >     mu.AssertHeld();
> >   } catch (...) {
> >     a = 0; // No warning.
> >   }
> > }
> > ```
> > 
> > We can't warn there because `AssertHeld` might terminate in case the mutex isn't held.
> > 
> > Not sure if we need to clarify this here: we just assume that the capability is held on a regular return. The other case is basically UB for us.
> Maybe don't mention "throwing", given the example above and `s/at the call/after the call/`.
> It is similar to:
> 
> ```
> void f(char x, unsigned char y)
> {
>     assert(x >= 0);
>     assert(y <= 127);
>     if (x > y) { // it is ok to omit a warning about comparing signed and unsigned because AFTER the asserts we know we are good.
>         ...
>     }
> }
> ```
> That's an interesting point.

Removed language about throwing now. That was just my misunderstanding.


================
Comment at: clang/docs/ThreadSafetyAnalysis.rst:452-454
+and terminating or throwing if the capability is not held.  Presence of this
+annotation causes the analysis to assume the capability is held at the point of
+the call. See :ref:`mutexheader`, below, for example uses.
----------------
ryanofsky wrote:
> vasild wrote:
> > aaronpuchert wrote:
> > > That's an interesting point. We currently do assume that the capability is held even when an exception is thrown, although that's primarily because Clang's source-level CFG doesn't really model exception handling that well:
> > > 
> > > ```
> > > Mutex mu;
> > > bool a GUARDED_BY(mu);
> > > 
> > > void except() {
> > >   try {
> > >     mu.AssertHeld();
> > >   } catch (...) {
> > >     a = 0; // No warning.
> > >   }
> > > }
> > > ```
> > > 
> > > We can't warn there because `AssertHeld` might terminate in case the mutex isn't held.
> > > 
> > > Not sure if we need to clarify this here: we just assume that the capability is held on a regular return. The other case is basically UB for us.
> > Maybe don't mention "throwing", given the example above and `s/at the call/after the call/`.
> > It is similar to:
> > 
> > ```
> > void f(char x, unsigned char y)
> > {
> >     assert(x >= 0);
> >     assert(y <= 127);
> >     if (x > y) { // it is ok to omit a warning about comparing signed and unsigned because AFTER the asserts we know we are good.
> >         ...
> >     }
> > }
> > ```
> > That's an interesting point.
> 
> Removed language about throwing now. That was just my misunderstanding.
> Maybe don't mention "throwing", given the example above and `s/at the call/after the call/`.

Thanks, update has both changes


================
Comment at: clang/docs/ThreadSafetyAnalysis.rst:453
+and terminating or throwing if the capability is not held.  Presence of this
+annotation causes the analysis to assume the capability is held at the point of
+the call. See :ref:`mutexheader`, below, for example uses.
----------------
aaronpuchert wrote:
> It's implemented a bit differently:
> 
> ```
> Mutex mu;
> bool a GUARDED_BY(mu);
> 
> void f() {
>   a = 0; // warning.
>   mu.AssertHeld();
>   a = 0; // Ok.
> }
> ```
> 
> If we were to assume that `mu` is held at the call site, it would also be held right before it.
> 
> I'm not sure if this is the right behavior, but assuming that it is, calling an `ASSERT_CAPABILITY` function introduces an assumption which can be used from that point on, and which disappears on join points with branches that don't have the assumption.
> It's implemented a bit differently:

Tweaked to say that assumption applies after the call.



================
Comment at: clang/docs/ThreadSafetyAnalysis.rst:456-457
+
+The given capability must be held on entry to the function, or the function is
+assumed to fail (no return).
 
----------------
aaronpuchert wrote:
> "The function is assumed to return only if the given capability is held."?
> "The function is assumed to return only if the given capability is held."?

Updated to drop this extra paragraph. I don't think any information is lost and it seems better to avoid implying that annotating a function which does return (NDEBUG assert) will causes the analysis to assume something not true.



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D87629