Linux kernel mirror (for testing)
git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
tjh.dev
kernel
os
linux
1/* SPDX-License-Identifier: GPL-2.0 */
2/*
3 * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
4 *
5 * Deterministic automata (DA) monitor functions, to be used together
6 * with automata models in C generated by the dot2k tool.
7 *
8 * The dot2k tool is available at tools/verification/dot2k/
9 *
10 * For further information, see:
11 * Documentation/trace/rv/da_monitor_synthesis.rst
12 */
13
14#include <rv/automata.h>
15#include <linux/rv.h>
16#include <linux/bug.h>
17#include <linux/sched.h>
18
19#ifdef CONFIG_RV_REACTORS
20
21#define DECLARE_RV_REACTING_HELPERS(name, type) \
22static void cond_react_##name(type curr_state, type event) \
23{ \
24 if (!rv_reacting_on() || !rv_##name.react) \
25 return; \
26 rv_##name.react("rv: monitor %s does not allow event %s on state %s\n", \
27 #name, \
28 model_get_event_name_##name(event), \
29 model_get_state_name_##name(curr_state)); \
30}
31
32#else /* CONFIG_RV_REACTOR */
33
34#define DECLARE_RV_REACTING_HELPERS(name, type) \
35static void cond_react_##name(type curr_state, type event) \
36{ \
37 return; \
38}
39#endif
40
41/*
42 * Generic helpers for all types of deterministic automata monitors.
43 */
44#define DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
45 \
46DECLARE_RV_REACTING_HELPERS(name, type) \
47 \
48/* \
49 * da_monitor_reset_##name - reset a monitor and setting it to init state \
50 */ \
51static inline void da_monitor_reset_##name(struct da_monitor *da_mon) \
52{ \
53 da_mon->monitoring = 0; \
54 da_mon->curr_state = model_get_initial_state_##name(); \
55} \
56 \
57/* \
58 * da_monitor_start_##name - start monitoring \
59 * \
60 * The monitor will ignore all events until monitoring is set to true. This \
61 * function needs to be called to tell the monitor to start monitoring. \
62 */ \
63static inline void da_monitor_start_##name(struct da_monitor *da_mon) \
64{ \
65 da_mon->curr_state = model_get_initial_state_##name(); \
66 da_mon->monitoring = 1; \
67} \
68 \
69/* \
70 * da_monitoring_##name - returns true if the monitor is processing events \
71 */ \
72static inline bool da_monitoring_##name(struct da_monitor *da_mon) \
73{ \
74 return da_mon->monitoring; \
75} \
76 \
77/* \
78 * da_monitor_enabled_##name - checks if the monitor is enabled \
79 */ \
80static inline bool da_monitor_enabled_##name(void) \
81{ \
82 /* global switch */ \
83 if (unlikely(!rv_monitoring_on())) \
84 return 0; \
85 \
86 /* monitor enabled */ \
87 if (unlikely(!rv_##name.enabled)) \
88 return 0; \
89 \
90 return 1; \
91} \
92 \
93/* \
94 * da_monitor_handling_event_##name - checks if the monitor is ready to handle events \
95 */ \
96static inline bool da_monitor_handling_event_##name(struct da_monitor *da_mon) \
97{ \
98 \
99 if (!da_monitor_enabled_##name()) \
100 return 0; \
101 \
102 /* monitor is actually monitoring */ \
103 if (unlikely(!da_monitoring_##name(da_mon))) \
104 return 0; \
105 \
106 return 1; \
107}
108
109/*
110 * Event handler for implicit monitors. Implicit monitor is the one which the
111 * handler does not need to specify which da_monitor to manipulate. Examples
112 * of implicit monitor are the per_cpu or the global ones.
113 *
114 * Retry in case there is a race between getting and setting the next state,
115 * warn and reset the monitor if it runs out of retries. The monitor should be
116 * able to handle various orders.
117 */
118#define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
119 \
120static inline bool \
121da_event_##name(struct da_monitor *da_mon, enum events_##name event) \
122{ \
123 enum states_##name curr_state, next_state; \
124 \
125 curr_state = READ_ONCE(da_mon->curr_state); \
126 for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \
127 next_state = model_get_next_state_##name(curr_state, event); \
128 if (next_state == INVALID_STATE) { \
129 cond_react_##name(curr_state, event); \
130 trace_error_##name(model_get_state_name_##name(curr_state), \
131 model_get_event_name_##name(event)); \
132 return false; \
133 } \
134 if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \
135 trace_event_##name(model_get_state_name_##name(curr_state), \
136 model_get_event_name_##name(event), \
137 model_get_state_name_##name(next_state), \
138 model_is_final_state_##name(next_state)); \
139 return true; \
140 } \
141 } \
142 \
143 trace_rv_retries_error(#name, model_get_event_name_##name(event)); \
144 pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \
145 " retries reached for event %s, resetting monitor %s", \
146 model_get_event_name_##name(event), #name); \
147 return false; \
148} \
149
150/*
151 * Event handler for per_task monitors.
152 *
153 * Retry in case there is a race between getting and setting the next state,
154 * warn and reset the monitor if it runs out of retries. The monitor should be
155 * able to handle various orders.
156 */
157#define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \
158 \
159static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct *tsk, \
160 enum events_##name event) \
161{ \
162 enum states_##name curr_state, next_state; \
163 \
164 curr_state = READ_ONCE(da_mon->curr_state); \
165 for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \
166 next_state = model_get_next_state_##name(curr_state, event); \
167 if (next_state == INVALID_STATE) { \
168 cond_react_##name(curr_state, event); \
169 trace_error_##name(tsk->pid, \
170 model_get_state_name_##name(curr_state), \
171 model_get_event_name_##name(event)); \
172 return false; \
173 } \
174 if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \
175 trace_event_##name(tsk->pid, \
176 model_get_state_name_##name(curr_state), \
177 model_get_event_name_##name(event), \
178 model_get_state_name_##name(next_state), \
179 model_is_final_state_##name(next_state)); \
180 return true; \
181 } \
182 } \
183 \
184 trace_rv_retries_error(#name, model_get_event_name_##name(event)); \
185 pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \
186 " retries reached for event %s, resetting monitor %s", \
187 model_get_event_name_##name(event), #name); \
188 return false; \
189}
190
191/*
192 * Functions to define, init and get a global monitor.
193 */
194#define DECLARE_DA_MON_INIT_GLOBAL(name, type) \
195 \
196/* \
197 * global monitor (a single variable) \
198 */ \
199static struct da_monitor da_mon_##name; \
200 \
201/* \
202 * da_get_monitor_##name - return the global monitor address \
203 */ \
204static struct da_monitor *da_get_monitor_##name(void) \
205{ \
206 return &da_mon_##name; \
207} \
208 \
209/* \
210 * da_monitor_reset_all_##name - reset the single monitor \
211 */ \
212static void da_monitor_reset_all_##name(void) \
213{ \
214 da_monitor_reset_##name(da_get_monitor_##name()); \
215} \
216 \
217/* \
218 * da_monitor_init_##name - initialize a monitor \
219 */ \
220static inline int da_monitor_init_##name(void) \
221{ \
222 da_monitor_reset_all_##name(); \
223 return 0; \
224} \
225 \
226/* \
227 * da_monitor_destroy_##name - destroy the monitor \
228 */ \
229static inline void da_monitor_destroy_##name(void) \
230{ \
231 return; \
232}
233
234/*
235 * Functions to define, init and get a per-cpu monitor.
236 */
237#define DECLARE_DA_MON_INIT_PER_CPU(name, type) \
238 \
239/* \
240 * per-cpu monitor variables \
241 */ \
242static DEFINE_PER_CPU(struct da_monitor, da_mon_##name); \
243 \
244/* \
245 * da_get_monitor_##name - return current CPU monitor address \
246 */ \
247static struct da_monitor *da_get_monitor_##name(void) \
248{ \
249 return this_cpu_ptr(&da_mon_##name); \
250} \
251 \
252/* \
253 * da_monitor_reset_all_##name - reset all CPUs' monitor \
254 */ \
255static void da_monitor_reset_all_##name(void) \
256{ \
257 struct da_monitor *da_mon; \
258 int cpu; \
259 for_each_cpu(cpu, cpu_online_mask) { \
260 da_mon = per_cpu_ptr(&da_mon_##name, cpu); \
261 da_monitor_reset_##name(da_mon); \
262 } \
263} \
264 \
265/* \
266 * da_monitor_init_##name - initialize all CPUs' monitor \
267 */ \
268static inline int da_monitor_init_##name(void) \
269{ \
270 da_monitor_reset_all_##name(); \
271 return 0; \
272} \
273 \
274/* \
275 * da_monitor_destroy_##name - destroy the monitor \
276 */ \
277static inline void da_monitor_destroy_##name(void) \
278{ \
279 return; \
280}
281
282/*
283 * Functions to define, init and get a per-task monitor.
284 */
285#define DECLARE_DA_MON_INIT_PER_TASK(name, type) \
286 \
287/* \
288 * The per-task monitor is stored a vector in the task struct. This variable \
289 * stores the position on the vector reserved for this monitor. \
290 */ \
291static int task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT; \
292 \
293/* \
294 * da_get_monitor_##name - return the monitor in the allocated slot for tsk \
295 */ \
296static inline struct da_monitor *da_get_monitor_##name(struct task_struct *tsk) \
297{ \
298 return &tsk->rv[task_mon_slot_##name].da_mon; \
299} \
300 \
301static void da_monitor_reset_all_##name(void) \
302{ \
303 struct task_struct *g, *p; \
304 int cpu; \
305 \
306 read_lock(&tasklist_lock); \
307 for_each_process_thread(g, p) \
308 da_monitor_reset_##name(da_get_monitor_##name(p)); \
309 for_each_present_cpu(cpu) \
310 da_monitor_reset_##name(da_get_monitor_##name(idle_task(cpu))); \
311 read_unlock(&tasklist_lock); \
312} \
313 \
314/* \
315 * da_monitor_init_##name - initialize the per-task monitor \
316 * \
317 * Try to allocate a slot in the task's vector of monitors. If there \
318 * is an available slot, use it and reset all task's monitor. \
319 */ \
320static int da_monitor_init_##name(void) \
321{ \
322 int slot; \
323 \
324 slot = rv_get_task_monitor_slot(); \
325 if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT) \
326 return slot; \
327 \
328 task_mon_slot_##name = slot; \
329 \
330 da_monitor_reset_all_##name(); \
331 return 0; \
332} \
333 \
334/* \
335 * da_monitor_destroy_##name - return the allocated slot \
336 */ \
337static inline void da_monitor_destroy_##name(void) \
338{ \
339 if (task_mon_slot_##name == RV_PER_TASK_MONITOR_INIT) { \
340 WARN_ONCE(1, "Disabling a disabled monitor: " #name); \
341 return; \
342 } \
343 rv_put_task_monitor_slot(task_mon_slot_##name); \
344 task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT; \
345 return; \
346}
347
348/*
349 * Handle event for implicit monitor: da_get_monitor_##name() will figure out
350 * the monitor.
351 */
352#define DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type) \
353 \
354static inline void __da_handle_event_##name(struct da_monitor *da_mon, \
355 enum events_##name event) \
356{ \
357 bool retval; \
358 \
359 retval = da_event_##name(da_mon, event); \
360 if (!retval) \
361 da_monitor_reset_##name(da_mon); \
362} \
363 \
364/* \
365 * da_handle_event_##name - handle an event \
366 */ \
367static inline void da_handle_event_##name(enum events_##name event) \
368{ \
369 struct da_monitor *da_mon = da_get_monitor_##name(); \
370 bool retval; \
371 \
372 retval = da_monitor_handling_event_##name(da_mon); \
373 if (!retval) \
374 return; \
375 \
376 __da_handle_event_##name(da_mon, event); \
377} \
378 \
379/* \
380 * da_handle_start_event_##name - start monitoring or handle event \
381 * \
382 * This function is used to notify the monitor that the system is returning \
383 * to the initial state, so the monitor can start monitoring in the next event. \
384 * Thus: \
385 * \
386 * If the monitor already started, handle the event. \
387 * If the monitor did not start yet, start the monitor but skip the event. \
388 */ \
389static inline bool da_handle_start_event_##name(enum events_##name event) \
390{ \
391 struct da_monitor *da_mon; \
392 \
393 if (!da_monitor_enabled_##name()) \
394 return 0; \
395 \
396 da_mon = da_get_monitor_##name(); \
397 \
398 if (unlikely(!da_monitoring_##name(da_mon))) { \
399 da_monitor_start_##name(da_mon); \
400 return 0; \
401 } \
402 \
403 __da_handle_event_##name(da_mon, event); \
404 \
405 return 1; \
406} \
407 \
408/* \
409 * da_handle_start_run_event_##name - start monitoring and handle event \
410 * \
411 * This function is used to notify the monitor that the system is in the \
412 * initial state, so the monitor can start monitoring and handling event. \
413 */ \
414static inline bool da_handle_start_run_event_##name(enum events_##name event) \
415{ \
416 struct da_monitor *da_mon; \
417 \
418 if (!da_monitor_enabled_##name()) \
419 return 0; \
420 \
421 da_mon = da_get_monitor_##name(); \
422 \
423 if (unlikely(!da_monitoring_##name(da_mon))) \
424 da_monitor_start_##name(da_mon); \
425 \
426 __da_handle_event_##name(da_mon, event); \
427 \
428 return 1; \
429}
430
431/*
432 * Handle event for per task.
433 */
434#define DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type) \
435 \
436static inline void \
437__da_handle_event_##name(struct da_monitor *da_mon, struct task_struct *tsk, \
438 enum events_##name event) \
439{ \
440 bool retval; \
441 \
442 retval = da_event_##name(da_mon, tsk, event); \
443 if (!retval) \
444 da_monitor_reset_##name(da_mon); \
445} \
446 \
447/* \
448 * da_handle_event_##name - handle an event \
449 */ \
450static inline void \
451da_handle_event_##name(struct task_struct *tsk, enum events_##name event) \
452{ \
453 struct da_monitor *da_mon = da_get_monitor_##name(tsk); \
454 bool retval; \
455 \
456 retval = da_monitor_handling_event_##name(da_mon); \
457 if (!retval) \
458 return; \
459 \
460 __da_handle_event_##name(da_mon, tsk, event); \
461} \
462 \
463/* \
464 * da_handle_start_event_##name - start monitoring or handle event \
465 * \
466 * This function is used to notify the monitor that the system is returning \
467 * to the initial state, so the monitor can start monitoring in the next event. \
468 * Thus: \
469 * \
470 * If the monitor already started, handle the event. \
471 * If the monitor did not start yet, start the monitor but skip the event. \
472 */ \
473static inline bool \
474da_handle_start_event_##name(struct task_struct *tsk, enum events_##name event) \
475{ \
476 struct da_monitor *da_mon; \
477 \
478 if (!da_monitor_enabled_##name()) \
479 return 0; \
480 \
481 da_mon = da_get_monitor_##name(tsk); \
482 \
483 if (unlikely(!da_monitoring_##name(da_mon))) { \
484 da_monitor_start_##name(da_mon); \
485 return 0; \
486 } \
487 \
488 __da_handle_event_##name(da_mon, tsk, event); \
489 \
490 return 1; \
491} \
492 \
493/* \
494 * da_handle_start_run_event_##name - start monitoring and handle event \
495 * \
496 * This function is used to notify the monitor that the system is in the \
497 * initial state, so the monitor can start monitoring and handling event. \
498 */ \
499static inline bool \
500da_handle_start_run_event_##name(struct task_struct *tsk, enum events_##name event) \
501{ \
502 struct da_monitor *da_mon; \
503 \
504 if (!da_monitor_enabled_##name()) \
505 return 0; \
506 \
507 da_mon = da_get_monitor_##name(tsk); \
508 \
509 if (unlikely(!da_monitoring_##name(da_mon))) \
510 da_monitor_start_##name(da_mon); \
511 \
512 __da_handle_event_##name(da_mon, tsk, event); \
513 \
514 return 1; \
515}
516
517/*
518 * Entry point for the global monitor.
519 */
520#define DECLARE_DA_MON_GLOBAL(name, type) \
521 \
522DECLARE_AUTOMATA_HELPERS(name, type) \
523DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
524DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
525DECLARE_DA_MON_INIT_GLOBAL(name, type) \
526DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
527
528/*
529 * Entry point for the per-cpu monitor.
530 */
531#define DECLARE_DA_MON_PER_CPU(name, type) \
532 \
533DECLARE_AUTOMATA_HELPERS(name, type) \
534DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
535DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
536DECLARE_DA_MON_INIT_PER_CPU(name, type) \
537DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
538
539/*
540 * Entry point for the per-task monitor.
541 */
542#define DECLARE_DA_MON_PER_TASK(name, type) \
543 \
544DECLARE_AUTOMATA_HELPERS(name, type) \
545DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
546DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \
547DECLARE_DA_MON_INIT_PER_TASK(name, type) \
548DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)