threading_deadlock Namespace Reference

Classes
class	Lock
class	Thread

Detailed Description

Deadlock-aware operational model for the standard ``threading`` module.

Loaded in place of ``threading.py`` when ESBMC is invoked with
``--deadlock-check``. The Python frontend's ``parser.py`` performs the
swap, mirroring the C preprocessor swap of ``pthread_mutex_lock`` to
``pthread_mutex_lock_check`` in ``src/clang-c-frontend/c_preprocess.cpp``.

The acquire path mirrors ``pthread_mutex_lock_check`` in
``src/c2goto/library/pthread_lib.c``: read the lock field inside an
atomic block, take the lock on the unlocked branch, or bump
``__ESBMC_blocked_threads_count`` and assert the global deadlock
predicate on the locked branch. The ``__ESBMC_assume(unlocked)`` after
the atomic-end kills the locked branch on this thread, but symex's
interleaving search observes the bumped counter on alternative
schedules where every running thread reaches the locked branch — that
is where the predicate fires.

The release path mirrors ``pthread_mutex_unlock_check``: assert the
lock was held before clearing the field, so a release-without-acquire
bug is caught under the same flag whose job it is to find concurrency
errors, then drain the waiters this lock registered. Without that drain
the global counter saturates and a later, unrelated block reads as a
deadlock (#6489).