Linux kernel mirror (for testing)
git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
kernel
os
linux
rv: Add Hybrid Automata monitor type
Deterministic automata define which events are allowed in every state,
but cannot define more sophisticated constraint taking into account the
system's environment (e.g. time or other states not producing events).
Add the Hybrid Automata monitor type as an extension of Deterministic
automata where each state transition is validating a constraint on a
finite number of environment variables.
Hybrid automata can be used to implement timed automata, where the
environment variables are clocks.
Also implement the necessary functionality to handle clock constraints
(ns or jiffy granularity) on state and events.
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260330111010.153663-3-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
+658
-4
+38
include/linux/rv.h
+38
include/linux/rv.h
···
81
81
82
82
#endif /* CONFIG_RV_LTL_MONITOR */
83
83
84
+
#ifdef CONFIG_RV_HA_MONITOR
85
+
/*
86
+
* In the future, hybrid automata may rely on multiple
87
+
* environment variables, e.g. different clocks started at
88
+
* different times or running at different speed.
89
+
* For now we support only 1 variable.
90
+
*/
91
+
#define MAX_HA_ENV_LEN 1
92
+
93
+
/*
94
+
* Monitors can pick the preferred timer implementation:
95
+
* No timer: if monitors don't have state invariants.
96
+
* Timer wheel: lightweight invariants check but far less precise.
97
+
* Hrtimer: accurate invariants check with higher overhead.
98
+
*/
99
+
#define HA_TIMER_NONE 0
100
+
#define HA_TIMER_WHEEL 1
101
+
#define HA_TIMER_HRTIMER 2
102
+
103
+
/*
104
+
* Hybrid automaton per-object variables.
105
+
*/
106
+
struct ha_monitor {
107
+
struct da_monitor da_mon;
108
+
u64 env_store[MAX_HA_ENV_LEN];
109
+
union {
110
+
struct hrtimer hrtimer;
111
+
struct timer_list timer;
112
+
};
113
+
};
114
+
115
+
#else
116
+
117
+
struct ha_monitor { };
118
+
119
+
#endif /* CONFIG_RV_HA_MONITOR */
120
+
84
121
#define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS)
85
122
86
123
union rv_task_monitor {
87
124
struct da_monitor da_mon;
88
125
struct ltl_monitor ltl_mon;
126
+
struct ha_monitor ha_mon;
89
127
};
90
128
91
129
#ifdef CONFIG_RV_REACTORS
+69
-4
include/rv/da_monitor.h
+69
-4
include/rv/da_monitor.h
···
3
3
* Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
4
4
*
5
5
* Deterministic automata (DA) monitor functions, to be used together
6
-
* with automata models in C generated by the dot2k tool.
6
+
* with automata models in C generated by the rvgen tool.
7
7
*
8
-
* The dot2k tool is available at tools/verification/dot2k/
8
+
* The rvgen tool is available at tools/verification/rvgen/
9
9
*
10
10
* For further information, see:
11
11
* Documentation/trace/rv/monitor_synthesis.rst
···
29
29
static struct rv_monitor rv_this;
30
30
31
31
/*
32
+
* Hook to allow the implementation of hybrid automata: define it with a
33
+
* function that takes curr_state, event and next_state and returns true if the
34
+
* environment constraints (e.g. timing) are satisfied, false otherwise.
35
+
*/
36
+
#ifndef da_monitor_event_hook
37
+
#define da_monitor_event_hook(...) true
38
+
#endif
39
+
40
+
/*
41
+
* Hook to allow the implementation of hybrid automata: define it with a
42
+
* function that takes the da_monitor and performs further initialisation
43
+
* (e.g. reset set up timers).
44
+
*/
45
+
#ifndef da_monitor_init_hook
46
+
#define da_monitor_init_hook(da_mon)
47
+
#endif
48
+
49
+
/*
50
+
* Hook to allow the implementation of hybrid automata: define it with a
51
+
* function that takes the da_monitor and performs further reset (e.g. reset
52
+
* all clocks).
53
+
*/
54
+
#ifndef da_monitor_reset_hook
55
+
#define da_monitor_reset_hook(da_mon)
56
+
#endif
57
+
58
+
/*
32
59
* Type for the target id, default to int but can be overridden.
33
60
*/
34
61
#ifndef da_id_type
···
76
49
*/
77
50
static inline void da_monitor_reset(struct da_monitor *da_mon)
78
51
{
52
+
da_monitor_reset_hook(da_mon);
79
53
da_mon->monitoring = 0;
80
54
da_mon->curr_state = model_get_initial_state();
81
55
}
···
91
63
{
92
64
da_mon->curr_state = model_get_initial_state();
93
65
da_mon->monitoring = 1;
66
+
da_monitor_init_hook(da_mon);
94
67
}
95
68
96
69
/*
···
171
142
/*
172
143
* da_monitor_destroy - destroy the monitor
173
144
*/
174
-
static inline void da_monitor_destroy(void) { }
145
+
static inline void da_monitor_destroy(void)
146
+
{
147
+
da_monitor_reset_all();
148
+
}
175
149
176
150
#elif RV_MON_TYPE == RV_MON_PER_CPU
177
151
/*
···
220
188
/*
221
189
* da_monitor_destroy - destroy the monitor
222
190
*/
223
-
static inline void da_monitor_destroy(void) { }
191
+
static inline void da_monitor_destroy(void)
192
+
{
193
+
da_monitor_reset_all();
194
+
}
224
195
225
196
#elif RV_MON_TYPE == RV_MON_PER_TASK
226
197
/*
···
242
207
static inline struct da_monitor *da_get_monitor(struct task_struct *tsk)
243
208
{
244
209
return &tsk->rv[task_mon_slot].da_mon;
210
+
}
211
+
212
+
/*
213
+
* da_get_task - return the task associated to the monitor
214
+
*/
215
+
static inline struct task_struct *da_get_task(struct da_monitor *da_mon)
216
+
{
217
+
return container_of(da_mon, struct task_struct, rv[task_mon_slot].da_mon);
218
+
}
219
+
220
+
/*
221
+
* da_get_id - return the id associated to the monitor
222
+
*
223
+
* For per-task monitors, the id is the task's PID.
224
+
*/
225
+
static inline da_id_type da_get_id(struct da_monitor *da_mon)
226
+
{
227
+
return da_get_task(da_mon)->pid;
245
228
}
246
229
247
230
static void da_monitor_reset_all(void)
···
306
253
}
307
254
rv_put_task_monitor_slot(task_mon_slot);
308
255
task_mon_slot = RV_PER_TASK_MONITOR_INIT;
256
+
257
+
da_monitor_reset_all();
309
258
}
310
259
#endif /* RV_MON_TYPE */
311
260
···
332
277
da_id_type id)
333
278
{
334
279
CONCATENATE(trace_error_, MONITOR_NAME)(curr_state, event);
280
+
}
281
+
282
+
/*
283
+
* da_get_id - unused for implicit monitors
284
+
*/
285
+
static inline da_id_type da_get_id(struct da_monitor *da_mon)
286
+
{
287
+
return 0;
335
288
}
336
289
337
290
#elif RV_MON_TYPE == RV_MON_PER_TASK
···
386
323
return false;
387
324
}
388
325
if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {
326
+
if (!da_monitor_event_hook(da_mon, curr_state, event, next_state, id))
327
+
return false;
389
328
da_trace_event(da_mon, model_get_state_name(curr_state),
390
329
model_get_event_name(event),
391
330
model_get_state_name(next_state),
+475
include/rv/ha_monitor.h
+475
include/rv/ha_monitor.h
···
1
+
/* SPDX-License-Identifier: GPL-2.0 */
2
+
/*
3
+
* Copyright (C) 2025-2028 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com>
4
+
*
5
+
* Hybrid automata (HA) monitor functions, to be used together
6
+
* with automata models in C generated by the rvgen tool.
7
+
*
8
+
* This type of monitors extends the Deterministic automata (DA) class by
9
+
* adding a set of environment variables (e.g. clocks) that can be used to
10
+
* constraint the valid transitions.
11
+
*
12
+
* The rvgen tool is available at tools/verification/rvgen/
13
+
*
14
+
* For further information, see:
15
+
* Documentation/trace/rv/monitor_synthesis.rst
16
+
*/
17
+
18
+
#ifndef _RV_HA_MONITOR_H
19
+
#define _RV_HA_MONITOR_H
20
+
21
+
#include <rv/automata.h>
22
+
23
+
#ifndef da_id_type
24
+
#define da_id_type int
25
+
#endif
26
+
27
+
static inline void ha_monitor_init_env(struct da_monitor *da_mon);
28
+
static inline void ha_monitor_reset_env(struct da_monitor *da_mon);
29
+
static inline void ha_setup_timer(struct ha_monitor *ha_mon);
30
+
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon);
31
+
static bool ha_monitor_handle_constraint(struct da_monitor *da_mon,
32
+
enum states curr_state,
33
+
enum events event,
34
+
enum states next_state,
35
+
da_id_type id);
36
+
#define da_monitor_event_hook ha_monitor_handle_constraint
37
+
#define da_monitor_init_hook ha_monitor_init_env
38
+
#define da_monitor_reset_hook ha_monitor_reset_env
39
+
40
+
#include <rv/da_monitor.h>
41
+
#include <linux/seq_buf.h>
42
+
43
+
/* This simplifies things since da_mon and ha_mon coexist in the same union */
44
+
_Static_assert(offsetof(struct ha_monitor, da_mon) == 0,
45
+
"da_mon must be the first element in an ha_mon!");
46
+
#define to_ha_monitor(da) container_of(da, struct ha_monitor, da_mon)
47
+
48
+
#define ENV_MAX CONCATENATE(env_max_, MONITOR_NAME)
49
+
#define ENV_MAX_STORED CONCATENATE(env_max_stored_, MONITOR_NAME)
50
+
#define envs CONCATENATE(envs_, MONITOR_NAME)
51
+
52
+
/* Environment storage before being reset */
53
+
#define ENV_INVALID_VALUE U64_MAX
54
+
/* Error with no event occurs only on timeouts */
55
+
#define EVENT_NONE EVENT_MAX
56
+
#define EVENT_NONE_LBL "none"
57
+
#define ENV_BUFFER_SIZE 64
58
+
59
+
#ifdef CONFIG_RV_REACTORS
60
+
61
+
/*
62
+
* ha_react - trigger the reaction after a failed environment constraint
63
+
*
64
+
* The transition from curr_state with event is otherwise valid, but the
65
+
* environment constraint is false. This function can be called also with no
66
+
* event from a timer (state constraints only).
67
+
*/
68
+
static void ha_react(enum states curr_state, enum events event, char *env)
69
+
{
70
+
rv_react(&rv_this,
71
+
"rv: monitor %s does not allow event %s on state %s with env %s\n",
72
+
__stringify(MONITOR_NAME),
73
+
event == EVENT_NONE ? EVENT_NONE_LBL : model_get_event_name(event),
74
+
model_get_state_name(curr_state), env);
75
+
}
76
+
77
+
#else /* CONFIG_RV_REACTOR */
78
+
79
+
static void ha_react(enum states curr_state, enum events event, char *env) { }
80
+
#endif
81
+
82
+
/*
83
+
* model_get_state_name - return the (string) name of the given state
84
+
*/
85
+
static char *model_get_env_name(enum envs env)
86
+
{
87
+
if ((env < 0) || (env >= ENV_MAX))
88
+
return "INVALID";
89
+
90
+
return RV_AUTOMATON_NAME.env_names[env];
91
+
}
92
+
93
+
/*
94
+
* Monitors requiring a timer implementation need to request it explicitly.
95
+
*/
96
+
#ifndef HA_TIMER_TYPE
97
+
#define HA_TIMER_TYPE HA_TIMER_NONE
98
+
#endif
99
+
100
+
#if HA_TIMER_TYPE == HA_TIMER_WHEEL
101
+
static void ha_monitor_timer_callback(struct timer_list *timer);
102
+
#elif HA_TIMER_TYPE == HA_TIMER_HRTIMER
103
+
static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer);
104
+
#endif
105
+
106
+
/*
107
+
* ktime_get_ns is expensive, since we usually don't require precise accounting
108
+
* of changes within the same event, cache the current time at the beginning of
109
+
* the constraint handler and use the cache for subsequent calls.
110
+
* Monitors without ns clocks automatically skip this.
111
+
*/
112
+
#ifdef HA_CLK_NS
113
+
#define ha_get_ns() ktime_get_ns()
114
+
#else
115
+
#define ha_get_ns() 0
116
+
#endif /* HA_CLK_NS */
117
+
118
+
/* Should be supplied by the monitor */
119
+
static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env, u64 time_ns);
120
+
static bool ha_verify_constraint(struct ha_monitor *ha_mon,
121
+
enum states curr_state,
122
+
enum events event,
123
+
enum states next_state,
124
+
u64 time_ns);
125
+
126
+
/*
127
+
* ha_monitor_reset_all_stored - reset all environment variables in the monitor
128
+
*/
129
+
static inline void ha_monitor_reset_all_stored(struct ha_monitor *ha_mon)
130
+
{
131
+
for (int i = 0; i < ENV_MAX_STORED; i++)
132
+
WRITE_ONCE(ha_mon->env_store[i], ENV_INVALID_VALUE);
133
+
}
134
+
135
+
/*
136
+
* ha_monitor_init_env - setup timer and reset all environment
137
+
*
138
+
* Called from a hook in the DA start functions, it supplies the da_mon
139
+
* corresponding to the current ha_mon.
140
+
* Not all hybrid automata require the timer, still set it for simplicity.
141
+
*/
142
+
static inline void ha_monitor_init_env(struct da_monitor *da_mon)
143
+
{
144
+
struct ha_monitor *ha_mon = to_ha_monitor(da_mon);
145
+
146
+
ha_monitor_reset_all_stored(ha_mon);
147
+
ha_setup_timer(ha_mon);
148
+
}
149
+
150
+
/*
151
+
* ha_monitor_reset_env - stop timer and reset all environment
152
+
*
153
+
* Called from a hook in the DA reset functions, it supplies the da_mon
154
+
* corresponding to the current ha_mon.
155
+
* Not all hybrid automata require the timer, still clear it for simplicity.
156
+
*/
157
+
static inline void ha_monitor_reset_env(struct da_monitor *da_mon)
158
+
{
159
+
struct ha_monitor *ha_mon = to_ha_monitor(da_mon);
160
+
161
+
/* Initialisation resets the monitor before initialising the timer */
162
+
if (likely(da_monitoring(da_mon)))
163
+
ha_cancel_timer(ha_mon);
164
+
}
165
+
166
+
/*
167
+
* ha_monitor_env_invalid - return true if env has not been initialised
168
+
*/
169
+
static inline bool ha_monitor_env_invalid(struct ha_monitor *ha_mon, enum envs env)
170
+
{
171
+
return READ_ONCE(ha_mon->env_store[env]) == ENV_INVALID_VALUE;
172
+
}
173
+
174
+
static inline void ha_get_env_string(struct seq_buf *s,
175
+
struct ha_monitor *ha_mon, u64 time_ns)
176
+
{
177
+
const char *format_str = "%s=%llu";
178
+
179
+
for (int i = 0; i < ENV_MAX; i++) {
180
+
seq_buf_printf(s, format_str, model_get_env_name(i),
181
+
ha_get_env(ha_mon, i, time_ns));
182
+
format_str = ",%s=%llu";
183
+
}
184
+
}
185
+
186
+
#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
187
+
static inline void ha_trace_error_env(struct ha_monitor *ha_mon,
188
+
char *curr_state, char *event, char *env,
189
+
da_id_type id)
190
+
{
191
+
CONCATENATE(trace_error_env_, MONITOR_NAME)(curr_state, event, env);
192
+
}
193
+
#elif RV_MON_TYPE == RV_MON_PER_TASK
194
+
static inline void ha_trace_error_env(struct ha_monitor *ha_mon,
195
+
char *curr_state, char *event, char *env,
196
+
da_id_type id)
197
+
{
198
+
CONCATENATE(trace_error_env_, MONITOR_NAME)(id, curr_state, event, env);
199
+
}
200
+
#endif /* RV_MON_TYPE */
201
+
202
+
/*
203
+
* ha_get_monitor - return the current monitor
204
+
*/
205
+
#define ha_get_monitor(...) to_ha_monitor(da_get_monitor(__VA_ARGS__))
206
+
207
+
/*
208
+
* ha_monitor_handle_constraint - handle the constraint on the current transition
209
+
*
210
+
* If the monitor implementation defines a constraint in the transition from
211
+
* curr_state to event, react and trace appropriately as well as return false.
212
+
* This function is called from the hook in the DA event handle function and
213
+
* triggers a failure in the monitor.
214
+
*/
215
+
static bool ha_monitor_handle_constraint(struct da_monitor *da_mon,
216
+
enum states curr_state,
217
+
enum events event,
218
+
enum states next_state,
219
+
da_id_type id)
220
+
{
221
+
struct ha_monitor *ha_mon = to_ha_monitor(da_mon);
222
+
u64 time_ns = ha_get_ns();
223
+
DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE);
224
+
225
+
if (ha_verify_constraint(ha_mon, curr_state, event, next_state, time_ns))
226
+
return true;
227
+
228
+
ha_get_env_string(&env_string, ha_mon, time_ns);
229
+
ha_react(curr_state, event, env_string.buffer);
230
+
ha_trace_error_env(ha_mon,
231
+
model_get_state_name(curr_state),
232
+
model_get_event_name(event),
233
+
env_string.buffer, id);
234
+
return false;
235
+
}
236
+
237
+
static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
238
+
{
239
+
enum states curr_state = READ_ONCE(ha_mon->da_mon.curr_state);
240
+
DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE);
241
+
u64 time_ns = ha_get_ns();
242
+
243
+
ha_get_env_string(&env_string, ha_mon, time_ns);
244
+
ha_react(curr_state, EVENT_NONE, env_string.buffer);
245
+
ha_trace_error_env(ha_mon, model_get_state_name(curr_state),
246
+
EVENT_NONE_LBL, env_string.buffer,
247
+
da_get_id(&ha_mon->da_mon));
248
+
249
+
da_monitor_reset(&ha_mon->da_mon);
250
+
}
251
+
252
+
/*
253
+
* The clock variables have 2 different representations in the env_store:
254
+
* - The guard representation is the timestamp of the last reset
255
+
* - The invariant representation is the timestamp when the invariant expires
256
+
* As the representations are incompatible, care must be taken when switching
257
+
* between them: the invariant representation can only be used when starting a
258
+
* timer when the previous representation was guard (e.g. no other invariant
259
+
* started since the last reset operation).
260
+
* Likewise, switching from invariant to guard representation without a reset
261
+
* can be done only by subtracting the exact value used to start the invariant.
262
+
*
263
+
* Reading the environment variable (ha_get_clk) also reflects this difference
264
+
* any reads in states that have an invariant return the (possibly negative)
265
+
* time since expiration, other reads return the time since last reset.
266
+
*/
267
+
268
+
/*
269
+
* Helper functions for env variables describing clocks with ns granularity
270
+
*/
271
+
static inline u64 ha_get_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
272
+
{
273
+
return time_ns - READ_ONCE(ha_mon->env_store[env]);
274
+
}
275
+
static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
276
+
{
277
+
WRITE_ONCE(ha_mon->env_store[env], time_ns);
278
+
}
279
+
static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
280
+
u64 value, u64 time_ns)
281
+
{
282
+
WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
283
+
}
284
+
static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
285
+
enum envs env, u64 time_ns)
286
+
{
287
+
return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
288
+
}
289
+
/*
290
+
* ha_invariant_passed_ns - prepare the invariant and return the time since reset
291
+
*/
292
+
static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env,
293
+
u64 expire, u64 time_ns)
294
+
{
295
+
u64 passed = 0;
296
+
297
+
if (env < 0 || env >= ENV_MAX_STORED)
298
+
return 0;
299
+
if (ha_monitor_env_invalid(ha_mon, env))
300
+
return 0;
301
+
passed = ha_get_env(ha_mon, env, time_ns);
302
+
ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
303
+
return passed;
304
+
}
305
+
306
+
/*
307
+
* Helper functions for env variables describing clocks with jiffy granularity
308
+
*/
309
+
static inline u64 ha_get_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
310
+
{
311
+
return get_jiffies_64() - READ_ONCE(ha_mon->env_store[env]);
312
+
}
313
+
static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
314
+
{
315
+
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
316
+
}
317
+
static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
318
+
enum envs env, u64 value)
319
+
{
320
+
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
321
+
}
322
+
static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
323
+
enum envs env, u64 time_ns)
324
+
{
325
+
return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());
326
+
327
+
}
328
+
/*
329
+
* ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
330
+
*/
331
+
static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env,
332
+
u64 expire, u64 time_ns)
333
+
{
334
+
u64 passed = 0;
335
+
336
+
if (env < 0 || env >= ENV_MAX_STORED)
337
+
return 0;
338
+
if (ha_monitor_env_invalid(ha_mon, env))
339
+
return 0;
340
+
passed = ha_get_env(ha_mon, env, time_ns);
341
+
ha_set_invariant_jiffy(ha_mon, env, expire - passed);
342
+
return passed;
343
+
}
344
+
345
+
/*
346
+
* Retrieve the last reset time (guard representation) from the invariant
347
+
* representation (expiration).
348
+
* It the caller's responsibility to make sure the storage was actually in the
349
+
* invariant representation (e.g. the current state has an invariant).
350
+
* The provided value must be the same used when starting the invariant.
351
+
*
352
+
* This function's access to the storage is NOT atomic, due to the rarity when
353
+
* this is used. If a monitor allows writes concurrent to this, likely
354
+
* other things are broken and need rethinking the model or additional locking.
355
+
*/
356
+
static inline void ha_inv_to_guard(struct ha_monitor *ha_mon, enum envs env,
357
+
u64 value, u64 time_ns)
358
+
{
359
+
WRITE_ONCE(ha_mon->env_store[env], READ_ONCE(ha_mon->env_store[env]) - value);
360
+
}
361
+
362
+
#if HA_TIMER_TYPE == HA_TIMER_WHEEL
363
+
/*
364
+
* Helper functions to handle the monitor timer.
365
+
* Not all monitors require a timer, in such case the timer will be set up but
366
+
* never armed.
367
+
* Timers start since the last reset of the supplied env or from now if env is
368
+
* not an environment variable. If env was not initialised no timer starts.
369
+
* Timers can expire on any CPU unless the monitor is per-cpu,
370
+
* where we assume every event occurs on the local CPU.
371
+
*/
372
+
static void ha_monitor_timer_callback(struct timer_list *timer)
373
+
{
374
+
struct ha_monitor *ha_mon = container_of(timer, struct ha_monitor, timer);
375
+
376
+
__ha_monitor_timer_callback(ha_mon);
377
+
}
378
+
static inline void ha_setup_timer(struct ha_monitor *ha_mon)
379
+
{
380
+
int mode = 0;
381
+
382
+
if (RV_MON_TYPE == RV_MON_PER_CPU)
383
+
mode |= TIMER_PINNED;
384
+
timer_setup(&ha_mon->timer, ha_monitor_timer_callback, mode);
385
+
}
386
+
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
387
+
u64 expire, u64 time_ns)
388
+
{
389
+
u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
390
+
391
+
mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
392
+
}
393
+
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
394
+
u64 expire, u64 time_ns)
395
+
{
396
+
u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
397
+
398
+
ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
399
+
nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns);
400
+
}
401
+
/*
402
+
* ha_cancel_timer - Cancel the timer
403
+
*
404
+
* Returns:
405
+
* * 1 when the timer was active
406
+
* * 0 when the timer was not active or running a callback
407
+
*/
408
+
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
409
+
{
410
+
return timer_delete(&ha_mon->timer);
411
+
}
412
+
#elif HA_TIMER_TYPE == HA_TIMER_HRTIMER
413
+
/*
414
+
* Helper functions to handle the monitor timer.
415
+
* Not all monitors require a timer, in such case the timer will be set up but
416
+
* never armed.
417
+
* Timers start since the last reset of the supplied env or from now if env is
418
+
* not an environment variable. If env was not initialised no timer starts.
419
+
* Timers can expire on any CPU unless the monitor is per-cpu,
420
+
* where we assume every event occurs on the local CPU.
421
+
*/
422
+
static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer)
423
+
{
424
+
struct ha_monitor *ha_mon = container_of(hrtimer, struct ha_monitor, hrtimer);
425
+
426
+
__ha_monitor_timer_callback(ha_mon);
427
+
return HRTIMER_NORESTART;
428
+
}
429
+
static inline void ha_setup_timer(struct ha_monitor *ha_mon)
430
+
{
431
+
hrtimer_setup(&ha_mon->hrtimer, ha_monitor_timer_callback,
432
+
CLOCK_MONOTONIC, HRTIMER_MODE_REL_HARD);
433
+
}
434
+
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
435
+
u64 expire, u64 time_ns)
436
+
{
437
+
int mode = HRTIMER_MODE_REL_HARD;
438
+
u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
439
+
440
+
if (RV_MON_TYPE == RV_MON_PER_CPU)
441
+
mode |= HRTIMER_MODE_PINNED;
442
+
hrtimer_start(&ha_mon->hrtimer, ns_to_ktime(expire - passed), mode);
443
+
}
444
+
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
445
+
u64 expire, u64 time_ns)
446
+
{
447
+
u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
448
+
449
+
ha_start_timer_ns(ha_mon, ENV_MAX_STORED,
450
+
jiffies_to_nsecs(expire - passed), time_ns);
451
+
}
452
+
/*
453
+
* ha_cancel_timer - Cancel the timer
454
+
*
455
+
* Returns:
456
+
* * 1 when the timer was active
457
+
* * 0 when the timer was not active or running a callback
458
+
*/
459
+
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
460
+
{
461
+
return hrtimer_try_to_cancel(&ha_mon->hrtimer) == 1;
462
+
}
463
+
#else /* HA_TIMER_NONE */
464
+
/*
465
+
* Start function is intentionally not defined, monitors using timers must
466
+
* set HA_TIMER_TYPE to either HA_TIMER_WHEEL or HA_TIMER_HRTIMER.
467
+
*/
468
+
static inline void ha_setup_timer(struct ha_monitor *ha_mon) { }
469
+
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
470
+
{
471
+
return false;
472
+
}
473
+
#endif
474
+
475
+
#endif
+13
kernel/trace/rv/Kconfig
+13
kernel/trace/rv/Kconfig
···
23
23
config RV_LTL_MONITOR
24
24
bool
25
25
26
+
config RV_HA_MONITOR
27
+
bool
28
+
29
+
config HA_MON_EVENTS_IMPLICIT
30
+
select DA_MON_EVENTS_IMPLICIT
31
+
select RV_HA_MONITOR
32
+
bool
33
+
34
+
config HA_MON_EVENTS_ID
35
+
select DA_MON_EVENTS_ID
36
+
select RV_HA_MONITOR
37
+
bool
38
+
26
39
menuconfig RV
27
40
bool "Runtime Verification"
28
41
select TRACING
+63
kernel/trace/rv/rv_trace.h
+63
kernel/trace/rv/rv_trace.h
···
65
65
#include <monitors/opid/opid_trace.h>
66
66
// Add new monitors based on CONFIG_DA_MON_EVENTS_IMPLICIT here
67
67
68
+
#ifdef CONFIG_HA_MON_EVENTS_IMPLICIT
69
+
/* For simplicity this class is marked as DA although relevant only for HA */
70
+
DECLARE_EVENT_CLASS(error_env_da_monitor,
71
+
72
+
TP_PROTO(char *state, char *event, char *env),
73
+
74
+
TP_ARGS(state, event, env),
75
+
76
+
TP_STRUCT__entry(
77
+
__string( state, state )
78
+
__string( event, event )
79
+
__string( env, env )
80
+
),
81
+
82
+
TP_fast_assign(
83
+
__assign_str(state);
84
+
__assign_str(event);
85
+
__assign_str(env);
86
+
),
87
+
88
+
TP_printk("event %s not expected in the state %s with env %s",
89
+
__get_str(event),
90
+
__get_str(state),
91
+
__get_str(env))
92
+
);
93
+
94
+
// Add new monitors based on CONFIG_HA_MON_EVENTS_IMPLICIT here
95
+
96
+
#endif
97
+
68
98
#endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */
69
99
70
100
#ifdef CONFIG_DA_MON_EVENTS_ID
···
157
127
#include <monitors/nrp/nrp_trace.h>
158
128
#include <monitors/sssw/sssw_trace.h>
159
129
// Add new monitors based on CONFIG_DA_MON_EVENTS_ID here
130
+
131
+
#ifdef CONFIG_HA_MON_EVENTS_ID
132
+
/* For simplicity this class is marked as DA although relevant only for HA */
133
+
DECLARE_EVENT_CLASS(error_env_da_monitor_id,
134
+
135
+
TP_PROTO(int id, char *state, char *event, char *env),
136
+
137
+
TP_ARGS(id, state, event, env),
138
+
139
+
TP_STRUCT__entry(
140
+
__field( int, id )
141
+
__string( state, state )
142
+
__string( event, event )
143
+
__string( env, env )
144
+
),
145
+
146
+
TP_fast_assign(
147
+
__assign_str(state);
148
+
__assign_str(event);
149
+
__assign_str(env);
150
+
__entry->id = id;
151
+
),
152
+
153
+
TP_printk("%d: event %s not expected in the state %s with env %s",
154
+
__entry->id,
155
+
__get_str(event),
156
+
__get_str(state),
157
+
__get_str(env))
158
+
);
159
+
160
+
// Add new monitors based on CONFIG_HA_MON_EVENTS_ID here
161
+
162
+
#endif
160
163
161
164
#endif /* CONFIG_DA_MON_EVENTS_ID */
162
165
#ifdef CONFIG_LTL_MON_EVENTS_ID