xref: /linux/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c (revision 55ee4b931a7ffedc886175d265dd6e6d08fd4151)
1 // SPDX-License-Identifier: GPL-2.0
2 #include <linux/ftrace.h>
3 #include <linux/tracepoint.h>
4 #include <linux/kernel.h>
5 #include <linux/module.h>
6 #include <linux/init.h>
7 #include <linux/rv.h>
8 #include <rv/instrumentation.h>
9 
10 #define MODULE_NAME "ha_percpu"
11 
12 /*
13  * XXX: include required tracepoint headers, e.g.,
14  * #include <trace/events/sched.h>
15  */
16 #include <rv_trace.h>
17 
18 /*
19  * This is the self-generated part of the monitor. Generally, there is no need
20  * to touch this section.
21  */
22 #define RV_MON_TYPE RV_MON_PER_CPU
23 /* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
24 #define HA_TIMER_TYPE HA_TIMER_HRTIMER
25 #include "ha_percpu.h"
26 #include <rv/ha_monitor.h>
27 
28 /*
29  * This is the instrumentation part of the monitor.
30  *
31  * This is the section where manual work is required. Here the kernel events
32  * are translated into model's event.
33  *
34  */
35 #define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */
36 
37 #define FOO_NS /* XXX: what is FOO_NS? */
38 
39 static inline u64 bar_ns(struct ha_monitor *ha_mon)
40 {
41 	return /* XXX: what is bar_ns(ha_mon)? */;
42 }
43 
44 static u64 foo_ns = /* XXX: default value */;
45 module_param(foo_ns, ullong, 0644);
46 
47 /*
48  * These functions define how to read and reset the environment variable.
49  *
50  * Common environment variables like ns-based and jiffy-based clocks have
51  * pre-define getters and resetters you can use. The parser can infer the type
52  * of the environment variable if you supply a measure unit in the constraint.
53  * If you define your own functions, make sure to add appropriate memory
54  * barriers if required.
55  * Some environment variables don't require a storage as they read a system
56  * state (e.g. preemption count). Those variables are never reset, so we don't
57  * define a reset function on monitors only relying on this type of variables.
58  */
59 static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
60 {
61 	if (env == clk_ha_percpu)
62 		return ha_get_clk_ns(ha_mon, env, time_ns);
63 	else if (env == env1_ha_percpu)
64 		return /* XXX: how do I read env1? */
65 	else if (env == env2_ha_percpu)
66 		return /* XXX: how do I read env2? */
67 	return ENV_INVALID_VALUE;
68 }
69 
70 static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
71 {
72 	if (env == clk_ha_percpu)
73 		ha_reset_clk_ns(ha_mon, env, time_ns);
74 }
75 
76 /*
77  * These functions are used to validate state transitions.
78  *
79  * They are generated by parsing the model, there is usually no need to change them.
80  * If the monitor requires a timer, there are functions responsible to arm it when
81  * the next state has a constraint, cancel it in any other case and to check
82  * that it didn't expire before the callback run. Transitions to the same state
83  * without a reset never affect timers.
84  */
85 static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
86 					enum states curr_state, enum events event,
87 					enum states next_state, u64 time_ns)
88 {
89 	if (curr_state == S0_ha_percpu)
90 		return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, bar_ns(ha_mon));
91 	else if (curr_state == S2_ha_percpu)
92 		return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, BAR_NS(ha_mon));
93 	return true;
94 }
95 
96 static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
97 				    enum states curr_state, enum events event,
98 				    enum states next_state, u64 time_ns)
99 {
100 	bool res = true;
101 
102 	if (curr_state == S0_ha_percpu && event == event0_ha_percpu)
103 		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
104 	else if (curr_state == S0_ha_percpu && event == event1_ha_percpu)
105 		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
106 	else if (curr_state == S1_ha_percpu && event == event0_ha_percpu)
107 		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
108 	else if (curr_state == S1_ha_percpu && event == event2_ha_percpu) {
109 		res = ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 0ull;
110 		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
111 	} else if (curr_state == S2_ha_percpu && event == event1_ha_percpu)
112 		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
113 		      ha_get_env(ha_mon, clk_ha_percpu, time_ns) < foo_ns;
114 	else if (curr_state == S3_ha_percpu && event == event0_ha_percpu)
115 		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
116 		      (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < FOO_NS &&
117 		      ha_get_env(ha_mon, env2_ha_percpu, time_ns) == 0ull);
118 	else if (curr_state == S3_ha_percpu && event == event1_ha_percpu) {
119 		res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
120 		      (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < 5000ull &&
121 		      ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 1ull);
122 		ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
123 	}
124 	return res;
125 }
126 
127 static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
128 				       enum states curr_state, enum events event,
129 				       enum states next_state, u64 time_ns)
130 {
131 	if (next_state == curr_state && event != event0_ha_percpu)
132 		return;
133 	if (next_state == S0_ha_percpu)
134 		ha_start_timer_ns(ha_mon, clk_ha_percpu, bar_ns(ha_mon), time_ns);
135 	else if (next_state == S2_ha_percpu)
136 		ha_start_timer_ns(ha_mon, clk_ha_percpu, BAR_NS(ha_mon), time_ns);
137 	else if (curr_state == S0_ha_percpu)
138 		ha_cancel_timer(ha_mon);
139 	else if (curr_state == S2_ha_percpu)
140 		ha_cancel_timer(ha_mon);
141 }
142 
143 static bool ha_verify_constraint(struct ha_monitor *ha_mon,
144 				 enum states curr_state, enum events event,
145 				 enum states next_state, u64 time_ns)
146 {
147 	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
148 		return false;
149 
150 	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
151 		return false;
152 
153 	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
154 
155 	return true;
156 }
157 
158 static void handle_event0(void *data, /* XXX: fill header */)
159 {
160 	/* XXX: validate that this event always leads to the initial state */
161 	da_handle_start_event(event0_ha_percpu);
162 }
163 
164 static void handle_event1(void *data, /* XXX: fill header */)
165 {
166 	da_handle_event(event1_ha_percpu);
167 }
168 
169 static void handle_event2(void *data, /* XXX: fill header */)
170 {
171 	da_handle_event(event2_ha_percpu);
172 }
173 
174 static int enable_ha_percpu(void)
175 {
176 	int retval;
177 
178 	retval = ha_monitor_init();
179 	if (retval)
180 		return retval;
181 
182 	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
183 	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
184 	rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);
185 
186 	return 0;
187 }
188 
189 static void disable_ha_percpu(void)
190 {
191 	rv_this.enabled = 0;
192 
193 	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
194 	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
195 	rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);
196 
197 	ha_monitor_destroy();
198 }
199 
200 /*
201  * This is the monitor register section.
202  */
203 static struct rv_monitor rv_this = {
204 	.name = "ha_percpu",
205 	.description = "auto-generated",
206 	.enable = enable_ha_percpu,
207 	.disable = disable_ha_percpu,
208 	.reset = da_monitor_reset_all,
209 	.enabled = 0,
210 };
211 
212 static int __init register_ha_percpu(void)
213 {
214 	return rv_register_monitor(&rv_this, NULL);
215 }
216 
217 static void __exit unregister_ha_percpu(void)
218 {
219 	rv_unregister_monitor(&rv_this);
220 }
221 
222 module_init(register_ha_percpu);
223 module_exit(unregister_ha_percpu);
224 
225 MODULE_LICENSE("GPL");
226 MODULE_AUTHOR("rvgen: auto-generated");
227 MODULE_DESCRIPTION("ha_percpu: auto-generated");
228