/* 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
*/
#include <rv/automata.h>
#include <linux/rv.h>
#include <linux/bug.h>
#include <linux/sched.h>
#ifdef CONFIG_RV_REACTORS
#define DECLARE_RV_REACTING_HELPERS(name, type) \
static void cond_react_## name(type curr_state, type event) \
{ \
if (!rv_reacting_on() || !rv_## name.react) \
return ; \
rv_## name.react("rv: monitor %s does not allow event %s on state %s\n" , \
#name , \
model_get_event_name_## name(event), \
model_get_state_name_## name(curr_state)); \
}
#else /* CONFIG_RV_REACTOR */
#define DECLARE_RV_REACTING_HELPERS(name, type) \
static void cond_react_## name(type curr_state, type event) \
{ \
return ; \
}
#endif
/*
* 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 \
*/ \
static inline void 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 . \
*/ \
static inline void 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 \
*/ \
static inline bool da_monitoring_## name(struct da_monitor *da_mon) \
{ \
return da_mon->monitoring; \
} \
\
/* \
* da_monitor_enabled_ # # name - checks if the monitor is enabled \
*/ \
static inline bool 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 \
*/ \
static inline bool 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) \
\
static inline bool \
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)); \
return false ; \
} \
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)); \
return true ; \
} \
} \
\
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 ); \
return false ; \
} \
/*
* 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) \
\
static inline bool 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)); \
return false ; \
} \
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)); \
return true ; \
} \
} \
\
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 ); \
return false ; \
}
/*
* Functions to define , init and get a global monitor .
*/
#define DECLARE_DA_MON_INIT_GLOBAL(name, type) \
\
/* \
* global monitor ( a single variable ) \
*/ \
static struct da_monitor da_mon_## name; \
\
/* \
* da_get_monitor_ # # name - return the global monitor address \
*/ \
static struct da_monitor *da_get_monitor_## name(void ) \
{ \
return &da_mon_## name; \
} \
\
/* \
* da_monitor_reset_all_ # # name - reset the single monitor \
*/ \
static void da_monitor_reset_all_## name(void ) \
{ \
da_monitor_reset_## name(da_get_monitor_## name()); \
} \
\
/* \
* da_monitor_init_ # # name - initialize a monitor \
*/ \
static inline int da_monitor_init_## name(void ) \
{ \
da_monitor_reset_all_## name(); \
return 0 ; \
} \
\
/* \
* da_monitor_destroy_ # # name - destroy the monitor \
*/ \
static inline void da_monitor_destroy_## name(void ) \
{ \
return ; \
}
/*
* Functions to define , init and get a per - cpu monitor .
*/
#define DECLARE_DA_MON_INIT_PER_CPU(name, type) \
\
/* \
* per - cpu monitor variables \
*/ \
static DEFINE_PER_CPU(struct da_monitor, da_mon_## name); \
\
/* \
* da_get_monitor_ # # name - return current CPU monitor address \
*/ \
static struct da_monitor *da_get_monitor_## name(void ) \
{ \
return this_cpu_ptr(&da_mon_## name); \
} \
\
/* \
* da_monitor_reset_all_ # # name - reset all CPUs ' monitor \
*/ \
static void da_monitor_reset_all_## name(void ) \
{ \
struct da_monitor *da_mon; \
int cpu; \
for_each_cpu(cpu, cpu_online_mask) { \
da_mon = per_cpu_ptr(&da_mon_## name, cpu); \
da_monitor_reset_## name(da_mon); \
} \
} \
\
/* \
* da_monitor_init_ # # name - initialize all CPUs ' monitor \
*/ \
static inline int da_monitor_init_## name(void ) \
{ \
da_monitor_reset_all_## name(); \
return 0 ; \
} \
\
/* \
* da_monitor_destroy_ # # name - destroy the monitor \
*/ \
static inline void da_monitor_destroy_## name(void ) \
{ \
return ; \
}
/*
* Functions to define , init and get a per - task monitor .
*/
#define DECLARE_DA_MON_INIT_PER_TASK(name, type) \
\
/* \
* The per - task monitor is stored a vector in the task struct . This variable \
* stores the position on the vector reserved for this monitor . \
*/ \
static int task_mon_slot_## name = RV_PER_TASK_MONITOR_INIT; \
\
/* \
* da_get_monitor_ # # name - return the monitor in the allocated slot for tsk \
*/ \
static inline struct da_monitor *da_get_monitor_## name(struct task_struct *tsk) \
{ \
return &tsk->rv[task_mon_slot_## name].da_mon; \
} \
\
static void da_monitor_reset_all_## name(void ) \
{ \
struct task_struct *g, *p; \
int cpu; \
\
read_lock(&tasklist_lock); \
for_each_process_thread(g, p) \
da_monitor_reset_## name(da_get_monitor_## name(p)); \
for_each_present_cpu(cpu) \
da_monitor_reset_## name(da_get_monitor_## name(idle_task(cpu))); \
read_unlock(&tasklist_lock); \
} \
\
/* \
* da_monitor_init_ # # name - initialize the per - task monitor \
* \
* Try to allocate a slot in the task ' s vector of monitors . If there \
* is an available slot , use it and reset all task ' s monitor . \
*/ \
static int da_monitor_init_## name(void ) \
{ \
int slot; \
\
slot = rv_get_task_monitor_slot(); \
if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT) \
return slot; \
\
task_mon_slot_## name = slot; \
\
da_monitor_reset_all_## name(); \
return 0 ; \
} \
\
/* \
* da_monitor_destroy_ # # name - return the allocated slot \
*/ \
static inline void da_monitor_destroy_## name(void ) \
{ \
if (task_mon_slot_## name == RV_PER_TASK_MONITOR_INIT) { \
WARN_ONCE(1 , "Disabling a disabled monitor: " #name ); \
return ; \
} \
rv_put_task_monitor_slot(task_mon_slot_## name); \
task_mon_slot_## name = RV_PER_TASK_MONITOR_INIT; \
return ; \
}
/*
* Handle event for implicit monitor : da_get_monitor_ # # name ( ) will figure out
* the monitor .
*/
#define DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type) \
\
static inline void __da_handle_event_## name(struct da_monitor *da_mon, \
enum events_## name event) \
{ \
bool retval; \
\
retval = da_event_## name(da_mon, event); \
if (!retval) \
da_monitor_reset_## name(da_mon); \
} \
\
/* \
* da_handle_event_ # # name - handle an event \
*/ \
static inline void da_handle_event_## name(enum events_## name event) \
{ \
struct da_monitor *da_mon = da_get_monitor_## name(); \
bool retval; \
\
retval = da_monitor_handling_event_## name(da_mon); \
if (!retval) \
return ; \
\
__da_handle_event_## name(da_mon, event); \
} \
\
/* \
* da_handle_start_event_ # # name - start monitoring or handle event \
* \
* This function is used to notify the monitor that the system is returning \
* to the initial state , so the monitor can start monitoring in the next event . \
* Thus : \
* \
* If the monitor already started , handle the event . \
* If the monitor did not start yet , start the monitor but skip the event . \
*/ \
static inline bool da_handle_start_event_## name(enum events_## name event) \
{ \
struct da_monitor *da_mon; \
\
if (!da_monitor_enabled_## name()) \
return 0 ; \
\
da_mon = da_get_monitor_## name(); \
\
if (unlikely(!da_monitoring_## name(da_mon))) { \
da_monitor_start_## name(da_mon); \
return 0 ; \
} \
\
__da_handle_event_## name(da_mon, event); \
\
return 1 ; \
} \
\
/* \
* da_handle_start_run_event_ # # name - start monitoring and handle event \
* \
* This function is used to notify the monitor that the system is in the \
* initial state , so the monitor can start monitoring and handling event . \
*/ \
static inline bool da_handle_start_run_event_## name(enum events_## name event) \
{ \
struct da_monitor *da_mon; \
\
if (!da_monitor_enabled_## name()) \
return 0 ; \
\
da_mon = da_get_monitor_## name(); \
\
if (unlikely(!da_monitoring_## name(da_mon))) \
da_monitor_start_## name(da_mon); \
\
__da_handle_event_## name(da_mon, event); \
\
return 1 ; \
}
/*
* Handle event for per task .
*/
#define DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type) \
\
static inline void \
__da_handle_event_## name(struct da_monitor *da_mon, struct task_struct *tsk, \
enum events_## name event) \
{ \
bool retval; \
\
retval = da_event_## name(da_mon, tsk, event); \
if (!retval) \
da_monitor_reset_## name(da_mon); \
} \
\
/* \
* da_handle_event_ # # name - handle an event \
*/ \
static inline void \
da_handle_event_## name(struct task_struct *tsk, enum events_## name event) \
{ \
struct da_monitor *da_mon = da_get_monitor_## name(tsk); \
bool retval; \
\
retval = da_monitor_handling_event_## name(da_mon); \
if (!retval) \
return ; \
\
__da_handle_event_## name(da_mon, tsk, event); \
} \
\
/* \
* da_handle_start_event_ # # name - start monitoring or handle event \
* \
* This function is used to notify the monitor that the system is returning \
* to the initial state , so the monitor can start monitoring in the next event . \
* Thus : \
* \
* If the monitor already started , handle the event . \
* If the monitor did not start yet , start the monitor but skip the event . \
*/ \
static inline bool \
da_handle_start_event_## name(struct task_struct *tsk, enum events_## name event) \
{ \
struct da_monitor *da_mon; \
\
if (!da_monitor_enabled_## name()) \
return 0 ; \
\
da_mon = da_get_monitor_## name(tsk); \
\
if (unlikely(!da_monitoring_## name(da_mon))) { \
da_monitor_start_## name(da_mon); \
return 0 ; \
} \
\
__da_handle_event_## name(da_mon, tsk, event); \
\
return 1 ; \
} \
\
/* \
* da_handle_start_run_event_ # # name - start monitoring and handle event \
* \
* This function is used to notify the monitor that the system is in the \
* initial state , so the monitor can start monitoring and handling event . \
*/ \
static inline bool \
da_handle_start_run_event_## name(struct task_struct *tsk, enum events_## name event) \
{ \
struct da_monitor *da_mon; \
\
if (!da_monitor_enabled_## name()) \
return 0 ; \
\
da_mon = da_get_monitor_## name(tsk); \
\
if (unlikely(!da_monitoring_## name(da_mon))) \
da_monitor_start_## name(da_mon); \
\
__da_handle_event_## name(da_mon, tsk, event); \
\
return 1 ; \
}
/*
* Entry point for the global monitor .
*/
#define DECLARE_DA_MON_GLOBAL(name, type) \
\
DECLARE_AUTOMATA_HELPERS(name, type) \
DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
DECLARE_DA_MON_INIT_GLOBAL(name, type) \
DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
/*
* Entry point for the per - cpu monitor .
*/
#define DECLARE_DA_MON_PER_CPU(name, type) \
\
DECLARE_AUTOMATA_HELPERS(name, type) \
DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
DECLARE_DA_MON_INIT_PER_CPU(name, type) \
DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
/*
* Entry point for the per - task monitor .
*/
#define DECLARE_DA_MON_PER_TASK(name, type) \
\
DECLARE_AUTOMATA_HELPERS(name, type) \
DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \
DECLARE_DA_MON_INIT_PER_TASK(name, type) \
DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)
Messung V0.5 in Prozent C=93 H=99 G=95
¤ 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.0.14Bemerkung:
(vorverarbeitet am 2026-09-29)
¤
*© Formatika GbR, Deutschland