[SwayamInSync]

With more than one job, functions are verified as tasks on a pool, and each annotates its obligations with source locations through Clang's SourceManager, which caches its last lookups (getLineNumber, getFileID). The tasks took a lock for that annotation, but not every lookup did:

• the notes of a failure whose counterexample passes through a loop (failureNotes) unroll the loop and annotate each bound's module: that call bound to the member annotateObligationSources, declared before the locking wrapper, so it ran unlocked; and its at helper looked up the loop's line unlocked;
• a failure's place and its callee clause (placeFailure, relateClause) fall back to sourceOf when no source was recorded, unlocked.

ThreadSanitizer reported the race in SourceManager::getLineNumber (both sides in sourceOf under annotateObligationSources, one from the failure notes) on calls_in_expressions.cpp, inductive_counterexamples.cpp, pointer_origins.cpp, and range_for.cpp.

Change

The lock is now Verifier::SourceLock, a recursive mutex taken inside sourceOf, annotateObligationSources, and the failure notes' at, so every caller is covered. The local mutex and the wrapper lambda are gone.

Audit

Every member function reachable from the two lambdas that run on the pool (verifyFunction and confirm): 55 functions. The source manager or the ASTContext is used only in those three; confirm makes no lookup. VCR nodes hold source locations, not AST pointers, and no other file of clang/lib/Verify but the (serial) converter reaches the source manager.

Test

suite/parallel_failure_notes.cpp fails sixteen functions at once through loops whose invariants are too weak, so each failure's notes unroll to 9 iterations, and checks every failure's place and notes. Under ThreadSanitizer (-DLLVM_USE_SANITIZER=Thread, this branch): main reported the race in 12 of 12 runs of it (8209 reports), the fix in 0 of 12. In a release build the race rarely changes the output, so the lit test itself passes on main; the TSan sweep of the nightly job (separate PR) is what fails there. It takes 3 s in a release build.

Release notes: "Source lookups from parallel failures"; ARCHITECTURE.md says which lookups take the lock.

Not covered: verification during a compilation

clang++ -fverify-contracts runs the whole verifier on a std::async thread while the main thread runs CodeGen's HandleTranslationUnit on the same ASTContext and SourceManager (BackendConsumer::HandleTranslationUnit), so this lock cannot order those. A TSan clang compiling a file with contracts and deferred template code (-g -c) reported races in 4 of 4 runs, with this fix: CodeGen's debug locations against Verifier::sourceOf in getLineNumber; linkage caching (setLinkageForGV against ASTConverter::functionIdentity); and ASTContext::getTypeInfo's map, which CodeGen inserts into while VType::fromQualType looks up. That needs verification ordered against CodeGen and is left for its own change.