Right, but that’s a global property of everything that uses the lock, so if you’re writing a library you'd have to run the analysis against real or synthetic call graphs. Plus it’s very easy to accidentally break that property if you’re not using it in an analysis-friendly way, no? Instead, role-separated data structures like eg channels, run-once-functions and atomic value swaps can - due to their constraints - make them harder to use in ways that break analysis, and can be analyzed locally.

Say eg my library is acting as a producer. Ideally I can check that I am producing 0-N items and that it closes the channel. Analyzing the consumer can be deferred and decoupled, which is good because it may not exist yet.