0001 Monitor wip
0002 ===========
0003
0004 - Name: wip - wakeup in preemptive
0005 - Type: per-cpu deterministic automaton
0006 - Author: Daniel Bristot de Oliveira <bristot@kernel.org>
0007
0008 Description
0009 -----------
0010
0011 The wakeup in preemptive (wip) monitor is a sample per-cpu monitor
0012 that verifies if the wakeup events always take place with
0013 preemption disabled::
0014
0015 |
0016 |
0017 v
0018 #==================#
0019 H preemptive H <+
0020 #==================# |
0021 | |
0022 | preempt_disable | preempt_enable
0023 v |
0024 sched_waking +------------------+ |
0025 +--------------- | | |
0026 | | non_preemptive | |
0027 +--------------> | | -+
0028 +------------------+
0029
0030 The wakeup event always takes place with preemption disabled because
0031 of the scheduler synchronization. However, because the preempt_count
0032 and its trace event are not atomic with regard to interrupts, some
0033 inconsistencies might happen. For example::
0034
0035 preempt_disable() {
0036 __preempt_count_add(1)
0037 -------> smp_apic_timer_interrupt() {
0038 preempt_disable()
0039 do not trace (preempt count >= 1)
0040
0041 wake up a thread
0042
0043 preempt_enable()
0044 do not trace (preempt count >= 1)
0045 }
0046 <------
0047 trace_preempt_disable();
0048 }
0049
0050 This problem was reported and discussed here:
0051 https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/
0052
0053 Specification
0054 -------------
0055 Grapviz Dot file in tools/verification/models/wip.dot
