On Wed, Jul 13, 2022 at 11:17:27PM +0200, Daniel Bristot de Oliveira wrote: > Add the da_monitor_instrumentation.rst. It describes the basics > of RV monitor instrumentation. > > Cc: Wim Van Sebroeck <wim@xxxxxxxxxxxxxxxxxx> > Cc: Guenter Roeck <linux@xxxxxxxxxxxx> > Cc: Jonathan Corbet <corbet@xxxxxxx> > Cc: Steven Rostedt <rostedt@xxxxxxxxxxx> > Cc: Ingo Molnar <mingo@xxxxxxxxxx> > Cc: Thomas Gleixner <tglx@xxxxxxxxxxxxx> > Cc: Peter Zijlstra <peterz@xxxxxxxxxxxxx> > Cc: Will Deacon <will@xxxxxxxxxx> > Cc: Catalin Marinas <catalin.marinas@xxxxxxx> > Cc: Marco Elver <elver@xxxxxxxxxx> > Cc: Dmitry Vyukov <dvyukov@xxxxxxxxxx> > Cc: "Paul E. McKenney" <paulmck@xxxxxxxxxx> > Cc: Shuah Khan <skhan@xxxxxxxxxxxxxxxxxxx> > Cc: Gabriele Paoloni <gpaoloni@xxxxxxxxxx> > Cc: Juri Lelli <juri.lelli@xxxxxxxxxx> > Cc: Clark Williams <williams@xxxxxxxxxx> > Cc: Tao Zhou <tao.zhou@xxxxxxxxx> > Cc: Randy Dunlap <rdunlap@xxxxxxxxxxxxx> > Cc: linux-doc@xxxxxxxxxxxxxxx > Cc: linux-kernel@xxxxxxxxxxxxxxx > Cc: linux-trace-devel@xxxxxxxxxxxxxxx > Signed-off-by: Daniel Bristot de Oliveira <bristot@xxxxxxxxxx> > --- > .../trace/rv/da_monitor_instrumentation.rst | 169 ++++++++++++++++++ > Documentation/trace/rv/index.rst | 1 + > 2 files changed, 170 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..7b83d6c7dbed > --- /dev/null > +++ b/Documentation/trace/rv/da_monitor_instrumentation.rst > @@ -0,0 +1,169 @@ > +Deterministic Automata Instrumentation > +======================================== > + > +The RV monitor file created by dot2k, with the name "$MODEL_NAME.c" > +includes a section dedicated to instrumentation. > + > +In the example of the wip.dot monitor created on [1], 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_wip); > + } > + > + static void handle_preempt_enable(void *data, /* XXX: fill header */) > + { > + da_handle_event_wip(preempt_enable_wip); > + } > + > + static void handle_sched_waking(void *data, /* XXX: fill header */) > + { > + da_handle_event_wip(sched_waking_wip); > + } > + > + 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 *model's > +event*. > + > +Tracing callback functions > +----------------------------- > + > +The first three functions are the starting point of the 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_wip); > + } > + > +The preempt_disable event from the model connects 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 event translates one to one with the automata > +event, and indeed, no other change is required 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 has 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 a special handle function, the > +"da_handle_init_event_$(MONITOR)(event)", in this case:: > + > + da_handle_event_wip(preempt_disable_wip); In this case, it is da_handle_init_event_wip(preempt_disable_wip). Thanks.