xref: /linux/include/rv/da_monitor.h (revision 4ff261e725d7376c12e745fdbe8a33cd6dbd5a83)
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_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  */												\
63 static 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  */												\
72 static 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  */												\
80 static 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  */												\
96 static 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 												\
120 static inline bool										\
121 da_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 												\
159 static 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  */												\
199 static struct da_monitor da_mon_##name;								\
200 												\
201 /*												\
202  * da_get_monitor_##name - return the global monitor address					\
203  */												\
204 static 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  */												\
212 static 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  */												\
220 static 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  */												\
229 static 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  */												\
242 static DEFINE_PER_CPU(struct da_monitor, da_mon_##name);					\
243 												\
244 /*												\
245  * da_get_monitor_##name - return current CPU monitor address					\
246  */												\
247 static 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  */												\
255 static 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  */												\
268 static 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  */												\
277 static 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  */												\
291 static 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  */												\
296 static 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 												\
301 static 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  */												\
320 static 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  */												\
337 static 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 												\
354 static 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  */												\
367 static 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  */												\
389 static 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  */												\
414 static 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 												\
436 static 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  */												\
450 static inline void										\
451 da_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  */												\
473 static inline bool										\
474 da_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  */												\
499 static inline bool										\
500 da_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 												\
522 DECLARE_AUTOMATA_HELPERS(name, type)								\
523 DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
524 DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)						\
525 DECLARE_DA_MON_INIT_GLOBAL(name, type)								\
526 DECLARE_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 												\
533 DECLARE_AUTOMATA_HELPERS(name, type)								\
534 DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
535 DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)						\
536 DECLARE_DA_MON_INIT_PER_CPU(name, type)								\
537 DECLARE_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 												\
544 DECLARE_AUTOMATA_HELPERS(name, type)								\
545 DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
546 DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)						\
547 DECLARE_DA_MON_INIT_PER_TASK(name, type)							\
548 DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)
549