Skip to content

Commit f75c03a

Browse files
torvaldstorvalds
committed
Merge tag 'trace-rv-v7.0' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace
Pull runtime verifier updates from Steven Rostedt: - Refactor da_monitor to minimize macros Complete refactor of da_monitor.h to reduce reliance on macros generating functions. Use generic static functions and uses the preprocessor only when strictly necessary (e.g. for tracepoint handlers). The change essentially relies on functions with generic names (e.g. da_handle) instead of monitor-specific as well adding the need to define constant (e.g. MONITOR_NAME, MONITOR_TYPE) before including the header rather than calling macros that would define functions. Also adapt monitors and documentation accordingly. - Cleanup DA code generation scripts Clean up functions in dot2c removing reimplementations of trivial library functions (__buff_to_string) and removing some other unused intermediate steps. - Annotate functions with types in the rvgen python scripts - Remove superfluous assignments and cleanup generated code The rvgen scripts generate a superfluous assignment to 0 for enum variables and don't add commas to the last elements, which is against the kernel coding standards. Change the generation process for a better compliance and slightly simpler logic. - Remove superfluous declarations from generated code The monitor container source files contained a declaration and a definition for the rv_monitor variable. The former is superfluous and was removed. - Fix reference to outdated documentation s/da_monitor_synthesis.rst/monitor_synthesis.rst in comment in da_monitor.h * tag 'trace-rv-v7.0' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: rv: Fix documentation reference in da_monitor.h verification/rvgen: Remove unused variable declaration from containers verification/dot2c: Remove superfluous enum assignment and add last comma verification/dot2c: Remove __buff_to_string() and cleanup verification/rvgen: Annotate DA functions with types verification/rvgen: Adapt dot2k and templates after refactoring da_monitor.h Documentation/rv: Adapt documentation after da_monitor refactoring rv: Cleanup da_monitor after refactor rv: Refactor da_monitor to minimise macros
2 parents a67594c + 403faa5 commit f75c03a

31 files changed

Lines changed: 835 additions & 908 deletions

File tree

‎Documentation/trace/rv/monitor_synthesis.rst‎

Lines changed: 21 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -100,54 +100,52 @@ rv/da_monitor.h
100100

101101
This initial implementation presents three different types of monitor instances:
102102

103-
- ``#define DECLARE_DA_MON_GLOBAL(name, type)``
104-
- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
105-
- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
103+
- ``#define RV_MON_TYPE RV_MON_GLOBAL``
104+
- ``#define RV_MON_TYPE RV_MON_PER_CPU``
105+
- ``#define RV_MON_TYPE RV_MON_PER_TASK``
106106

107-
The first declares the functions for a global deterministic automata monitor,
108-
the second for monitors with per-cpu instances, and the third with per-task
109-
instances.
107+
The first sets up functions declaration for a global deterministic automata
108+
monitor, the second for monitors with per-cpu instances, and the third with
109+
per-task instances.
110110

111-
In all cases, the 'name' argument is a string that identifies the monitor, and
112-
the 'type' argument is the data type used by rvgen on the representation of
113-
the model in C.
111+
In all cases, the C file must include the $(MODEL_NAME).h file (generated by
112+
`rvgen`), for example, to define the per-cpu 'wip' monitor, the `wip.c` source
113+
file must include::
114114

115-
For example, the wip model with two states and three events can be
116-
stored in an 'unsigned char' type. Considering that the preemption control
117-
is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
118-
119-
DECLARE_DA_MON_PER_CPU(wip, unsigned char);
115+
#define RV_MON_TYPE RV_MON_PER_CPU
116+
#include "wip.h"
117+
#include <rv/da_monitor.h>
120118

121119
The monitor is executed by sending events to be processed via the functions
122120
presented below::
123121

124-
da_handle_event_$(MONITOR_NAME)($(event from event enum));
125-
da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
126-
da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
122+
da_handle_event($(event from event enum));
123+
da_handle_start_event($(event from event enum));
124+
da_handle_start_run_event($(event from event enum));
127125

128-
The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
126+
The function ``da_handle_event()`` is the regular case where
129127
the event will be processed if the monitor is processing events.
130128

131129
When a monitor is enabled, it is placed in the initial state of the automata.
132130
However, the monitor does not know if the system is in the *initial state*.
133131

134-
The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
132+
The ``da_handle_start_event()`` function is used to notify the
135133
monitor that the system is returning to the initial state, so the monitor can
136134
start monitoring the next event.
137135

138-
The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
136+
The ``da_handle_start_run_event()`` function is used to notify
139137
the monitor that the system is known to be in the initial state, so the
140138
monitor can start monitoring and monitor the current event.
141139

142140
Using the wip model as example, the events "preempt_disable" and
143141
"sched_waking" should be sent to monitor, respectively, via [2]::
144142

145-
da_handle_event_wip(preempt_disable_wip);
146-
da_handle_event_wip(sched_waking_wip);
143+
da_handle_event(preempt_disable_wip);
144+
da_handle_event(sched_waking_wip);
147145

148146
While the event "preempt_enabled" will use::
149147

150-
da_handle_start_event_wip(preempt_enable_wip);
148+
da_handle_start_event(preempt_enable_wip);
151149

152150
To notify the monitor that the system will be returning to the initial state,
153151
so the system and the monitor should be in sync.

‎include/linux/rv.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,10 @@
1010
#define MAX_DA_NAME_LEN 32
1111
#define MAX_DA_RETRY_RACING_EVENTS 3
1212

