Previous changes refactored the da_monitor header file to avoid using macros, however empty macros (e.g. DECLARE_DA_FUNCTION) were left to ease review with diff tools. Most macros also get the argument type which doesn't really have a purpose since states have their own enum and the storage in struct da_monitor is fixed to unsigned int. Remove empty and no longer required macros and substitute the type parameter with the appropriate enum. Additionally break long line and adjust the format overall. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20251126104241.291258-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
499 lines
12 KiB
C
499 lines
12 KiB
C
/* 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
|
|
*/
|
|
|
|
#ifndef _RV_DA_MONITOR_H
|
|
#define _RV_DA_MONITOR_H
|
|
|
|
#include <rv/automata.h>
|
|
#include <linux/rv.h>
|
|
#include <linux/stringify.h>
|
|
#include <linux/bug.h>
|
|
#include <linux/sched.h>
|
|
|
|
static struct rv_monitor rv_this;
|
|
|
|
static void react(enum states curr_state, enum events event)
|
|
{
|
|
rv_react(&rv_this,
|
|
"rv: monitor %s does not allow event %s on state %s\n",
|
|
__stringify(MONITOR_NAME),
|
|
model_get_event_name(event),
|
|
model_get_state_name(curr_state));
|
|
}
|
|
|
|
/*
|
|
* da_monitor_reset - reset a monitor and setting it to init state
|
|
*/
|
|
static inline void da_monitor_reset(struct da_monitor *da_mon)
|
|
{
|
|
da_mon->monitoring = 0;
|
|
da_mon->curr_state = model_get_initial_state();
|
|
}
|
|
|
|
/*
|
|
* da_monitor_start - 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(struct da_monitor *da_mon)
|
|
{
|
|
da_mon->curr_state = model_get_initial_state();
|
|
da_mon->monitoring = 1;
|
|
}
|
|
|
|
/*
|
|
* da_monitoring - returns true if the monitor is processing events
|
|
*/
|
|
static inline bool da_monitoring(struct da_monitor *da_mon)
|
|
{
|
|
return da_mon->monitoring;
|
|
}
|
|
|
|
/*
|
|
* da_monitor_enabled - checks if the monitor is enabled
|
|
*/
|
|
static inline bool da_monitor_enabled(void)
|
|
{
|
|
/* global switch */
|
|
if (unlikely(!rv_monitoring_on()))
|
|
return 0;
|
|
|
|
/* monitor enabled */
|
|
if (unlikely(!rv_this.enabled))
|
|
return 0;
|
|
|
|
return 1;
|
|
}
|
|
|
|
/*
|
|
* da_monitor_handling_event - checks if the monitor is ready to handle events
|
|
*/
|
|
static inline bool da_monitor_handling_event(struct da_monitor *da_mon)
|
|
{
|
|
if (!da_monitor_enabled())
|
|
return 0;
|
|
|
|
/* monitor is actually monitoring */
|
|
if (unlikely(!da_monitoring(da_mon)))
|
|
return 0;
|
|
|
|
return 1;
|
|
}
|
|
|
|
#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
|
|
/*
|
|
* 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.
|
|
*/
|
|
|
|
static inline bool da_event(struct da_monitor *da_mon, enum events event)
|
|
{
|
|
enum states 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(curr_state, event);
|
|
if (next_state == INVALID_STATE) {
|
|
react(curr_state, event);
|
|
CONCATENATE(trace_error_, MONITOR_NAME)(
|
|
model_get_state_name(curr_state),
|
|
model_get_event_name(event));
|
|
return false;
|
|
}
|
|
if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {
|
|
CONCATENATE(trace_event_, MONITOR_NAME)(
|
|
model_get_state_name(curr_state),
|
|
model_get_event_name(event),
|
|
model_get_state_name(next_state),
|
|
model_is_final_state(next_state));
|
|
return true;
|
|
}
|
|
}
|
|
|
|
trace_rv_retries_error(__stringify(MONITOR_NAME), model_get_event_name(event));
|
|
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS)
|
|
" retries reached for event %s, resetting monitor %s",
|
|
model_get_event_name(event), __stringify(MONITOR_NAME));
|
|
return false;
|
|
}
|
|
|
|
#elif RV_MON_TYPE == RV_MON_PER_TASK
|
|
/*
|
|
* 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.
|
|
*/
|
|
|
|
static inline bool da_event(struct da_monitor *da_mon, struct task_struct *tsk,
|
|
enum events event)
|
|
{
|
|
enum states 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(curr_state, event);
|
|
if (next_state == INVALID_STATE) {
|
|
react(curr_state, event);
|
|
CONCATENATE(trace_error_, MONITOR_NAME)(tsk->pid,
|
|
model_get_state_name(curr_state),
|
|
model_get_event_name(event));
|
|
return false;
|
|
}
|
|
if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {
|
|
CONCATENATE(trace_event_, MONITOR_NAME)(tsk->pid,
|
|
model_get_state_name(curr_state),
|
|
model_get_event_name(event),
|
|
model_get_state_name(next_state),
|
|
model_is_final_state(next_state));
|
|
return true;
|
|
}
|
|
}
|
|
|
|
trace_rv_retries_error(__stringify(MONITOR_NAME), model_get_event_name(event));
|
|
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS)
|
|
" retries reached for event %s, resetting monitor %s",
|
|
model_get_event_name(event), __stringify(MONITOR_NAME));
|
|
return false;
|
|
}
|
|
#endif /* RV_MON_TYPE */
|
|
|
|
#if RV_MON_TYPE == RV_MON_GLOBAL
|
|
/*
|
|
* Functions to define, init and get a global monitor.
|
|
*/
|
|
|
|
/*
|
|
* global monitor (a single variable)
|
|
*/
|
|
static struct da_monitor da_mon_this;
|
|
|
|
/*
|
|
* da_get_monitor - return the global monitor address
|
|
*/
|
|
static struct da_monitor *da_get_monitor(void)
|
|
{
|
|
return &da_mon_this;
|
|
}
|
|
|
|
/*
|
|
* da_monitor_reset_all - reset the single monitor
|
|
*/
|
|
static void da_monitor_reset_all(void)
|
|
{
|
|
da_monitor_reset(da_get_monitor());
|
|
}
|
|
|
|
/*
|
|
* da_monitor_init - initialize a monitor
|
|
*/
|
|
static inline int da_monitor_init(void)
|
|
{
|
|
da_monitor_reset_all();
|
|
return 0;
|
|
}
|
|
|
|
/*
|
|
* da_monitor_destroy - destroy the monitor
|
|
*/
|
|
static inline void da_monitor_destroy(void) { }
|
|
|
|
#elif RV_MON_TYPE == RV_MON_PER_CPU
|
|
/*
|
|
* Functions to define, init and get a per-cpu monitor.
|
|
*/
|
|
|
|
/*
|
|
* per-cpu monitor variables
|
|
*/
|
|
static DEFINE_PER_CPU(struct da_monitor, da_mon_this);
|
|
|
|
/*
|
|
* da_get_monitor - return current CPU monitor address
|
|
*/
|
|
static struct da_monitor *da_get_monitor(void)
|
|
{
|
|
return this_cpu_ptr(&da_mon_this);
|
|
}
|
|
|
|
/*
|
|
* da_monitor_reset_all - reset all CPUs' monitor
|
|
*/
|
|
static void da_monitor_reset_all(void)
|
|
{
|
|
struct da_monitor *da_mon;
|
|
int cpu;
|
|
|
|
for_each_cpu(cpu, cpu_online_mask) {
|
|
da_mon = per_cpu_ptr(&da_mon_this, cpu);
|
|
da_monitor_reset(da_mon);
|
|
}
|
|
}
|
|
|
|
/*
|
|
* da_monitor_init - initialize all CPUs' monitor
|
|
*/
|
|
static inline int da_monitor_init(void)
|
|
{
|
|
da_monitor_reset_all();
|
|
return 0;
|
|
}
|
|
|
|
/*
|
|
* da_monitor_destroy - destroy the monitor
|
|
*/
|
|
static inline void da_monitor_destroy(void) { }
|
|
|
|
#elif RV_MON_TYPE == RV_MON_PER_TASK
|
|
/*
|
|
* Functions to define, init and get a per-task monitor.
|
|
*/
|
|
|
|
/*
|
|
* 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 = RV_PER_TASK_MONITOR_INIT;
|
|
|
|
/*
|
|
* da_get_monitor - return the monitor in the allocated slot for tsk
|
|
*/
|
|
static inline struct da_monitor *da_get_monitor(struct task_struct *tsk)
|
|
{
|
|
return &tsk->rv[task_mon_slot].da_mon;
|
|
}
|
|
|
|
static void da_monitor_reset_all(void)
|
|
{
|
|
struct task_struct *g, *p;
|
|
int cpu;
|
|
|
|
read_lock(&tasklist_lock);
|
|
for_each_process_thread(g, p)
|
|
da_monitor_reset(da_get_monitor(p));
|
|
for_each_present_cpu(cpu)
|
|
da_monitor_reset(da_get_monitor(idle_task(cpu)));
|
|
read_unlock(&tasklist_lock);
|
|
}
|
|
|
|
/*
|
|
* da_monitor_init - 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(void)
|
|
{
|
|
int slot;
|
|
|
|
slot = rv_get_task_monitor_slot();
|
|
if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT)
|
|
return slot;
|
|
|
|
task_mon_slot = slot;
|
|
|
|
da_monitor_reset_all();
|
|
return 0;
|
|
}
|
|
|
|
/*
|
|
* da_monitor_destroy - return the allocated slot
|
|
*/
|
|
static inline void da_monitor_destroy(void)
|
|
{
|
|
if (task_mon_slot == RV_PER_TASK_MONITOR_INIT) {
|
|
WARN_ONCE(1, "Disabling a disabled monitor: " __stringify(MONITOR_NAME));
|
|
return;
|
|
}
|
|
rv_put_task_monitor_slot(task_mon_slot);
|
|
task_mon_slot = RV_PER_TASK_MONITOR_INIT;
|
|
}
|
|
#endif /* RV_MON_TYPE */
|
|
|
|
#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
|
|
/*
|
|
* Handle event for implicit monitor: da_get_monitor() will figure out
|
|
* the monitor.
|
|
*/
|
|
|
|
static inline void __da_handle_event(struct da_monitor *da_mon,
|
|
enum events event)
|
|
{
|
|
bool retval;
|
|
|
|
retval = da_event(da_mon, event);
|
|
if (!retval)
|
|
da_monitor_reset(da_mon);
|
|
}
|
|
|
|
/*
|
|
* da_handle_event - handle an event
|
|
*/
|
|
static inline void da_handle_event(enum events event)
|
|
{
|
|
struct da_monitor *da_mon = da_get_monitor();
|
|
bool retval;
|
|
|
|
retval = da_monitor_handling_event(da_mon);
|
|
if (!retval)
|
|
return;
|
|
|
|
__da_handle_event(da_mon, event);
|
|
}
|
|
|
|
/*
|
|
* da_handle_start_event - 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(enum events event)
|
|
{
|
|
struct da_monitor *da_mon;
|
|
|
|
if (!da_monitor_enabled())
|
|
return 0;
|
|
|
|
da_mon = da_get_monitor();
|
|
|
|
if (unlikely(!da_monitoring(da_mon))) {
|
|
da_monitor_start(da_mon);
|
|
return 0;
|
|
}
|
|
|
|
__da_handle_event(da_mon, event);
|
|
|
|
return 1;
|
|
}
|
|
|
|
/*
|
|
* da_handle_start_run_event - 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(enum events event)
|
|
{
|
|
struct da_monitor *da_mon;
|
|
|
|
if (!da_monitor_enabled())
|
|
return 0;
|
|
|
|
da_mon = da_get_monitor();
|
|
|
|
if (unlikely(!da_monitoring(da_mon)))
|
|
da_monitor_start(da_mon);
|
|
|
|
__da_handle_event(da_mon, event);
|
|
|
|
return 1;
|
|
}
|
|
|
|
#elif RV_MON_TYPE == RV_MON_PER_TASK
|
|
/*
|
|
* Handle event for per task.
|
|
*/
|
|
|
|
static inline void __da_handle_event(struct da_monitor *da_mon,
|
|
struct task_struct *tsk, enum events event)
|
|
{
|
|
bool retval;
|
|
|
|
retval = da_event(da_mon, tsk, event);
|
|
if (!retval)
|
|
da_monitor_reset(da_mon);
|
|
}
|
|
|
|
/*
|
|
* da_handle_event - handle an event
|
|
*/
|
|
static inline void da_handle_event(struct task_struct *tsk, enum events event)
|
|
{
|
|
struct da_monitor *da_mon = da_get_monitor(tsk);
|
|
bool retval;
|
|
|
|
retval = da_monitor_handling_event(da_mon);
|
|
if (!retval)
|
|
return;
|
|
|
|
__da_handle_event(da_mon, tsk, event);
|
|
}
|
|
|
|
/*
|
|
* da_handle_start_event - 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(struct task_struct *tsk,
|
|
enum events event)
|
|
{
|
|
struct da_monitor *da_mon;
|
|
|
|
if (!da_monitor_enabled())
|
|
return 0;
|
|
|
|
da_mon = da_get_monitor(tsk);
|
|
|
|
if (unlikely(!da_monitoring(da_mon))) {
|
|
da_monitor_start(da_mon);
|
|
return 0;
|
|
}
|
|
|
|
__da_handle_event(da_mon, tsk, event);
|
|
|
|
return 1;
|
|
}
|
|
|
|
/*
|
|
* da_handle_start_run_event - 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(struct task_struct *tsk,
|
|
enum events event)
|
|
{
|
|
struct da_monitor *da_mon;
|
|
|
|
if (!da_monitor_enabled())
|
|
return 0;
|
|
|
|
da_mon = da_get_monitor(tsk);
|
|
|
|
if (unlikely(!da_monitoring(da_mon)))
|
|
da_monitor_start(da_mon);
|
|
|
|
__da_handle_event(da_mon, tsk, event);
|
|
|
|
return 1;
|
|
}
|
|
#endif /* RV_MON_TYPE */
|
|
|
|
#endif
|