File Index
Files and directories
Sign in
FILE

da_monitor.h

File preview with syntax highlighting.

linux-6.19.14/include/rv/da_monitor.h C
  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)
~/ Read-only file preview.