xref: /linux/include/rv/da_monitor.h (revision 0b1b4a3d8ebec3c42231c306d4b9a5153d047674)
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 												\
24 static 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  */												\
36 static 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  */												\
48 static 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  */												\
57 static 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  */												\
65 static 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  */												\
81 static 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 												\
105 static inline bool										\
106 da_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 												\
144 static 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  */												\
184 static struct da_monitor da_mon_##name;								\
185 												\
186 /*												\
187  * da_get_monitor_##name - return the global monitor address					\
188  */												\
189 static 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  */												\
197 static 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  */												\
205 static 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  */												\
214 static 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  */												\
227 static DEFINE_PER_CPU(struct da_monitor, da_mon_##name);					\
228 												\
229 /*												\
230  * da_get_monitor_##name - return current CPU monitor address					\
231  */												\
232 static 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  */												\
240 static 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  */												\
253 static 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  */												\
262 static 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  */												\
276 static 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  */												\
281 static 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 												\
286 static 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  */												\
305 static 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  */												\
322 static 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 												\
339 static 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  */												\
352 static 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  */												\
374 static 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  */												\
399 static 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 												\
421 static 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  */												\
435 static inline void										\
436 da_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  */												\
458 static inline bool										\
459 da_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  */												\
484 static inline bool										\
485 da_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 												\
507 DECLARE_AUTOMATA_HELPERS(name, type)								\
508 DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
509 DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)						\
510 DECLARE_DA_MON_INIT_GLOBAL(name, type)								\
511 DECLARE_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 												\
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_PER_CPU(name, type)								\
522 DECLARE_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 												\
529 DECLARE_AUTOMATA_HELPERS(name, type)								\
530 DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
531 DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)						\
532 DECLARE_DA_MON_INIT_PER_TASK(name, type)							\
533 DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)
534