1*b6172b51SDaniel Bristot de OliveiraDeterministic Automata Instrumentation 2*b6172b51SDaniel Bristot de Oliveira====================================== 3*b6172b51SDaniel Bristot de Oliveira 4*b6172b51SDaniel Bristot de OliveiraThe RV monitor file created by dot2k, with the name "$MODEL_NAME.c" 5*b6172b51SDaniel Bristot de Oliveiraincludes a section dedicated to instrumentation. 6*b6172b51SDaniel Bristot de Oliveira 7*b6172b51SDaniel Bristot de OliveiraIn the example of the wip.dot monitor created on [1], it will look like:: 8*b6172b51SDaniel Bristot de Oliveira 9*b6172b51SDaniel Bristot de Oliveira /* 10*b6172b51SDaniel Bristot de Oliveira * This is the instrumentation part of the monitor. 11*b6172b51SDaniel Bristot de Oliveira * 12*b6172b51SDaniel Bristot de Oliveira * This is the section where manual work is required. Here the kernel events 13*b6172b51SDaniel Bristot de Oliveira * are translated into model's event. 14*b6172b51SDaniel Bristot de Oliveira * 15*b6172b51SDaniel Bristot de Oliveira */ 16*b6172b51SDaniel Bristot de Oliveira static void handle_preempt_disable(void *data, /* XXX: fill header */) 17*b6172b51SDaniel Bristot de Oliveira { 18*b6172b51SDaniel Bristot de Oliveira da_handle_event_wip(preempt_disable_wip); 19*b6172b51SDaniel Bristot de Oliveira } 20*b6172b51SDaniel Bristot de Oliveira 21*b6172b51SDaniel Bristot de Oliveira static void handle_preempt_enable(void *data, /* XXX: fill header */) 22*b6172b51SDaniel Bristot de Oliveira { 23*b6172b51SDaniel Bristot de Oliveira da_handle_event_wip(preempt_enable_wip); 24*b6172b51SDaniel Bristot de Oliveira } 25*b6172b51SDaniel Bristot de Oliveira 26*b6172b51SDaniel Bristot de Oliveira static void handle_sched_waking(void *data, /* XXX: fill header */) 27*b6172b51SDaniel Bristot de Oliveira { 28*b6172b51SDaniel Bristot de Oliveira da_handle_event_wip(sched_waking_wip); 29*b6172b51SDaniel Bristot de Oliveira } 30*b6172b51SDaniel Bristot de Oliveira 31*b6172b51SDaniel Bristot de Oliveira static int enable_wip(void) 32*b6172b51SDaniel Bristot de Oliveira { 33*b6172b51SDaniel Bristot de Oliveira int retval; 34*b6172b51SDaniel Bristot de Oliveira 35*b6172b51SDaniel Bristot de Oliveira retval = da_monitor_init_wip(); 36*b6172b51SDaniel Bristot de Oliveira if (retval) 37*b6172b51SDaniel Bristot de Oliveira return retval; 38*b6172b51SDaniel Bristot de Oliveira 39*b6172b51SDaniel Bristot de Oliveira rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable); 40*b6172b51SDaniel Bristot de Oliveira rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable); 41*b6172b51SDaniel Bristot de Oliveira rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking); 42*b6172b51SDaniel Bristot de Oliveira 43*b6172b51SDaniel Bristot de Oliveira return 0; 44*b6172b51SDaniel Bristot de Oliveira } 45*b6172b51SDaniel Bristot de Oliveira 46*b6172b51SDaniel Bristot de OliveiraThe comment at the top of the section explains the general idea: the 47*b6172b51SDaniel Bristot de Oliveirainstrumentation section translates *kernel events* into the *model's 48*b6172b51SDaniel Bristot de Oliveiraevent*. 49*b6172b51SDaniel Bristot de Oliveira 50*b6172b51SDaniel Bristot de OliveiraTracing callback functions 51*b6172b51SDaniel Bristot de Oliveira-------------------------- 52*b6172b51SDaniel Bristot de Oliveira 53*b6172b51SDaniel Bristot de OliveiraThe first three functions are the starting point of the callback *handler 54*b6172b51SDaniel Bristot de Oliveirafunctions* for each of the three events from the wip model. The developer 55*b6172b51SDaniel Bristot de Oliveiradoes not necessarily need to use them: they are just starting points. 56*b6172b51SDaniel Bristot de Oliveira 57*b6172b51SDaniel Bristot de OliveiraUsing the example of:: 58*b6172b51SDaniel Bristot de Oliveira 59*b6172b51SDaniel Bristot de Oliveira void handle_preempt_disable(void *data, /* XXX: fill header */) 60*b6172b51SDaniel Bristot de Oliveira { 61*b6172b51SDaniel Bristot de Oliveira da_handle_event_wip(preempt_disable_wip); 62*b6172b51SDaniel Bristot de Oliveira } 63*b6172b51SDaniel Bristot de Oliveira 64*b6172b51SDaniel Bristot de OliveiraThe preempt_disable event from the model connects directly to the 65*b6172b51SDaniel Bristot de Oliveirapreemptirq:preempt_disable. The preemptirq:preempt_disable event 66*b6172b51SDaniel Bristot de Oliveirahas the following signature, from include/trace/events/preemptirq.h:: 67*b6172b51SDaniel Bristot de Oliveira 68*b6172b51SDaniel Bristot de Oliveira TP_PROTO(unsigned long ip, unsigned long parent_ip) 69*b6172b51SDaniel Bristot de Oliveira 70*b6172b51SDaniel Bristot de OliveiraHence, the handle_preempt_disable() function will look like:: 71*b6172b51SDaniel Bristot de Oliveira 72*b6172b51SDaniel Bristot de Oliveira void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip) 73*b6172b51SDaniel Bristot de Oliveira 74*b6172b51SDaniel Bristot de OliveiraIn this case, the kernel event translates one to one with the automata 75*b6172b51SDaniel Bristot de Oliveiraevent, and indeed, no other change is required for this function. 76*b6172b51SDaniel Bristot de Oliveira 77*b6172b51SDaniel Bristot de OliveiraThe next handler function, handle_preempt_enable() has the same argument 78*b6172b51SDaniel Bristot de Oliveiralist from the handle_preempt_disable(). The difference is that the 79*b6172b51SDaniel Bristot de Oliveirapreempt_enable event will be used to synchronize the system to the model. 80*b6172b51SDaniel Bristot de Oliveira 81*b6172b51SDaniel Bristot de OliveiraInitially, the *model* is placed in the initial state. However, the *system* 82*b6172b51SDaniel Bristot de Oliveiramight or might not be in the initial state. The monitor cannot start 83*b6172b51SDaniel Bristot de Oliveiraprocessing events until it knows that the system has reached the initial state. 84*b6172b51SDaniel Bristot de OliveiraOtherwise, the monitor and the system could be out-of-sync. 85*b6172b51SDaniel Bristot de Oliveira 86*b6172b51SDaniel Bristot de OliveiraLooking at the automata definition, it is possible to see that the system 87*b6172b51SDaniel Bristot de Oliveiraand the model are expected to return to the initial state after the 88*b6172b51SDaniel Bristot de Oliveirapreempt_enable execution. Hence, it can be used to synchronize the 89*b6172b51SDaniel Bristot de Oliveirasystem and the model at the initialization of the monitoring section. 90*b6172b51SDaniel Bristot de Oliveira 91*b6172b51SDaniel Bristot de OliveiraThe start is informed via a special handle function, the 92*b6172b51SDaniel Bristot de Oliveira"da_handle_start_event_$(MONITOR_NAME)(event)", in this case:: 93*b6172b51SDaniel Bristot de Oliveira 94*b6172b51SDaniel Bristot de Oliveira da_handle_start_event_wip(preempt_enable_wip); 95*b6172b51SDaniel Bristot de Oliveira 96*b6172b51SDaniel Bristot de OliveiraSo, the callback function will look like:: 97*b6172b51SDaniel Bristot de Oliveira 98*b6172b51SDaniel Bristot de Oliveira void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip) 99*b6172b51SDaniel Bristot de Oliveira { 100*b6172b51SDaniel Bristot de Oliveira da_handle_start_event_wip(preempt_enable_wip); 101*b6172b51SDaniel Bristot de Oliveira } 102*b6172b51SDaniel Bristot de Oliveira 103*b6172b51SDaniel Bristot de OliveiraFinally, the "handle_sched_waking()" will look like:: 104*b6172b51SDaniel Bristot de Oliveira 105*b6172b51SDaniel Bristot de Oliveira void handle_sched_waking(void *data, struct task_struct *task) 106*b6172b51SDaniel Bristot de Oliveira { 107*b6172b51SDaniel Bristot de Oliveira da_handle_event_wip(sched_waking_wip); 108*b6172b51SDaniel Bristot de Oliveira } 109*b6172b51SDaniel Bristot de Oliveira 110*b6172b51SDaniel Bristot de OliveiraAnd the explanation is left for the reader as an exercise. 111*b6172b51SDaniel Bristot de Oliveira 112*b6172b51SDaniel Bristot de Oliveiraenable and disable functions 113*b6172b51SDaniel Bristot de Oliveira---------------------------- 114*b6172b51SDaniel Bristot de Oliveira 115*b6172b51SDaniel Bristot de Oliveiradot2k automatically creates two special functions:: 116*b6172b51SDaniel Bristot de Oliveira 117*b6172b51SDaniel Bristot de Oliveira enable_$(MONITOR_NAME)() 118*b6172b51SDaniel Bristot de Oliveira disable_$(MONITOR_NAME)() 119*b6172b51SDaniel Bristot de Oliveira 120*b6172b51SDaniel Bristot de OliveiraThese functions are called when the monitor is enabled and disabled, 121*b6172b51SDaniel Bristot de Oliveirarespectively. 122*b6172b51SDaniel Bristot de Oliveira 123*b6172b51SDaniel Bristot de OliveiraThey should be used to *attach* and *detach* the instrumentation to the running 124*b6172b51SDaniel Bristot de Oliveirasystem. The developer must add to the relative function all that is needed to 125*b6172b51SDaniel Bristot de Oliveira*attach* and *detach* its monitor to the system. 126*b6172b51SDaniel Bristot de Oliveira 127*b6172b51SDaniel Bristot de OliveiraFor the wip case, these functions were named:: 128*b6172b51SDaniel Bristot de Oliveira 129*b6172b51SDaniel Bristot de Oliveira enable_wip() 130*b6172b51SDaniel Bristot de Oliveira disable_wip() 131*b6172b51SDaniel Bristot de Oliveira 132*b6172b51SDaniel Bristot de OliveiraBut no change was required because: by default, these functions *attach* and 133*b6172b51SDaniel Bristot de Oliveira*detach* the tracepoints_to_attach, which was enough for this case. 134*b6172b51SDaniel Bristot de Oliveira 135*b6172b51SDaniel Bristot de OliveiraInstrumentation helpers 136*b6172b51SDaniel Bristot de Oliveira----------------------- 137*b6172b51SDaniel Bristot de Oliveira 138*b6172b51SDaniel Bristot de OliveiraTo complete the instrumentation, the *handler functions* need to be attached to a 139*b6172b51SDaniel Bristot de Oliveirakernel event, at the monitoring enable phase. 140*b6172b51SDaniel Bristot de Oliveira 141*b6172b51SDaniel Bristot de OliveiraThe RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()" 142*b6172b51SDaniel Bristot de Oliveirais used to connect the wip model events to the relative kernel event. dot2k automatically 143*b6172b51SDaniel Bristot de Oliveiraadds "rv_attach_trace_probe()" function call for each model event in the enable phase, as 144*b6172b51SDaniel Bristot de Oliveiraa suggestion. 145*b6172b51SDaniel Bristot de Oliveira 146*b6172b51SDaniel Bristot de OliveiraFor example, from the wip sample model:: 147*b6172b51SDaniel Bristot de Oliveira 148*b6172b51SDaniel Bristot de Oliveira static int enable_wip(void) 149*b6172b51SDaniel Bristot de Oliveira { 150*b6172b51SDaniel Bristot de Oliveira int retval; 151*b6172b51SDaniel Bristot de Oliveira 152*b6172b51SDaniel Bristot de Oliveira retval = da_monitor_init_wip(); 153*b6172b51SDaniel Bristot de Oliveira if (retval) 154*b6172b51SDaniel Bristot de Oliveira return retval; 155*b6172b51SDaniel Bristot de Oliveira 156*b6172b51SDaniel Bristot de Oliveira rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable); 157*b6172b51SDaniel Bristot de Oliveira rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking); 158*b6172b51SDaniel Bristot de Oliveira rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable); 159*b6172b51SDaniel Bristot de Oliveira 160*b6172b51SDaniel Bristot de Oliveira return 0; 161*b6172b51SDaniel Bristot de Oliveira } 162*b6172b51SDaniel Bristot de Oliveira 163*b6172b51SDaniel Bristot de OliveiraThe probes then need to be detached at the disable phase. 164*b6172b51SDaniel Bristot de Oliveira 165*b6172b51SDaniel Bristot de Oliveira[1] The wip model is presented in:: 166*b6172b51SDaniel Bristot de Oliveira 167*b6172b51SDaniel Bristot de Oliveira Documentation/trace/rv/deterministic_automata.rst 168*b6172b51SDaniel Bristot de Oliveira 169*b6172b51SDaniel Bristot de OliveiraThe wip monitor is presented in:: 170*b6172b51SDaniel Bristot de Oliveira 171*b6172b51SDaniel Bristot de Oliveira Documentation/trace/rv/da_monitor_synthesis.rst 172