| 12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455 |
- Monitor wip
- ===========
- - Name: wip - wakeup in preemptive
- - Type: per-cpu deterministic automaton
- - Author: Daniel Bristot de Oliveira <bristot@kernel.org>
- Description
- -----------
- The wakeup in preemptive (wip) monitor is a sample per-cpu monitor
- that verifies if the wakeup events always take place with
- preemption disabled::
- |
- |
- v
- #==================#
- H preemptive H <+
- #==================# |
- | |
- | preempt_disable | preempt_enable
- v |
- sched_waking +------------------+ |
- +--------------- | | |
- | | non_preemptive | |
- +--------------> | | -+
- +------------------+
- The wakeup event always takes place with preemption disabled because
- of the scheduler synchronization. However, because the preempt_count
- and its trace event are not atomic with regard to interrupts, some
- inconsistencies might happen. For example::
- preempt_disable() {
- __preempt_count_add(1)
- -------> smp_apic_timer_interrupt() {
- preempt_disable()
- do not trace (preempt count >= 1)
- wake up a thread
- preempt_enable()
- do not trace (preempt count >= 1)
- }
- <------
- trace_preempt_disable();
- }
- This problem was reported and discussed here:
- https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/
- Specification
- -------------
- Grapviz Dot file in tools/verification/models/wip.dot
|
