Public Member Functions
None	__init__ (self)
None	acquire (self)
None	release (self)

Protected Attributes
int	_locked = 0
int	_waiters = 0

Detailed Description

Non-recursive mutex; mirrors ``threading.Lock`` with deadlock detection.

Constructor & Destructor Documentation

◆ init()

None threading_deadlock.Lock.__init__ ( self )

Member Function Documentation

◆ acquire()

None threading_deadlock.Lock.acquire ( self )

Block until the lock is free, then mark it held.

On the blocked branch, register the thread as blocked and assert
that not every running thread is now blocked. Symex's
interleaving search lifts the bumped counter into schedules
where the deadlock predicate becomes true and the assertion
fires; on this thread's own path, ``__ESBMC_assume(unlocked)``
kills the blocked branch after the predicate has been checked.

◆ release()

None threading_deadlock.Lock.release ( self )

Mark the lock free; assert it was held.

The assert is consumed by ESBMC's parser.py via ast.parse() and
lowered to a verification claim, so `python -O` byte-code
stripping never applies — the nosec marker silences Bandit's
generic B101 finding, which does not model that pipeline.

Member Data Documentation

◆ _locked

int threading_deadlock.Lock._locked = 0

protected

◆ _waiters

threading_deadlock.Lock._waiters = 0