Commit 10bde81c authored by Daniel Bristot de Oliveira's avatar Daniel Bristot de Oliveira Committed by Steven Rostedt (Google)
Browse files

rv/monitor: Add the wip monitor 

The wakeup in preemptive (wip) monitor 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.

The documentation illustrates one of these cases.

Link: https://lkml.kernel.org/r/c98ca678df81115fddc04921b3c79720c836b18f.1659052063.git.bristot@kernel.org



Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
Cc: Guenter Roeck <linux@roeck-us.net>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Will Deacon <will@kernel.org>
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Marco Elver <elver@google.com>
Cc: Dmitry Vyukov <dvyukov@google.com>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Shuah Khan <skhan@linuxfoundation.org>
Cc: Gabriele Paoloni <gpaoloni@redhat.com>
Cc: Juri Lelli <juri.lelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: Tao Zhou <tao.zhou@linux.dev>
Cc: Randy Dunlap <rdunlap@infradead.org>
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Cc: linux-trace-devel@vger.kernel.org
Signed-off-by: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
parent 8812d212

Documentation/trace/rv/index.rst

+1 −0
Original line number Diff line number Diff line
@@ -10,3 +10,4 @@ Runtime Verification 
   deterministic_automata.rst

   da_monitor_synthesis.rst

   da_monitor_instrumentation.rst

   monitor_wip.rst

Documentation/trace/rv/monitor_wip.rst

0 → 100644
+55 −0
Original line number Diff line number Diff line 
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

include/trace/events/rv.h

+10 −0
Original line number Diff line number Diff line
@@ -56,6 +56,16 @@ DECLARE_EVENT_CLASS(error_da_monitor, 
		__entry->event,

		__entry->state)

);



#ifdef CONFIG_RV_MON_WIP

DEFINE_EVENT(event_da_monitor, event_wip,

	    TP_PROTO(char *state, char *event, char *next_state, bool final_state),

	    TP_ARGS(state, event, next_state, final_state));



DEFINE_EVENT(error_da_monitor, error_wip,

	     TP_PROTO(char *state, char *event),

	     TP_ARGS(state, event));

#endif /* CONFIG_RV_MON_WIP */

#endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */



#ifdef CONFIG_DA_MON_EVENTS_ID

kernel/trace/rv/Kconfig

+13 −0
Original line number Diff line number Diff line
@@ -25,6 +25,19 @@ menuconfig RV 
	  For further information, see:

	    Documentation/trace/rv/runtime-verification.rst



config RV_MON_WIP

	depends on RV

	depends on PREEMPT_TRACER

	select DA_MON_EVENTS_IMPLICIT

	bool "wip monitor"

	help

	  Enable wip (wakeup in preemptive) sample monitor that illustrates

	  the usage of per-cpu monitors, and one limitation of the

	  preempt_disable/enable events.



	  For further information, see:

	    Documentation/trace/rv/monitor_wip.rst



config RV_REACTORS

	bool "Runtime verification reactors"

	default y

kernel/trace/rv/Makefile

+1 −0
Original line number Diff line number Diff line
@@ -2,3 +2,4 @@ 


obj-$(CONFIG_RV) += rv.o

obj-$(CONFIG_RV_REACTORS) += rv_reactors.o

obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o