13+
#define RV_MON_GLOBAL 0
14+
#define RV_MON_PER_CPU 1
15+
#define RV_MON_PER_TASK 2
16+
1317
#ifdef CONFIG_RV
1418
#include <linux/array_size.h>
1519
#include <linux/bitops.h>

‎include/rv/automata.h‎

Lines changed: 69 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -6,70 +6,76 @@
66
* models in C generated by the dot2k tool.
77
*/
88

9+
#ifndef _RV_AUTOMATA_H
10+
#define _RV_AUTOMATA_H
11+
12+
#ifndef MONITOR_NAME
13+
#error "MONITOR_NAME macro is not defined. Did you include $(MODEL_NAME).h generated by rvgen?"
14+
#endif
15+
16+
#define RV_AUTOMATON_NAME CONCATENATE(automaton_, MONITOR_NAME)
17+
#define EVENT_MAX CONCATENATE(event_max_, MONITOR_NAME)
18+
#define STATE_MAX CONCATENATE(state_max_, MONITOR_NAME)
19+
#define events CONCATENATE(events_, MONITOR_NAME)
20+
#define states CONCATENATE(states_, MONITOR_NAME)
21+
22+
/*
23+
* model_get_state_name - return the (string) name of the given state
24+
*/
25+
static char *model_get_state_name(enum states state)
26+
{
27+
if ((state < 0) || (state >= STATE_MAX))
28+
return "INVALID";
29+
30+
return RV_AUTOMATON_NAME.state_names[state];
31+
}
32+
33+
/*
34+
* model_get_event_name - return the (string) name of the given event
35+
*/
36+
static char *model_get_event_name(enum events event)
37+
{
38+
if ((event < 0) || (event >= EVENT_MAX))
39+
return "INVALID";
40+
41+
return RV_AUTOMATON_NAME.event_names[event];
42+
}
43+
944
/*
10-
* DECLARE_AUTOMATA_HELPERS - define a set of helper functions for automata
45+
* model_get_initial_state - return the automaton's initial state
46+
*/
47+
static inline enum states model_get_initial_state(void)
48+
{
49+
return RV_AUTOMATON_NAME.initial_state;
50+
}
51+
52+
/*
53+
* model_get_next_state - process an automaton event occurrence
1154
*
12-
* Define a set of helper functions for automata. The 'name' argument is used
13-
* as suffix for the functions and data. These functions will handle automaton
14-
* with data type 'type'.
55+
* Given the current state (curr_state) and the event (event), returns
56+
* the next state, or INVALID_STATE in case of error.
57+
*/
58+
static inline enum states model_get_next_state(enum states curr_state,
59+
enum events event)
60+
{
61+
if ((curr_state < 0) || (curr_state >= STATE_MAX))
62+
return INVALID_STATE;
63+
64+
if ((event < 0) || (event >= EVENT_MAX))
65+
return INVALID_STATE;
66+
67+
return RV_AUTOMATON_NAME.function[curr_state][event];
68+
}
69+
70+
/*
71+
* model_is_final_state - check if the given state is a final state
1572
*/
16-
#define DECLARE_AUTOMATA_HELPERS(name, type) \
17-
\
18-
/* \
19-
* model_get_state_name_##name - return the (string) name of the given state \
20-
*/ \
21-
static char *model_get_state_name_##name(enum states_##name state) \
22-
{ \
23-
if ((state < 0) || (state >= state_max_##name)) \
24-
return "INVALID"; \
25-
\
26-
return automaton_##name.state_names[state]; \
27-
} \
28-
\
29-
/* \
30-
* model_get_event_name_##name - return the (string) name of the given event \
31-
*/ \
32-
static char *model_get_event_name_##name(enum events_##name event) \
33-
{ \
34-
if ((event < 0) || (event >= event_max_##name)) \
35-
return "INVALID"; \
36-
\
37-
return automaton_##name.event_names[event]; \
38-
} \
39-
\
40-
/* \
41-
* model_get_initial_state_##name - return the automaton's initial state \
42-
*/ \
43-
static inline type model_get_initial_state_##name(void) \
44-
{ \
45-
return automaton_##name.initial_state; \
46-
} \
47-
\
48-
/* \
49-
* model_get_next_state_##name - process an automaton event occurrence \
50-
* \
51-
* Given the current state (curr_state) and the event (event), returns \
52-
* the next state, or INVALID_STATE in case of error. \
53-
*/ \
54-
static inline type model_get_next_state_##name(enum states_##name curr_state, \
55-
enum events_##name event) \
56-
{ \
57-
if ((curr_state < 0) || (curr_state >= state_max_##name)) \
58-
return INVALID_STATE; \
59-
\
60-
if ((event < 0) || (event >= event_max_##name)) \
61-
return INVALID_STATE; \
62-
\
63-
return automaton_##name.function[curr_state][event]; \
64-
} \
65-
\
66-
/* \
67-
* model_is_final_state_##name - check if the given state is a final state \
68-
*/ \
69-
static inline bool model_is_final_state_##name(enum states_##name state) \
70-
{ \
71-
if ((state < 0) || (state >= state_max_##name)) \
72-
return 0; \
73-
\
74-
return automaton_##name.final_states[state]; \
73+
static inline bool model_is_final_state(enum states state)
74+
{
75+
if ((state < 0) || (state >= STATE_MAX))
76+
return 0;
77+
78+
return RV_AUTOMATON_NAME.final_states[state];
7579
}
80+
81+
#endif

0 commit comments

Comments
 (0)