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