/* SPDX-License-Identifier: GPL-2.0 */ /* * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> * * Deterministic automata (DA) monitor functions, to be used together * with automata models in C generated by the dot2k tool. * * The dot2k tool is available at tools/verification/dot2k/ * * For further information, see: * Documentation/trace/rv/da_monitor_synthesis.rst
*/
/* * Generic helpers for all types of deterministic automata monitors.
*/ #define DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
\
DECLARE_RV_REACTING_HELPERS(name, type) \
\ /* \ * da_monitor_reset_##name - reset a monitor and setting it to init state \
*/ staticinlinevoid da_monitor_reset_##name(struct da_monitor *da_mon) \
{ \
da_mon->monitoring = 0; \
da_mon->curr_state = model_get_initial_state_##name(); \
} \
\ /* \ * da_monitor_start_##name - start monitoring \ * \ * The monitor will ignore all events until monitoring is set to true. This \ * function needs to be called to tell the monitor to start monitoring. \
*/ staticinlinevoid da_monitor_start_##name(struct da_monitor *da_mon) \
{ \
da_mon->curr_state = model_get_initial_state_##name(); \
da_mon->monitoring = 1; \
} \
\ /* \ * da_monitoring_##name - returns true if the monitor is processing events \
*/ staticinlinebool da_monitoring_##name(struct da_monitor *da_mon) \
{ \ return da_mon->monitoring; \
} \
\ /* \ * da_monitor_enabled_##name - checks if the monitor is enabled \
*/ staticinlinebool da_monitor_enabled_##name(void) \
{ \ /* global switch */ \ if (unlikely(!rv_monitoring_on())) \ return 0; \
\ /* monitor enabled */ \ if (unlikely(!rv_##name.enabled)) \ return 0; \
\ return 1; \
} \
\ /* \ * da_monitor_handling_event_##name - checks if the monitor is ready to handle events \
*/ staticinlinebool da_monitor_handling_event_##name(struct da_monitor *da_mon) \
{ \
\ if (!da_monitor_enabled_##name()) \ return 0; \
\ /* monitor is actually monitoring */ \ if (unlikely(!da_monitoring_##name(da_mon))) \ return 0; \
\ return 1; \
}
/* * Event handler for implicit monitors. Implicit monitor is the one which the * handler does not need to specify which da_monitor to manipulate. Examples * of implicit monitor are the per_cpu or the global ones. * * Retry in case there is a race between getting and setting the next state, * warn and reset the monitor if it runs out of retries. The monitor should be * able to handle various orders.
*/ #define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
\ staticinlinebool \
da_event_##name(struct da_monitor *da_mon, enum events_##name event) \
{ \ enum states_##name curr_state, next_state; \
\
curr_state = READ_ONCE(da_mon->curr_state); \ for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \
next_state = model_get_next_state_##name(curr_state, event); \ if (next_state == INVALID_STATE) { \
cond_react_##name(curr_state, event); \
trace_error_##name(model_get_state_name_##name(curr_state), \
model_get_event_name_##name(event)); \ returnfalse; \
} \ if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \
trace_event_##name(model_get_state_name_##name(curr_state), \
model_get_event_name_##name(event), \
model_get_state_name_##name(next_state), \
model_is_final_state_##name(next_state)); \ returntrue; \
} \
} \
\
trace_rv_retries_error(#name, model_get_event_name_##name(event)); \
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \ " retries reached for event %s, resetting monitor %s", \
model_get_event_name_##name(event), #name); \ returnfalse; \
} \
/* * Event handler for per_task monitors. * * Retry in case there is a race between getting and setting the next state, * warn and reset the monitor if it runs out of retries. The monitor should be * able to handle various orders.
*/ #define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \
\ staticinlinebool da_event_##name(struct da_monitor *da_mon, struct task_struct *tsk, \ enum events_##name event) \
{ \ enum states_##name curr_state, next_state; \
\
curr_state = READ_ONCE(da_mon->curr_state); \ for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \
next_state = model_get_next_state_##name(curr_state, event); \ if (next_state == INVALID_STATE) { \
cond_react_##name(curr_state, event); \
trace_error_##name(tsk->pid, \
model_get_state_name_##name(curr_state), \
model_get_event_name_##name(event)); \ returnfalse; \
} \ if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \
trace_event_##name(tsk->pid, \
model_get_state_name_##name(curr_state), \
model_get_event_name_##name(event), \
model_get_state_name_##name(next_state), \
model_is_final_state_##name(next_state)); \ returntrue; \
} \
} \
\
trace_rv_retries_error(#name, model_get_event_name_##name(event)); \
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \ " retries reached for event %s, resetting monitor %s", \
model_get_event_name_##name(event), #name); \ returnfalse; \
}
/* * Functions to define, init and get a global monitor.
*/ #define DECLARE_DA_MON_INIT_GLOBAL(name, type) \
\ /* \ * global monitor (a single variable) \
*/ staticstruct da_monitor da_mon_##name; \
\ /* \ * da_get_monitor_##name - return the global monitor address \
*/ staticstruct da_monitor *da_get_monitor_##name(void) \
{ \ return &da_mon_##name; \
} \
\ /* \ * da_monitor_reset_all_##name - reset the single monitor \
*/ staticvoid da_monitor_reset_all_##name(void) \
{ \
da_monitor_reset_##name(da_get_monitor_##name()); \
} \
\ /* \ * da_monitor_init_##name - initialize a monitor \
*/ staticinlineint da_monitor_init_##name(void) \
{ \
da_monitor_reset_all_##name(); \ return 0; \
} \
\ /* \ * da_monitor_destroy_##name - destroy the monitor \
*/ staticinlinevoid da_monitor_destroy_##name(void) \
{ \ return; \
}
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.