0001 Deterministic Automata Instrumentation
0002 ======================================
0003
0004 The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
0005 includes a section dedicated to instrumentation.
0006
0007 In the example of the wip.dot monitor created on [1], it will look like::
0008
0009 /*
0010 * This is the instrumentation part of the monitor.
0011 *
0012 * This is the section where manual work is required. Here the kernel events
0013 * are translated into model's event.
0014 *
0015 */
0016 static void handle_preempt_disable(void *data, /* XXX: fill header */)
0017 {
0018 da_handle_event_wip(preempt_disable_wip);
0019 }
0020
0021 static void handle_preempt_enable(void *data, /* XXX: fill header */)
0022 {
0023 da_handle_event_wip(preempt_enable_wip);
0024 }
0025
0026 static void handle_sched_waking(void *data, /* XXX: fill header */)
0027 {
0028 da_handle_event_wip(sched_waking_wip);
0029 }
0030
0031 static int enable_wip(void)
0032 {
0033 int retval;
0034
0035 retval = da_monitor_init_wip();
0036 if (retval)
0037 return retval;
0038
0039 rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
0040 rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
0041 rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
0042
0043 return 0;
0044 }
0045
0046 The comment at the top of the section explains the general idea: the
0047 instrumentation section translates *kernel events* into the *model's
0048 event*.
0049
0050 Tracing callback functions
0051 --------------------------
0052
0053 The first three functions are the starting point of the callback *handler
0054 functions* for each of the three events from the wip model. The developer
0055 does not necessarily need to use them: they are just starting points.
0056
0057 Using the example of::
0058
0059 void handle_preempt_disable(void *data, /* XXX: fill header */)
0060 {
0061 da_handle_event_wip(preempt_disable_wip);
0062 }
0063
0064 The preempt_disable event from the model connects directly to the
0065 preemptirq:preempt_disable. The preemptirq:preempt_disable event
0066 has the following signature, from include/trace/events/preemptirq.h::
0067
0068 TP_PROTO(unsigned long ip, unsigned long parent_ip)
0069
0070 Hence, the handle_preempt_disable() function will look like::
0071
0072 void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
0073
0074 In this case, the kernel event translates one to one with the automata
0075 event, and indeed, no other change is required for this function.
0076
0077 The next handler function, handle_preempt_enable() has the same argument
0078 list from the handle_preempt_disable(). The difference is that the
0079 preempt_enable event will be used to synchronize the system to the model.
0080
0081 Initially, the *model* is placed in the initial state. However, the *system*
0082 might or might not be in the initial state. The monitor cannot start
0083 processing events until it knows that the system has reached the initial state.
0084 Otherwise, the monitor and the system could be out-of-sync.
0085
0086 Looking at the automata definition, it is possible to see that the system
0087 and the model are expected to return to the initial state after the
0088 preempt_enable execution. Hence, it can be used to synchronize the
0089 system and the model at the initialization of the monitoring section.
0090
0091 The start is informed via a special handle function, the
0092 "da_handle_start_event_$(MONITOR_NAME)(event)", in this case::
0093
0094 da_handle_start_event_wip(preempt_enable_wip);
0095
0096 So, the callback function will look like::
0097
0098 void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
0099 {
0100 da_handle_start_event_wip(preempt_enable_wip);
0101 }
0102
0103 Finally, the "handle_sched_waking()" will look like::
0104
0105 void handle_sched_waking(void *data, struct task_struct *task)
0106 {
0107 da_handle_event_wip(sched_waking_wip);
0108 }
0109
0110 And the explanation is left for the reader as an exercise.
0111
0112 enable and disable functions
0113 ----------------------------
0114
0115 dot2k automatically creates two special functions::
0116
0117 enable_$(MONITOR_NAME)()
0118 disable_$(MONITOR_NAME)()
0119
0120 These functions are called when the monitor is enabled and disabled,
0121 respectively.
0122
0123 They should be used to *attach* and *detach* the instrumentation to the running
0124 system. The developer must add to the relative function all that is needed to
0125 *attach* and *detach* its monitor to the system.
0126
0127 For the wip case, these functions were named::
0128
0129 enable_wip()
0130 disable_wip()
0131
0132 But no change was required because: by default, these functions *attach* and
0133 *detach* the tracepoints_to_attach, which was enough for this case.
0134
0135 Instrumentation helpers
0136 -----------------------
0137
0138 To complete the instrumentation, the *handler functions* need to be attached to a
0139 kernel event, at the monitoring enable phase.
0140
0141 The RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()"
0142 is used to connect the wip model events to the relative kernel event. dot2k automatically
0143 adds "rv_attach_trace_probe()" function call for each model event in the enable phase, as
0144 a suggestion.
0145
0146 For example, from the wip sample model::
0147
0148 static int enable_wip(void)
0149 {
0150 int retval;
0151
0152 retval = da_monitor_init_wip();
0153 if (retval)
0154 return retval;
0155
0156 rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
0157 rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
0158 rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
0159
0160 return 0;
0161 }
0162
0163 The probes then need to be detached at the disable phase.
0164
0165 [1] The wip model is presented in::
0166
0167 Documentation/trace/rv/deterministic_automata.rst
0168
0169 The wip monitor is presented in::
0170
0171 Documentation/trace/rv/da_monitor_synthesis.rst
