56 lines · plain
1Monitor wip2===========3 4- Name: wip - wakeup in preemptive5- Type: per-cpu deterministic automaton6- Author: Daniel Bristot de Oliveira <bristot@kernel.org>7 8Description9-----------10 11The wakeup in preemptive (wip) monitor is a sample per-cpu monitor12that verifies if the wakeup events always take place with13preemption disabled::14 15 |16 |17 v18 #==================#19 H preemptive H <+20 #==================# |21 | |22 | preempt_disable | preempt_enable23 v |24 sched_waking +------------------+ |25 +--------------- | | |26 | | non_preemptive | |27 +--------------> | | -+28 +------------------+29 30The wakeup event always takes place with preemption disabled because31of the scheduler synchronization. However, because the preempt_count32and its trace event are not atomic with regard to interrupts, some33inconsistencies 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 thread42 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 53Specification54-------------55Grapviz Dot file in tools/verification/models/wip.dot56