lkml.org 
[lkml]   [2006]   [May]   [29]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    Patch in this message
    /
    Date
    From
    Subject[patch 61/61] lock validator: enable lock validator in Kconfig
    From: Ingo Molnar <mingo@elte.hu>

    offer the following lock validation options:

    CONFIG_PROVE_SPIN_LOCKING
    CONFIG_PROVE_RW_LOCKING
    CONFIG_PROVE_MUTEX_LOCKING
    CONFIG_PROVE_RWSEM_LOCKING

    Signed-off-by: Ingo Molnar <mingo@elte.hu>
    Signed-off-by: Arjan van de Ven <arjan@linux.intel.com>
    ---
    lib/Kconfig.debug | 167 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
    1 file changed, 167 insertions(+)

    Index: linux/lib/Kconfig.debug
    ===================================================================
    --- linux.orig/lib/Kconfig.debug
    +++ linux/lib/Kconfig.debug
    @@ -184,6 +184,173 @@ config DEBUG_SPINLOCK
    best used in conjunction with the NMI watchdog so that spinlock
    deadlocks are also debuggable.

    +config PROVE_SPIN_LOCKING
    + bool "Prove spin-locking correctness"
    + default y
    + help
    + This feature enables the kernel to prove that all spinlock
    + locking that occurs in the kernel runtime is mathematically
    + correct: that under no circumstance could an arbitrary (and
    + not yet triggered) combination of observed spinlock 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 spinlock
    + 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-correctness.txt.
    +
    +config PROVE_RW_LOCKING
    + bool "Prove rw-locking correctness"
    + default y
    + help
    + This feature enables the kernel to prove that all rwlock
    + locking that occurs in the kernel runtime is mathematically
    + correct: that under no circumstance could an arbitrary (and
    + not yet triggered) combination of observed rwlock 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 rwlock
    + 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 spinlocks, 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-correctness.txt.
    +
    +config PROVE_MUTEX_LOCKING
    + bool "Prove mutex-locking correctness"
    + default y
    + help
    + This feature enables the kernel to prove that all mutexlock
    + locking that occurs in the kernel runtime is mathematically
    + correct: that under no circumstance could an arbitrary (and
    + not yet triggered) combination of observed mutexlock 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 mutexlock
    + 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 spinlock, rwlocks
    + 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-correctness.txt.
    +
    +config PROVE_RWSEM_LOCKING
    + bool "Prove rwsem-locking correctness"
    + default y
    + help
    + This feature enables the kernel to prove that all rwsemlock
    + locking that occurs in the kernel runtime is mathematically
    + correct: that under no circumstance could an arbitrary (and
    + not yet triggered) combination of observed rwsemlock 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 rwsemlock
    + 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 spinlocks, rwlocks
    + and mutexes - 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-correctness.txt.
    +
    +config LOCKDEP
    + bool
    + default y
    + depends on PROVE_SPIN_LOCKING || PROVE_RW_LOCKING || PROVE_MUTEX_LOCKING || PROVE_RWSEM_LOCKING
    +
    +config DEBUG_LOCKDEP
    + bool "Lock dependency engine debugging"
    + depends on LOCKDEP
    + default y
    + help
    + If you say Y here, the lock dependency engine will do
    + additional runtime checks to debug itself, at the price
    + of more runtime overhead.
    +
    +config TRACE_IRQFLAGS
    + bool
    + default y
    + depends on PROVE_SPIN_LOCKING || PROVE_RW_LOCKING
    +
    config DEBUG_SPINLOCK_SLEEP
    bool "Sleep-inside-spinlock checking"
    depends on DEBUG_KERNEL
    -
    To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
    the body of a message to majordomo@vger.kernel.org
    More majordomo info at http://vger.kernel.org/majordomo-info.html
    Please read the FAQ at http://www.tux.org/lkml/
    \
     
     \ /
      Last update: 2006-05-29 23:32    [W:4.072 / U:0.364 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site