Documentation/trace/rv/da_monitor_instrumentation.rst
Source file repositories/reference/linux-study-clean/Documentation/trace/rv/da_monitor_instrumentation.rst
File Facts
- System
- Linux kernel
- Corpus path
Documentation/trace/rv/da_monitor_instrumentation.rst- Extension
.rst- Size
- 5528 bytes
- Lines
- 172
- Domain
- Support Tooling And Documentation
- Bucket
- Documentation
- Inferred role
- Support Tooling And Documentation: documentation
- Status
- atlas-only
Why This File Exists
Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.
- Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.
- Defines or uses C structs; map object ownership, embedded links, reference counts, and lock ownership.
Dependency Surface
- No C-style include directives detected by the generator.
Detected Declarations
function handle_preempt_disablefunction handle_preempt_enablefunction handle_sched_wakingfunction enable_wipfunction handle_preempt_disablefunction handle_preempt_enablefunction handle_sched_wakingfunction enable_wip
Annotated Snippet
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 enable_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::
Annotation
- Detected declarations: `function handle_preempt_disable`, `function handle_preempt_enable`, `function handle_sched_waking`, `function enable_wip`, `function handle_preempt_disable`, `function handle_preempt_enable`, `function handle_sched_waking`, `function enable_wip`.
- Atlas domain: Support Tooling And Documentation / Documentation.
- Implementation status: atlas-only.
Implementation Notes
- This generated page is the file-by-file coverage layer; curated subsystem chapters should link here when they synthesize a multi-file control flow.
- Core OS pages should be promoted from atlas-only to deep-reviewed when they explain data structures, invariants, locking, lifecycle, and C implementation snippets.
- Driver-family pages are intentionally pattern-oriented unless they are part of the selected PCIe/NVMe representative device path.