All of lore.kernel.org
 help / color / mirror / Atom feed
From: Daniel Bristot de Oliveira <bristot@kernel.org>
To: Steven Rostedt <rostedt@goodmis.org>, linux-kernel@vger.kernel.org
Cc: Daniel Bristot de Oliveira <bristot@kernel.org>,
	Jonathan Corbet <corbet@lwn.net>, Ingo Molnar <mingo@redhat.com>,
	Thomas Gleixner <tglx@linutronix.de>,
	Peter Zijlstra <peterz@infradead.org>,
	Will Deacon <will@kernel.org>,
	Catalin Marinas <catalin.marinas@arm.com>,
	Marco Elver <elver@google.com>,
	Dmitry Vyukov <dvyukov@google.com>,
	"Paul E. McKenney" <paulmck@kernel.org>,
	Shuah Khan <skhan@linuxfoundation.org>,
	Gabriele Paoloni <gpaoloni@redhat.com>,
	Juri Lelli <juri.lelli@redhat.com>,
	Clark Williams <williams@redhat.com>,
	linux-doc@vger.kernel.org, linux-trace-devel@vger.kernel.org
Subject: [RFC V3 16/20] Documentation/rv: Add deterministic automata instrumentation documentation
Date: Thu,  5 May 2022 18:06:56 +0200	[thread overview]
Message-ID: <9d97a7fd241c08ebbf86d32190d6ae376668495f.1651766361.git.bristot@kernel.org> (raw)
In-Reply-To: <cover.1651766361.git.bristot@kernel.org>

Add the da_monitor_instrumentation.rst. It describes the basics
of RV monitor instrumentation.

Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Steven Rostedt <rostedt@goodmis.org>
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: 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>
---
 .../trace/rv/da_monitor_instrumentation.rst   | 223 ++++++++++++++++++
 1 file changed, 223 insertions(+)
 create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst

