| 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 |
