How to tell compilers to not drop the lock stack when using Assume/Assert? #21596

1. 
   MarcoFalke commented at 4:28 pm on April 4, 2021: member

   It would be nice if there was a way to tell compilers not to drop the lock stack and thus issue warnings when accessing a symbol that needs a lock inside Assume/Assert.

   Hit by (at least): @ajtowns , @jnewbery , me.

2. MarcoFalke added the label Feature on Apr 4, 2021
3. MarcoFalke added the label Brainstorming on Apr 4, 2021
4. 
   MarcoFalke commented at 4:29 pm on April 4, 2021: member

   From IRC:

   0[21:42] <aj> could probably have an AssertWithLock(L, E) that adds the annotation for L i suppose, but...
   

5. 
   ajtowns commented at 6:41 am on April 5, 2021: member

   I think this would be solved if (implicit) lambda capture of variable foo which is annotated as foo GUARDED_BY(bar) implied that the lambda was annotated with EXCLUSIVE_LOCKS_REQUIRED(bar).

   If we got a new compiler version that supported the above to the point where we could use it in our test suite, we could probably then mark Assert/Assume as NO_THREAD_SAFETY_ANALYSIS on older versions of clang.

6. 
   ryanofsky commented at 12:28 pm on April 5, 2021: member

   A convention I use when writing lambdas is to use [&] implicit capture when I believe the lambda will be called synchronously in the current scope, and use [] or explicit captures [&var1, var2, var3] when then lambda will be called asynchronously later.

   I think this is a good convention, and if it is followed, analysis could treat the lambda like a nested scope when the capture list starts with unnamed [&].

   But probably the compiler shouldn’t assume this convention is used, and it would make more sense for it to provide an explicit annotation for lambdas that would tell the analysis whether the lambda is called synchronously or asynchronously. Maybe it could the allow the existing SCOPED_CAPABILITY attribute to be applied to lambdas to indicate this, or just add a new attribute.

   re: #21596 (comment), I don’t think it would be legitimate for analysis to assume whether locks needed to access a variable are acquired based on whether the variable is captured. This assumption would make analysis skip useful checking in asynchronous lambdas where a variable is captured but a lock still needs to be acquired before the variable is used. You don’t need locks to access the address of a guarded variable if you aren’t accessing the variable itself, and conversely having the address doesn’t imply whether you have the locks.

7. 
   MarcoFalke commented at 10:20 am on November 2, 2021: member

   I think this is a good convention

   I don’t think we should need to change code for that. Assume is inline (the lambda is defined and then called with () in the same line). At least this case should be trivial for a compiler to figure out that it is a synchronous call.

8. MarcoFalke added the label Upstream on Nov 2, 2021
9. MarcoFalke referenced this in commit 87dc1dc55f on Mar 31, 2022
10. MarcoFalke closed this on Mar 31, 2022

    ---

11. sidhujag referenced this in commit 2cd931a679 on Apr 3, 2022
12. DrahtBot locked this on Mar 31, 2023

Contributors
MarcoFalke ajtowns ryanofsky

Labels
Feature Brainstorming Upstream