tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c

// SPDX-License-Identifier: GPL-2.0
#include <linux/ftrace.h>
#include <linux/tracepoint.h>
#include <linux/kernel.h>
#include <linux/module.h>
#include <linux/init.h>
#include <linux/rv.h>
#include <rv/instrumentation.h>

#define MODULE_NAME "ha_percpu"

/*
 * XXX: include required tracepoint headers, e.g.,
 * #include <trace/events/sched.h>
 */
#include <rv_trace.h>

/*
 * This is the self-generated part of the monitor. Generally, there is no need
 * to touch this section.
 */
#define RV_MON_TYPE RV_MON_PER_CPU
/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
#define HA_TIMER_TYPE HA_TIMER_HRTIMER
#include "ha_percpu.h"
#include <rv/ha_monitor.h>

/*
 * This is the instrumentation part of the monitor.
 *
 * This is the section where manual work is required. Here the kernel events
 * are translated into model's event.
 *
 */
#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */

#define FOO_NS /* XXX: what is FOO_NS? */

static inline u64 bar_ns(struct ha_monitor *ha_mon)
{
	return /* XXX: what is bar_ns(ha_mon)? */;
}

static u64 foo_ns = /* XXX: default value */;
module_param(foo_ns, ullong, 0644);

/*
 * These functions define how to read and reset the environment variable.
 *
 * Common environment variables like ns-based and jiffy-based clocks have
 * pre-define getters and resetters you can use. The parser can infer the type
 * of the environment variable if you supply a measure unit in the constraint.
 * If you define your own functions, make sure to add appropriate memory
 * barriers if required.
 * Some environment variables don't require a storage as they read a system
 * state (e.g. preemption count). Those variables are never reset, so we don't
 * define a reset function on monitors only relying on this type of variables.
 */
static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
{
	if (env == clk_ha_percpu)
		return ha_get_clk_ns(ha_mon, env, time_ns);
	else if (env == env1_ha_percpu)
		return /* XXX: how do I read env1? */
	else if (env == env2_ha_percpu)
		return /* XXX: how do I read env2? */
	return ENV_INVALID_VALUE;
}

static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
{
	if (env == clk_ha_percpu)
		ha_reset_clk_ns(ha_mon, env, time_ns);
}

/*
 * These functions are used to validate state transitions.
 *
 * They are generated by parsing the model, there is usually no need to change them.
 * If the monitor requires a timer, there are functions responsible to arm it when
 * the next state has a constraint, cancel it in any other case and to check
 * that it didn't expire before the callback run. Transitions to the same state
 * without a reset never affect timers.
 */
static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
					enum states curr_state, enum events event,
					enum states next_state, u64 time_ns)
{
	if (curr_state == S0_ha_percpu)
		return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, bar_ns(ha_mon));
	else if (curr_state == S2_ha_percpu)
		return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, BAR_NS(ha_mon));
	return true;
}

static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
				    enum states curr_state, enum events event,
				    enum states next_state, u64 time_ns)
{
	bool res = true;

	if (curr_state == S0_ha_percpu && event == event0_ha_percpu)
		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
	else if (curr_state == S0_ha_percpu && event == event1_ha_percpu)
		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
	else if (curr_state == S1_ha_percpu && event == event0_ha_percpu)
		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
	else if (curr_state == S1_ha_percpu && event == event2_ha_percpu) {
		res = ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 0ull;
		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
	} else if (curr_state == S2_ha_percpu && event == event1_ha_percpu)
		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
		      ha_get_env(ha_mon, clk_ha_percpu, time_ns) < foo_ns;
	else if (curr_state == S3_ha_percpu && event == event0_ha_percpu)
		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
		      (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < FOO_NS &&
		      ha_get_env(ha_mon, env2_ha_percpu, time_ns) == 0ull);
	else if (curr_state == S3_ha_percpu && event == event1_ha_percpu) {
		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
		      (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < 5000ull &&
		      ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 1ull);
		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
	}
	return res;
}

static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
				       enum states curr_state, enum events event,
				       enum states next_state, u64 time_ns)
{
	if (next_state == curr_state && event != event0_ha_percpu)
		return;
	if (next_state == S0_ha_percpu)
		ha_start_timer_ns(ha_mon, clk_ha_percpu, bar_ns(ha_mon), time_ns);
	else if (next_state == S2_ha_percpu)
		ha_start_timer_ns(ha_mon, clk_ha_percpu, BAR_NS(ha_mon), time_ns);
	else if (curr_state == S0_ha_percpu)
		ha_cancel_timer(ha_mon);
	else if (curr_state == S2_ha_percpu)
		ha_cancel_timer(ha_mon);
}

static bool ha_verify_constraint(struct ha_monitor *ha_mon,
				 enum states curr_state, enum events event,
				 enum states next_state, u64 time_ns)
{
	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
		return false;

	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
		return false;

	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);

	return true;
}

static void handle_event0(void *data, /* XXX: fill header */)
{
	/* XXX: validate that this event always leads to the initial state */
	da_handle_start_event(event0_ha_percpu);
}

static void handle_event1(void *data, /* XXX: fill header */)
{
	da_handle_event(event1_ha_percpu);
}

static void handle_event2(void *data, /* XXX: fill header */)
{
	da_handle_event(event2_ha_percpu);
}

static int enable_ha_percpu(void)
{
	int retval;

	retval = ha_monitor_init();
	if (retval)
		return retval;

	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);

	return 0;
}

static void disable_ha_percpu(void)
{
	rv_this.enabled = 0;

	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);

	ha_monitor_destroy();
}

/*
 * This is the monitor register section.
 */
static struct rv_monitor rv_this = {
	.name = "ha_percpu",
	.description = "auto-generated",
	.enable = enable_ha_percpu,
	.disable = disable_ha_percpu,
	.reset = da_monitor_reset_all,
	.enabled = 0,
};

static int __init register_ha_percpu(void)
{
	return rv_register_monitor(&rv_this, NULL);
}

static void __exit unregister_ha_percpu(void)
{
	rv_unregister_monitor(&rv_this);
}

module_init(register_ha_percpu);
module_exit(unregister_ha_percpu);

MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("ha_percpu: auto-generated");