diff --git a/Documentation/trace/rv/da_monitor_instrumentation.rst b/Documentation/trace/rv/da_monitor_instrumentation.rst
new file mode 100644
index 000000000000..bbc14cae7d6b
--- /dev/null
+++ b/Documentation/trace/rv/da_monitor_instrumentation.rst
@@ -0,0 +1,223 @@
+Deterministic Automata Instrumentation
+========================================
+
+This document introduces some concepts behind the **Deterministic Automata
+(DA)** monitor instrumentation.
+
+The synthesis of automata-based models into the Linux *RV monitor* abstraction
+is automated by a tool named dot2k, and the "rv/da_monitor.h" provided
+by the RV interface.
+
+For example, given a file "wip.dot", representing a per-cpu monitor, with
+this content::
+
+  digraph state_automaton {
+	center = true;
+	size = "7,11";
+	rankdir = LR;
+	{node [shape = circle] "non_preemptive"};
+	{node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
+	{node [shape = doublecircle] "preemptive"};
+	{node [shape = circle] "preemptive"};
+	"__init_preemptive" -> "preemptive";
+	"non_preemptive" [label = "non_preemptive"];
+	"non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
+	"non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
+	"preemptive" [label = "preemptive"];
+	"preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
+	{ rank = min ;
+		"__init_preemptive";
+		"preemptive";
+	}
+  }
+
+That is the "DOT" representation of this automata model::
+
+                       preempt_enable
+          +---------------------------------+
+          v                                 |
+        #============#  preempt_disable   +------------------+
+    --> H preemptive H -----------------> |  non_preemptive  |
+        #============#                    +------------------+
+                                            ^ sched_waking |
+                                            +--------------+
+
+
+Run the dot2k tool with the model, specifying that it is a "per-cpu"
+model::
+
+  $ dot2k -d ~/wip.dot -t per_cpu
+
+This will create a directory named "wip/" with the following files:
+
+- model.h: the wip in C
+- wip.h: tracepoints that report the execution of the events by the
+  monitor
+- wip.c: the RV monitor
+
+The monitor instrumentation should be done entirely in the RV monitor,
+in the example above, in the wip.c file.
+
+The RV monitor instrumentation section
+--------------------------------------
+
+The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
+will include a section dedicated to instrumentation.
+
+In the example of the wip.dot above, it will look like::
+
+  /*
+   * This is the instrumentation part of the monitor.
+   *
+   * This is the section where manual work is required. Here the kernel events
+   * are translated into model's event.
+   *
+   */
+  static void handle_preempt_disable(void *data, /* XXX: fill header */)
+  {
+	da_handle_event_wip(preempt_disable);
+  }
+
+  static void handle_preempt_enable(void *data, /* XXX: fill header */)
+  {
+	da_handle_event_wip(preempt_enable);
+  }
+
+  static void handle_sched_waking(void *data, /* XXX: fill header */)
+  {
+	da_handle_event_wip(sched_waking);
+  }
+
+  static int start_wip(void)
+  {
+	int retval;
+
+	retval = da_monitor_init_wip();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
+	rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
+
+	return 0;
+  }
+
+The comment at the top of the section explains the general idea: the
+instrumentation section translates *kernel events* into the *events
+accepted by the model*.
+
+Tracing callback functions
+-----------------------------
+
+The first three functions are skeletons for callback *handler functions* for
+each of the three events from the wip model. The developer does not
+necessarily need to use them: they are just starting points.
+
+Using the example of::
+
+ void handle_preempt_disable(void *data, /* XXX: fill header */)
+ {
+        da_handle_event_wip(preempt_disable);
+ }
+
+The "preempt_disable" event from the model conects directly to the
+"preemptirq:preempt_disable". The "preemptirq:preempt_disable" event
+has the following signature, from "include/trace/events/preemptirq.h"::
+
+  TP_PROTO(unsigned long ip, unsigned long parent_ip)
+
+Hence, the "handle_preempt_disable()" function will look like::
+
+  void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
+
+In this case, the kernel even translates one to one with the automata event,
+and indeed, no other change is needed for this function.
+
+The next handler function, "handle_preempt_enable()" has the same argument
+list from the "handle_preempt_disable()". The difference is that the
+"preempt_enable" event will be used to synchronize the system to the model.
+
+Initially, the *model* is placed in the initial state. However, the *system*
+might, or might not be in the initial state. The monitor cannot start
+processing events until it knows that the system reached the initial state.
+Otherwise the monitor and the system could be out-of-sync.
+
+Looking at the automata definition, it is possible to see that the system
+and the model are expected to return to the initial state after the
+"preempt_enable" execution. Hence, it can be used to synchronize the
+system and the model at the initialization of the monitoring section.
+
+The initialization is informed via an special handle function, the
+"da_handle_init_event_$(MONITOR)(event)", in this case::
+
+  da_handle_event_wip(preempt_disable);
+
+So, the callback function will look like::
+
+  void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
+  {
+        da_handle_init_event_wip(preempt_enable);
+  }
+
+Finally, the "handle_sched_waking()" will look like::
+
+  void handle_sched_waking(void *data, struct task_struct *task)
+  {
+        da_handle_event_wip(sched_waking);
+  }
+
+And the explanation is left for the reader as an exercise.
+
+Start and Stop functions
+------------------------
+
+dot2k automatically creates two special functions::
+
+  start_$MODELNAME()
+  stop_$MODELNAME()
+
+These functions are called when the monitor is enabled and disabled,
+respectivelly.
+
+They should be used to *attach* and *detach* the instrumentation to the running
+system. The developer must add to the relative function all that is needed to
+*attach* and *detach* its monitor to the system.
+
+For the wip case, these functions were named::
+
+ start_wip()
+ stop_wip()
+
+But no change was required because: by default, these functions *attach* and
+*detach* the tracepoints_to_attach, which was enough for this case.
+
+Instrumentation helpers
+--------------------------
+
+To complete the instrumentation, the *handler functions* need to be attached to a
+kernel event, at the monitoring start phase.
+
+The RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()"
+is used to connect the wip model events to the relative kernel event. dot2k automatically
+adds "rv_attach_trace_probe()" function call for each model event in the start phase, as
+a suggestion.
+
+For example, from the wip sample model::
+
+  static int start_wip(void)
+  {
+        int retval;
+
+        retval = da_monitor_init_wip();
+        if (retval)
+                return retval;
+
+        rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
+        rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
+        rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
+
+        return 0;
+  }
+
+The probes then need to be detached at the stop phase.
-- 
2.35.1


  parent reply	other threads:[~2022-05-05 16:09 UTC|newest]

Thread overview: 21+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-05-05 16:06 [RFC V3 00/20] The Runtime Verification (RV) interface Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 01/20] rv: Add " Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 02/20] rv: Add runtime reactors interface Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 03/20] rv/include: Add helper functions for deterministic automata Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 04/20] rv/include: Add deterministic automata monitor definition via C macros Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 05/20] rv/include: Add instrumentation helper functions Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 06/20] tools/rv: Add dot2c Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 07/20] tools/rv: Add dot2k Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 08/20] rv/monitor: Add the wip monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 09/20] rv/monitor: wip instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 10/20] rv/monitor: Add the wwnr monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 11/20] rv/monitor: wwnr instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 12/20] rv/reactor: Add the printk reactor Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 13/20] rv/reactor: Add the panic reactor Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 14/20] Documentation/rv: Add a basic documentation Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 15/20] Documentation/rv: Add deterministic automata monitor synthesis documentation Daniel Bristot de Oliveira
2022-05-05 16:06 ` Daniel Bristot de Oliveira [this message]
2022-05-05 16:06 ` [RFC V3 17/20] watchdog/dev: Add tracepoints Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 18/20] rv/monitor: Add safe watchdog monitor Daniel Bristot de Oliveira
2022-05-05 16:06 ` [RFC V3 19/20] rv/safety_app: Add an safety_app sample Daniel Bristot de Oliveira
2022-05-05 16:07 ` [RFC V3 20/20] Documentation/rv: Add watchdog-monitor documentation Daniel Bristot de Oliveira

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=9d97a7fd241c08ebbf86d32190d6ae376668495f.1651766361.git.bristot@kernel.org \
    --to=bristot@kernel.org \
    --cc=catalin.marinas@arm.com \
    --cc=corbet@lwn.net \
    --cc=dvyukov@google.com \
    --cc=elver@google.com \
    --cc=gpaoloni@redhat.com \
    --cc=juri.lelli@redhat.com \
    --cc=linux-doc@vger.kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=linux-trace-devel@vger.kernel.org \
    --cc=mingo@redhat.com \
    --cc=paulmck@kernel.org \
    --cc=peterz@infradead.org \
    --cc=rostedt@goodmis.org \
    --cc=skhan@linuxfoundation.org \
    --cc=tglx@linutronix.de \
    --cc=will@kernel.org \
    --cc=williams@redhat.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.