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