CONFIG_PROVE_LOCKING: Lock debugging: prove locking correctness

General informations

The Linux kernel configuration item CONFIG_PROVE_LOCKING:

• prompt: Lock debugging: prove locking correctness
• type: bool
• depends on: CONFIG_DEBUG_KERNEL && CONFIG_LOCK_DEBUGGING_SUPPORT
• defined in lib/Kconfig.debug
• found in Linux kernels: 2.6.18–2.6.39, 3.0–3.19, 4.0–4.20, 5.0–5.19, 6.0–6.8, 6.9-rc+HEAD

Help text

This feature enables the kernel to prove that all locking that occurs in the kernel runtime is mathematically correct: that under no circumstance could an arbitrary (and not yet triggered) combination of observed locking sequences (on an arbitrary number of CPUs, running an arbitrary number of tasks and interrupt contexts) cause a deadlock.

In short, this feature enables the kernel to report locking related deadlocks before they actually occur.

The proof does not depend on how hard and complex a deadlock scenario would be to trigger: how many participant CPUs, tasks and irq-contexts would be needed for it to trigger. The proof also does not depend on timing: if a race and a resulting deadlock is possible theoretically (no matter how unlikely the race scenario is), it will be proven so and will immediately be reported by the kernel (once the event is observed that makes the deadlock theoretically possible).

If a deadlock is impossible (i.e. the locking rules, as observed by the kernel, are mathematically correct), the kernel reports nothing.

NOTE: this feature can also be enabled for rwlocks, mutexes and rwsems - in which case all dependencies between these different locking variants are observed and mapped too, and the proof of observed correctness is also maintained for an arbitrary combination of these separate locking variants.

For more details, see Documentation/locking/lockdep-design.rst.

Hardware

LKDDb

Raw data from LKDDb:

• (none)

Sources

This page is automaticly generated with free (libre, open) software lkddb(see lkddb-sources).

The data is retrived from:

• Linux kernel
• Linux Kernel Driver DataBase (LKDDb)

Automatic links from Google (and ads)

Custom Search

Popular queries: