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

rv/monitor: Add the wwnr monitor 

Per task wakeup while not running (wwnr) monitor.

This model is broken, the reason is that a task can be running in the
processor without being set as RUNNABLE. Think about a task about to
sleep:

1:      set_current_state(TASK_UNINTERRUPTIBLE);
2:      schedule();

And then imagine an IRQ happening in between the lines one and two,
waking the task up. BOOM, the wakeup will happen while the task is
running.

Q: Why do we need this model, so?
A: To test the reactors.

Link: https://lkml.kernel.org/r/473c0fc39967250fdebcff8b620311c11dccad30.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 10bde81c

Documentation/trace/rv/index.rst

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

   da_monitor_instrumentation.rst

   monitor_wip.rst

   monitor_wwnr.rst

Documentation/trace/rv/monitor_wwnr.rst

0 → 100644
+45 −0
Original line number Diff line number Diff line 
Monitor wwnr

============



- Name: wwrn - wakeup while not running

- Type: per-task deterministic automaton

- Author: Daniel Bristot de Oliveira <bristot@kernel.org>



Description

-----------



This is a per-task sample monitor, with the following

definition::



               |

               |

               v

    wakeup   +-------------+

  +--------- |             |

  |          | not_running |

  +--------> |             | <+

             +-------------+  |

               |              |

               | switch_in    | switch_out

               v              |

             +-------------+  |

             |   running   | -+

             +-------------+



This model is borken, the reason is that a task can be running

in the processor without being set as RUNNABLE. Think about a

task about to sleep::



  1:      set_current_state(TASK_UNINTERRUPTIBLE);

  2:      schedule();



And then imagine an IRQ happening in between the lines one and two,

waking the task up. BOOM, the wakeup will happen while the task is

running.



- Why do we need this model, so?

- To test the reactors.



Specification

-------------

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

include/trace/events/rv.h

+12 −0
Original line number Diff line number Diff line
@@ -122,6 +122,18 @@ DECLARE_EVENT_CLASS(error_da_monitor_id, 
		__entry->event,

		__entry->state)

);



#ifdef CONFIG_RV_MON_WWNR

/* id is the pid of the task */

DEFINE_EVENT(event_da_monitor_id, event_wwnr,

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

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



DEFINE_EVENT(error_da_monitor_id, error_wwnr,

	     TP_PROTO(int id, char *state, char *event),

	     TP_ARGS(id, state, event));

#endif /* CONFIG_RV_MON_WWNR */



#endif /* CONFIG_DA_MON_EVENTS_ID */

#endif /* _TRACE_RV_H */

kernel/trace/rv/Kconfig

+12 −0
Original line number Diff line number Diff line
@@ -38,6 +38,18 @@ config RV_MON_WIP 
	  For further information, see:

	    Documentation/trace/rv/monitor_wip.rst



config RV_MON_WWNR

	depends on RV

	select DA_MON_EVENTS_ID

	bool "wwnr monitor"

	help

	  Enable wwnr (wakeup while not running) sample monitor, this is a

	  sample monitor that illustrates the usage of per-task monitor.

	  The model is borken on purpose: it serves to test reactors.



	  For further information, see:

	    Documentation/trace/rv/monitor_wwnr.rst



config RV_REACTORS

	bool "Runtime verification reactors"

	default y

kernel/trace/rv/Makefile

+1 −0
Original line number Diff line number Diff line
@@ -3,3 +3,4 @@ 
obj-$(CONFIG_RV) += rv.o

obj-$(CONFIG_RV_REACTORS) += rv_reactors.o

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

obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o