Monitor wip

• Name: wip - wakeup in preemptive
• Type: per-cpu deterministic automaton
• Author: Daniel Bristot de Oliveira [email protected]

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/[email protected]/

Specification

Grapviz Dot file in tools/verification/models/wip.dot