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