1Monitor wip 2=========== 3 4- Name: wip - wakeup in preemptive 5- Type: per-cpu deterministic automaton 6- Author: Daniel Bristot de Oliveira <bristot@kernel.org> 7 8Description 9----------- 10 11The wakeup in preemptive (wip) monitor is a sample per-cpu monitor 12that verifies if the wakeup events always take place with 13preemption disabled:: 14 15 | 16 | 17 v 18 #==================# 19 H preemptive H <+ 20 #==================# | 21 | | 22 | preempt_disable | preempt_enable 23 v | 24 sched_waking +------------------+ | 25 +--------------- | | | 26 | | non_preemptive | | 27 +--------------> | | -+ 28 +------------------+ 29 30The wakeup event always takes place with preemption disabled because 31of the scheduler synchronization. However, because the preempt_count 32and its trace event are not atomic with regard to interrupts, some 33inconsistencies might happen. For example:: 34 35 preempt_disable() { 36 __preempt_count_add(1) 37 -------> smp_apic_timer_interrupt() { 38 preempt_disable() 39 do not trace (preempt count >= 1) 40 41 wake up a thread 42 43 preempt_enable() 44 do not trace (preempt count >= 1) 45 } 46 <------ 47 trace_preempt_disable(); 48 } 49 50This problem was reported and discussed here: 51 https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/ 52 53Specification 54------------- 55Grapviz Dot file in tools/verification/models/wip.dot 56