summaryrefslogtreecommitdiffstats
path: root/Documentation/trace/rv
diff options
context:
space:
mode:
authorDaniel Bristot de Oliveira <bristot@kernel.org>2022-07-29 11:38:53 +0200
committerSteven Rostedt (Google) <rostedt@goodmis.org>2022-07-30 20:01:30 +0200
commitccc319dcb450d57b7befe924453d06804d83ba73 (patch)
tree577ee093d787669d2176cf96d2b9a41f8c33a67b /Documentation/trace/rv
parentrv/monitor: Add the wip monitor (diff)
downloadlinux-ccc319dcb450d57b7befe924453d06804d83ba73.tar.xz
linux-ccc319dcb450d57b7befe924453d06804d83ba73.zip
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: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
Diffstat (limited to 'Documentation/trace/rv')
-rw-r--r--Documentation/trace/rv/index.rst1
-rw-r--r--Documentation/trace/rv/monitor_wwnr.rst45
2 files changed, 46 insertions, 0 deletions
diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst
index 4cb71ed628b8..15fa966102c0 100644
--- a/Documentation/trace/rv/index.rst
+++ b/Documentation/trace/rv/index.rst
@@ -11,3 +11,4 @@ Runtime Verification
da_monitor_synthesis.rst
da_monitor_instrumentation.rst
monitor_wip.rst
+ monitor_wwnr.rst
diff --git a/Documentation/trace/rv/monitor_wwnr.rst b/Documentation/trace/rv/monitor_wwnr.rst
new file mode 100644
index 000000000000..80f1777b85aa
--- /dev/null
+++ b/Documentation/trace/rv/monitor_wwnr.rst
@@ -0,0 +1,45 @@
+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