projects/linux·blob master · refs

550 lines · 17.4 KiB

1/* SPDX-License-Identifier: GPL-2.0 */
2/*
3 * Copyright (C) 2025-2028 Red Hat, Inc. Gabriele Monaco <[email protected]>
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
27static inline void ha_monitor_init_env(struct da_monitor *da_mon);
28static inline void ha_monitor_reset_env(struct da_monitor *da_mon);
29static inline void ha_setup_timer(struct ha_monitor *ha_mon);
30static inline bool ha_cancel_timer(struct ha_monitor *ha_mon);
31static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon);
32static bool ha_monitor_handle_constraint(struct da_monitor *da_mon,
33 enum states curr_state,
34 enum events event,
35 enum states next_state,
36 da_id_type id);
37#define da_monitor_event_hook ha_monitor_handle_constraint
38#define da_monitor_init_hook ha_monitor_init_env
39#define da_monitor_reset_hook ha_monitor_reset_env
40#define da_monitor_sync_hook() synchronize_rcu()
41
42#if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK
43/*
44 * Automatic cleanup handlers for per-task HA monitors, only skip if you know
45 * what you are doing (e.g. you want to implement cleanup manually in another
46 * handler doing more things).
47 */
48static void ha_handle_sched_process_exit(void *data, struct task_struct *p,
49 bool group_dead);
50
51#define ha_monitor_enable_hook() \
52 rv_attach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \
53 ha_handle_sched_process_exit)
54#define ha_monitor_disable_hook() \
55 rv_detach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \
56 ha_handle_sched_process_exit)
57#else
58#define ha_monitor_enable_hook() ((void)0)
59#define ha_monitor_disable_hook() ((void)0)
60#endif
61
62#include <rv/da_monitor.h>
63#include <linux/seq_buf.h>
64
65/* This simplifies things since da_mon and ha_mon coexist in the same union */
66_Static_assert(offsetof(struct ha_monitor, da_mon) == 0,
67 "da_mon must be the first element in an ha_mon!");
68#define to_ha_monitor(da) container_of(da, struct ha_monitor, da_mon)
69
70#define ENV_MAX CONCATENATE(env_max_, MONITOR_NAME)
71#define ENV_MAX_STORED CONCATENATE(env_max_stored_, MONITOR_NAME)
72#define envs CONCATENATE(envs_, MONITOR_NAME)
73
74/* Environment storage before being reset */
75#define ENV_INVALID_VALUE U64_MAX
76/* Error with no event occurs only on timeouts */
77#define EVENT_NONE EVENT_MAX
78#define EVENT_NONE_LBL "none"
79#define ENV_BUFFER_SIZE 64
80
81#ifdef CONFIG_RV_REACTORS
82
83/*
84 * ha_react - trigger the reaction after a failed environment constraint
85 *
86 * The transition from curr_state with event is otherwise valid, but the
87 * environment constraint is false. This function can be called also with no
88 * event from a timer (state constraints only).
89 */
90static void ha_react(enum states curr_state, enum events event, char *env)
91{
92 rv_react(&rv_this,
93 "rv: monitor %s does not allow event %s on state %s with env %s\n",
94 __stringify(MONITOR_NAME),
95 event == EVENT_NONE ? EVENT_NONE_LBL : model_get_event_name(event),
96 model_get_state_name(curr_state), env);
97}
98
99#else /* CONFIG_RV_REACTOR */
100
101static void ha_react(enum states curr_state, enum events event, char *env) { }
102#endif
103
104/*
105 * model_get_state_name - return the (string) name of the given state
106 */
107static char *model_get_env_name(enum envs env)
108{
109 if ((env < 0) || (env >= ENV_MAX))
110 return "INVALID";
111
112 return RV_AUTOMATON_NAME.env_names[env];
113}
114
115/*
116 * Monitors requiring a timer implementation need to request it explicitly.
117 */
118#ifndef HA_TIMER_TYPE
119#define HA_TIMER_TYPE HA_TIMER_NONE
120#endif
121
122#if HA_TIMER_TYPE == HA_TIMER_WHEEL
123static void ha_monitor_timer_callback(struct timer_list *timer);
124#elif HA_TIMER_TYPE == HA_TIMER_HRTIMER
125static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer);
126#endif
127
128/*
129 * ktime_get_ns is expensive, since we usually don't require precise accounting
130 * of changes within the same event, cache the current time at the beginning of
131 * the constraint handler and use the cache for subsequent calls.
132 * Monitors without ns clocks automatically skip this.
133 */
134#ifdef HA_CLK_NS
135#define ha_get_ns() ktime_get_ns()
136#else
137#define ha_get_ns() 0
138#endif /* HA_CLK_NS */
139
140static bool ha_mon_destroying;
141
142static int ha_monitor_init(void)
143{
144 int ret;
145
146 WRITE_ONCE(ha_mon_destroying, false);
147 ret = da_monitor_init();
148 if (ret == 0)
149 ha_monitor_enable_hook();
150 return ret;
151}
152
153static void ha_monitor_destroy(void)
154{
155 WRITE_ONCE(ha_mon_destroying, true);
156 ha_monitor_disable_hook();
157 da_monitor_destroy();
158}
159
160/* Should be supplied by the monitor */
161static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env, u64 time_ns);
162static bool ha_verify_constraint(struct ha_monitor *ha_mon,
163 enum states curr_state,
164 enum events event,
165 enum states next_state,
166 u64 time_ns);
167
168/*
169 * ha_monitor_reset_all_stored - reset all environment variables in the monitor
170 */
171static inline void ha_monitor_reset_all_stored(struct ha_monitor *ha_mon)
172{
173 for (int i = 0; i < ENV_MAX_STORED; i++)
174 WRITE_ONCE(ha_mon->env_store[i], ENV_INVALID_VALUE);
175}
176
177/*
178 * ha_monitor_init_env - setup timer and reset all environment
179 *
180 * Called from a hook in the DA start functions, it supplies the da_mon
181 * corresponding to the current ha_mon.
182 * Not all hybrid automata require the timer, still set it for simplicity.
183 */
184static inline void ha_monitor_init_env(struct da_monitor *da_mon)
185{
186 struct ha_monitor *ha_mon = to_ha_monitor(da_mon);
187
188 ha_monitor_reset_all_stored(ha_mon);
189 ha_setup_timer(ha_mon);
190}
191
192/*
193 * ha_monitor_reset_env - stop timer and reset all environment
194 *
195 * Called from a hook in the DA reset functions, it supplies the da_mon
196 * corresponding to the current ha_mon.
197 * Not all hybrid automata require the timer, still clear it for simplicity.
198 * Monitors that never started have their timer uninitialized, do not stop those.
199 */
200static inline void ha_monitor_reset_env(struct da_monitor *da_mon)
201{
202 struct ha_monitor *ha_mon = to_ha_monitor(da_mon);
203
204 if (likely(da_monitoring(da_mon)))
205 ha_cancel_timer(ha_mon);
206}
207
208/*
209 * ha_monitor_env_invalid - return true if env has not been initialised
210 */
211static inline bool ha_monitor_env_invalid(struct ha_monitor *ha_mon, enum envs env)
212{
213 return READ_ONCE(ha_mon->env_store[env]) == ENV_INVALID_VALUE;
214}
215
216static inline void ha_get_env_string(struct seq_buf *s,
217 struct ha_monitor *ha_mon, u64 time_ns)
218{
219 const char *format_str = "%s=%llu";
220
221 for (int i = 0; i < ENV_MAX; i++) {
222 seq_buf_printf(s, format_str, model_get_env_name(i),
223 ha_get_env(ha_mon, i, time_ns));
224 format_str = ",%s=%llu";
225 }
226}
227
228#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
229static inline void ha_trace_error_env(struct ha_monitor *ha_mon,
230 char *curr_state, char *event, char *env,
231 da_id_type id)
232{
233 CONCATENATE(trace_error_env_, MONITOR_NAME)(curr_state, event, env);
234}
235#elif RV_MON_TYPE == RV_MON_PER_TASK || RV_MON_TYPE == RV_MON_PER_OBJ
236
237#define ha_get_target(ha_mon) da_get_target(&ha_mon->da_mon)
238
239static inline void ha_trace_error_env(struct ha_monitor *ha_mon,
240 char *curr_state, char *event, char *env,
241 da_id_type id)
242{
243 CONCATENATE(trace_error_env_, MONITOR_NAME)(id, curr_state, event, env);
244}
245
246#if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK
247static void ha_handle_sched_process_exit(void *data, struct task_struct *p,
248 bool group_dead)
249{
250 struct da_monitor *da_mon = da_get_monitor(p);
251
252 if (likely(da_monitoring(da_mon))) {
253 da_monitor_reset(da_mon);
254 ha_cancel_timer_sync(to_ha_monitor(da_mon));
255 }
256}
257#endif
258
259#endif /* RV_MON_TYPE */
260
261/*
262 * ha_get_monitor - return the current monitor
263 */
264#define ha_get_monitor(...) to_ha_monitor(da_get_monitor(__VA_ARGS__))
265
266/*
267 * ha_monitor_handle_constraint - handle the constraint on the current transition
268 *
269 * If the monitor implementation defines a constraint in the transition from
270 * curr_state to event, react and trace appropriately as well as return false.
271 * This function is called from the hook in the DA event handle function and
272 * triggers a failure in the monitor.
273 */
274static bool ha_monitor_handle_constraint(struct da_monitor *da_mon,
275 enum states curr_state,
276 enum events event,
277 enum states next_state,
278 da_id_type id)
279{
280 struct ha_monitor *ha_mon = to_ha_monitor(da_mon);
281 u64 time_ns = ha_get_ns();
282 DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE);
283
284 if (ha_verify_constraint(ha_mon, curr_state, event, next_state, time_ns))
285 return true;
286
287 ha_get_env_string(&env_string, ha_mon, time_ns);
288 ha_react(curr_state, event, env_string.buffer);
289 ha_trace_error_env(ha_mon,
290 model_get_state_name(curr_state),
291 model_get_event_name(event),
292 env_string.buffer, id);
293 return false;
294}
295
296/*
297 * __ha_monitor_timer_callback - generic callback representation
298 *
299 * This callback runs in an RCU read-side critical section to allow the
300 * destruction sequence to easily synchronize_rcu() with all pending timers
301 * after asynchronously disabling them. The ha_mon_destroying check ensures
302 * any callback entering the RCU section after synchronize_rcu() completes
303 * will see the flag and bail out immediately.
304 */
305static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
306{
307 DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE);
308 enum states curr_state;
309 u64 time_ns;
310
311 guard(rcu)();
312 if (unlikely(READ_ONCE(ha_mon_destroying)))
313 return;
314 /* Ensure consistent curr_state if we race with da_monitor_reset */
315 curr_state = smp_load_acquire(&ha_mon->da_mon.curr_state);
316 if (unlikely(!da_monitor_handling_event(&ha_mon->da_mon)))
317 return;
318
319 time_ns = ha_get_ns();
320 ha_get_env_string(&env_string, ha_mon, time_ns);
321 ha_react(curr_state, EVENT_NONE, env_string.buffer);
322 ha_trace_error_env(ha_mon, model_get_state_name(curr_state),
323 EVENT_NONE_LBL, env_string.buffer,
324 da_get_id(&ha_mon->da_mon));
325
326 da_monitor_reset(&ha_mon->da_mon);
327}
328
329/*
330 * The clock variables store the time epoch - the timestamp when the clock was last reset.
331 * They are read by subtracting the time epoch from the current time.
332 */
333
334/*
335 * Helper functions for env variables describing clocks with ns granularity
336 */
337static inline u64 ha_get_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
338{
339 return time_ns - READ_ONCE(ha_mon->env_store[env]);
340}
341static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
342{
343 WRITE_ONCE(ha_mon->env_store[env], time_ns);
344}
345static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
346 u64 time_ns, u64 expire_ns)
347{
348 return READ_ONCE(ha_mon->env_store[env]) >= time_ns - expire_ns;
349}
350/*
351 * ha_invariant_passed_ns - prepare the invariant and return the time since reset
352 */
353static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
354{
355 if (env < 0 || env >= ENV_MAX_STORED)
356 return 0;
357 if (ha_monitor_env_invalid(ha_mon, env))
358 return 0;
359 return ha_get_env(ha_mon, env, time_ns);
360}
361
362/*
363 * Helper functions for env variables describing clocks with jiffy granularity
364 */
365static inline u64 ha_get_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
366{
367 return get_jiffies_64() - READ_ONCE(ha_mon->env_store[env]);
368}
369static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
370{
371 WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
372}
373static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,
374 u64 time_ns, u64 expire_jiffy)
375{
376 return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64() - expire_jiffy);
377}
378/*
379 * ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
380 */
381static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
382{
383 if (env < 0 || env >= ENV_MAX_STORED)
384 return 0;
385 if (ha_monitor_env_invalid(ha_mon, env))
386 return 0;
387 return ha_get_env(ha_mon, env, time_ns);
388}
389
390/*
391 * Retrieve the last reset time (guard representation) from the invariant
392 * representation (expiration).
393 * It the caller's responsibility to make sure the storage was actually in the
394 * invariant representation (e.g. the current state has an invariant).
395 * The provided value must be the same used when starting the invariant.
396 *
397 * This function's access to the storage is NOT atomic, due to the rarity when
398 * this is used. If a monitor allows writes concurrent to this, likely
399 * other things are broken and need rethinking the model or additional locking.
400 */
401static inline void ha_inv_to_guard(struct ha_monitor *ha_mon, enum envs env,
402 u64 value, u64 time_ns)
403{
404 WRITE_ONCE(ha_mon->env_store[env], READ_ONCE(ha_mon->env_store[env]) - value);
405}
406
407#if HA_TIMER_TYPE == HA_TIMER_WHEEL
408/*
409 * Helper functions to handle the monitor timer.
410 * Not all monitors require a timer, in such case the timer will be set up but
411 * never armed.
412 * Timers start since the last reset of the supplied env or from now if env is
413 * not an environment variable. If env was not initialised no timer starts.
414 * Timers can expire on any CPU unless the monitor is per-cpu,
415 * where we assume every event occurs on the local CPU.
416 */
417static void ha_monitor_timer_callback(struct timer_list *timer)
418{
419 struct ha_monitor *ha_mon = container_of(timer, struct ha_monitor, timer);
420
421 __ha_monitor_timer_callback(ha_mon);
422}
423static inline void ha_setup_timer(struct ha_monitor *ha_mon)
424{
425 int mode = 0;
426
427 if (RV_MON_TYPE == RV_MON_PER_CPU)
428 mode |= TIMER_PINNED;
429 timer_setup(&ha_mon->timer, ha_monitor_timer_callback, mode);
430}
431static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
432 u64 expire, u64 time_ns)
433{
434 u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
435
436 mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
437}
438static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
439 u64 expire, u64 time_ns)
440{
441 u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
442
443 ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
444 nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns);
445}
446/*
447 * ha_cancel_timer - Cancel the timer
448 *
449 * Returns:
450 * * 1 when the timer was active
451 * * 0 when the timer was not active or running a callback
452 */
453static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
454{
455 return timer_delete(&ha_mon->timer);
456}
457static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon)
458{
459 timer_delete_sync(&ha_mon->timer);
460}
461#elif HA_TIMER_TYPE == HA_TIMER_HRTIMER
462/*
463 * Helper functions to handle the monitor timer.
464 * Not all monitors require a timer, in such case the timer will be set up but
465 * never armed.
466 * Timers start since the last reset of the supplied env or from now if env is
467 * not an environment variable. If env was not initialised no timer starts.
468 * Timers can expire on any CPU unless the monitor is per-cpu,
469 * where we assume every event occurs on the local CPU.
470 */
471static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer)
472{
473 struct ha_monitor *ha_mon = container_of(hrtimer, struct ha_monitor, hrtimer);
474
475 __ha_monitor_timer_callback(ha_mon);
476 return HRTIMER_NORESTART;
477}
478static inline void ha_setup_timer(struct ha_monitor *ha_mon)
479{
480 hrtimer_setup(&ha_mon->hrtimer, ha_monitor_timer_callback,
481 CLOCK_MONOTONIC, HRTIMER_MODE_REL_HARD);
482}
483static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
484 u64 expire, u64 time_ns)
485{
486 int mode = HRTIMER_MODE_REL_HARD;
487 u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
488
489 if (RV_MON_TYPE == RV_MON_PER_CPU)
490 mode |= HRTIMER_MODE_PINNED;
491 hrtimer_start(&ha_mon->hrtimer, ns_to_ktime(expire - passed), mode);
492}
493static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
494 u64 expire, u64 time_ns)
495{
496 u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
497
498 ha_start_timer_ns(ha_mon, ENV_MAX_STORED,
499 jiffies_to_nsecs(expire - passed), time_ns);
500}
501/*
502 * ha_cancel_timer - Cancel the timer
503 *
504 * Returns:
505 * * 1 when the timer was active
506 * * 0 when the timer was not active or running a callback
507 */
508static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
509{
510 return hrtimer_try_to_cancel(&ha_mon->hrtimer) == 1;
511}
512static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon)
513{
514 hrtimer_cancel(&ha_mon->hrtimer);
515}
516#else /* HA_TIMER_NONE */
517/*
518 * Start function is intentionally not defined, monitors using timers must
519 * set HA_TIMER_TYPE to either HA_TIMER_WHEEL or HA_TIMER_HRTIMER.
520 */
521static inline void ha_setup_timer(struct ha_monitor *ha_mon) { }
522static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
523{
524 return false;
525}
526static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) { }
527#endif
528
529#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
530#ifdef RV_MON_OPS_INIT
531#undef RV_MON_OPS_INIT
532#endif
533
534#if RV_MON_TYPE == RV_MON_PER_TASK
535#define RV_MON_OPS_INIT() { \
536 .rv_this = &rv_this, \
537 .is_per_task = true, \
538 .task_slot = &task_mon_slot, \
539 .task_reset = da_reset, \
540}
541#else
542#define RV_MON_OPS_INIT() { \
543 .rv_this = &rv_this, \
544 .monitor_init = ha_monitor_init, \
545 .monitor_destroy = ha_monitor_destroy, \
546}
547#endif /* RV_MON_TYPE */
548#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */
549
550#endif