[SwayamInSync]

Plan item T3, the ThreadSanitizer half. Builds on #133 (ci/sanitizers, the sanitizer option, script, and workflow) and on #136 (the race this sweep found), both merged; main is merged into this branch.

Why TSan failed

#133 dropped its TSan job because TSan's runtime crashed or hung in 66 of 69 runs of suite/spec_automation.cpp with four jobs. The cause is neither the partial instrumentation nor the counterexample checker's thread per check: TSan keeps each thread's calls on a shadow stack of 64 Ki frames (kShadowStackSize) that only a debug runtime bounds, and the checker nests up to CertifyLimits::Frames (50000) evaluations of several frames each, so it writes past it into the runtime's own memory.

spec_automation.cpp, --jobs=4, fresh proof cache	runs	failed
only the verifier instrumented, as #133	50	44 (11 hung, SEGV or TSan CHECK otherwise)
LLVM, Clang, verifier, and Z3 instrumented	50	45 (14 hung)
a __tsan_func_entry wrapper that stops at the limit	12	12 stopped at 65472 nested calls, all in Backend/Certify.cpp
Certify.cpp without entry/exit hooks, either instrumentation	60 + 60	0
the nightly's build (below) under gdb, idle and under load	100	0

A standalone program recursing 65,600 calls deep beside threads that start and stop failed in 3 of 6 runs, at 65,000 in 0 of 6.

Change

• Backend/Certify.cpp is compiled with -fno-sanitize-thread-func-entry-exit under TSan (LLVM_USE_SANITIZER=Thread or CPPVERIFY_SANITIZER with thread): its accesses are still checked, its frames are missing from reported stacks.
• tools/cpp-verify/ShadowStackGuard.cpp, linked into TSan builds only (uninstrumented, --wrap=__tsan_func_entry,--wrap=__tsan_func_exit), stops a run that reaches the limit with cpp-verify: ThreadSanitizer shadow stack full: N nested calls and its stack. With the hooks put back in Certify.cpp, 6 of 6 runs stopped so.
• CppVerifyZ3.cmake builds the vendored Z3 with -fsanitize=thread under LLVM_USE_SANITIZER=Thread, so TSan sees Z3's synchronization and accesses.
• cppverify-sanitize.sh BUILD address|thread [PARALLEL]: thread mode runs each program with --jobs=4, a proof cache of its own, and --backend=race where its RUN lines use it. Both modes skip programs lit never runs (UNSUPPORTED: true: llvm_uleb128_decoder_exhaustive.cpp, which needed 17.6 GB under TSan) and report a program without a result within 900 s, since a hung runtime prints nothing.
• cppverify-tsan.supp: three races and a lock order inside Z3 4.13.4 (global verbose stream, statistics read of the allocation counters, the timeout handler's flag, the timer pool), and LLVM's crash-time backtrace (crash_report_url.cpp crashes on purpose). Each with its reason.
• cppverify-sanitizers.yml: a ThreadSanitizer job, clang-18 against GCC 13's libstdc++ (below), everything instrumented, two programs at once.

The C++ library on CI's runner

The first CI run failed in Z3's build: scoped_timer.cpp:64, m_mutex.try_lock_until(end) with a steady_clock time, error: no member named '_M_clocklock' in 'std::timed_mutex' in /usr/include/c++/14/mutex:205. Clang 18 on ubuntu-24.04 compiles against the libstdc++ of the image's newest GCC, 14.2, and that is GCC PR 121496: GCC 14 defines _GLIBCXX_USE_PTHREAD_MUTEX_CLOCKLOCK as (_GLIBCXX_TSAN==0), so 0 under TSan, and <mutex> tests it with #if where timed_mutex::_M_clocklock is declared (line 300) but with #ifdef where the steady-clock _M_try_lock_until that calls it is defined (line 191). The #ifdefs are in 14.3.0 and 15.2.0 and gone in 14.4.0 and 15.3.0. GCC 13 defines the macro as 1, and its wait calls pthread_mutex_clocklock, which clang-18's TSan runtime intercepts (nm libclang_rt.tsan-x86_64.a). This machine has only GCC 13, so local builds never hit it; with Ubuntu's libstdc++-14-dev 14.2.0-4ubuntu2~24.04.1 selected through --gcc-install-dir, the same error appears, and nothing else in LLVM, Clang, or the verifier uses a timed mutex.

• The job passes --gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13 as CMAKE_C_FLAGS and CMAKE_CXX_FLAGS.
• CppVerifyZ3.cmake gives Z3's ExternalProject the cache's CMAKE_C_FLAGS, CMAKE_CXX_FLAGS, and CMAKE_EXE_LINKER_FLAGS (as configured, without LLVM's additions), then TSan's. Z3 got only the compilers before, so a flag that selects the C++ library reached LLVM and the verifier but not Z3. With no flags configured nothing more is passed, as before.
• Under TSan, configure checks that the library compiles that wait (CPPVERIFY_TSAN_TIMED_MUTEX_WAIT) and otherwise stops with the cause and the flags to use; a failed check is not cached, so it is rerun after the flags change.

Z3 module under TSan, configured with	configure	Z3's scoped_timer.cpp
before this change, GCC 14.2's directory	ok, the flag not passed to Z3	compiled against GCC 13's headers
this change without the check, GCC 14.2	ok	no member named '_M_clocklock'
this change, GCC 14.2	stops: GCC PR 121496 and the flags to use	not reached
this change, GCC 13	ok	compiled

A full configure of LLVM with TSan and GCC 14.2's headers stops at the check as well.

Instrumenting only the verifier is still accepted but not used: it reported a race on LLVM's RemoveFileOnSignal list that the full build, seeing LLVM's atomics, does not, and it cannot see a race on Z3 objects.

Results

The nightly's configuration (vendored Z3 through the ExternalProject) on all 465 programs with this branch plus #136: thread: no reports in 465 programs, 4800 CPU seconds (20 minutes on four cores here), at most 3.3 GB a program. Without #136 the sweep reports the source manager race in getLineNumber (calls_in_expressions.cpp, inductive_counterexamples.cpp, pointer_origins.cpp, range_for.cpp, and #136's test), so this PR's own TSan job fails until #136 is merged in.

After merging #133's fresh stacks for the certifier (ci/sanitizers at eb7b64d) and running at the default 8 MiB stack limit, as the script now does: 30 of 30 runs of spec_automation.cpp finished with no runtime failure; the sweep (4300 CPU seconds) reported only that source manager race, in 6 programs; and with the hooks put back in Certify.cpp, 6 of 6 runs still stopped at the guard, since half of a 256 MiB stack holds more than 65536 frames.

After merging main (#136, #138, #139, #133) and with the job's flags (--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13), the job's build and script with eight programs at once: thread: no reports in 468 programs, 3900 CPU seconds, at most 3.5 GB a program.

Two of 20 runs of the partly instrumented build with the manual wrapper stalled once, under heavy machine load, after storing every proof; 80 more runs of that binary under gdb did not reproduce it, and the fully instrumented builds never stalled (220 runs). The no-result check would report such a stall in CI.

Docs

ARCHITECTURE ("Regression and Coverage"), the tooling reference (the build, the script, the guard's exact output), and the release notes ("Testing").