Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
torvalds
GitHub Repository: torvalds/linux
Path: blob/master/include/rv/da_monitor.h
54332 views
1
/* SPDX-License-Identifier: GPL-2.0 */
2
/*
3
* Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
4
*
5
* Deterministic automata (DA) monitor functions, to be used together
6
* with automata models in C generated by the dot2k tool.
7
*
8
* The dot2k tool is available at tools/verification/dot2k/
9
*
10
* For further information, see:
11
* Documentation/trace/rv/monitor_synthesis.rst
12
*/
13
14
#ifndef _RV_DA_MONITOR_H
15
#define _RV_DA_MONITOR_H
16
17
#include <rv/automata.h>
18
#include <linux/rv.h>
19
#include <linux/stringify.h>
20
#include <linux/bug.h>
21
#include <linux/sched.h>
22
23
static struct rv_monitor rv_this;
24
25
static void react(enum states curr_state, enum events event)
26
{
27
rv_react(&rv_this,
28
"rv: monitor %s does not allow event %s on state %s\n",
29
__stringify(MONITOR_NAME),
30
model_get_event_name(event),
31
model_get_state_name(curr_state));
32
}
33
34
/*
35
* da_monitor_reset - reset a monitor and setting it to init state
36
*/
37
static inline void da_monitor_reset(struct da_monitor *da_mon)
38
{
39
da_mon->monitoring = 0;
40
da_mon->curr_state = model_get_initial_state();
41
}
42
43
/*
44
* da_monitor_start - start monitoring
45
*
46
* The monitor will ignore all events until monitoring is set to true. This
47
* function needs to be called to tell the monitor to start monitoring.
48
*/
49
static inline void da_monitor_start(struct da_monitor *da_mon)
50
{
51
da_mon->curr_state = model_get_initial_state();
52
da_mon->monitoring = 1;
53
}
54
55
/*
56
* da_monitoring - returns true if the monitor is processing events
57
*/
58
static inline bool da_monitoring(struct da_monitor *da_mon)
59
{
60
return da_mon->monitoring;
61
}
62
63
/*
64
* da_monitor_enabled - checks if the monitor is enabled
65
*/
66
static inline bool da_monitor_enabled(void)
67
{
68
/* global switch */
69
if (unlikely(!rv_monitoring_on()))
70
return 0;
71
72
/* monitor enabled */
73
if (unlikely(!rv_this.enabled))
74
return 0;
75
76
return 1;
77
}
78
79
/*
80
* da_monitor_handling_event - checks if the monitor is ready to handle events
81
*/
82
static inline bool da_monitor_handling_event(struct da_monitor *da_mon)
83
{
84
if (!da_monitor_enabled())
85
return 0;
86
87
/* monitor is actually monitoring */
88
if (unlikely(!da_monitoring(da_mon)))
89
return 0;
90
91
return 1;
92
}
93
94
#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
95
/*
96
* Event handler for implicit monitors. Implicit monitor is the one which the
97
* handler does not need to specify which da_monitor to manipulate. Examples
98
* of implicit monitor are the per_cpu or the global ones.
99
*
100
* Retry in case there is a race between getting and setting the next state,
101
* warn and reset the monitor if it runs out of retries. The monitor should be
102
* able to handle various orders.
103
*/
104
105
static inline bool da_event(struct da_monitor *da_mon, enum events event)
106
{
107
enum states curr_state, next_state;
108
109
curr_state = READ_ONCE(da_mon->curr_state);
110
for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) {
111
next_state = model_get_next_state(curr_state, event);
112
if (next_state == INVALID_STATE) {
113
react(curr_state, event);
114
CONCATENATE(trace_error_, MONITOR_NAME)(
115
model_get_state_name(curr_state),
116
model_get_event_name(event));
117
return false;
118
}
119
if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {
120
CONCATENATE(trace_event_, MONITOR_NAME)(
121
model_get_state_name(curr_state),
122
model_get_event_name(event),
123
model_get_state_name(next_state),
124
model_is_final_state(next_state));
125
return true;
126
}
127
}
128
129
trace_rv_retries_error(__stringify(MONITOR_NAME), model_get_event_name(event));
130
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS)
131
" retries reached for event %s, resetting monitor %s",
132
model_get_event_name(event), __stringify(MONITOR_NAME));
133
return false;
134
}
135
136
#elif RV_MON_TYPE == RV_MON_PER_TASK
137
/*
138
* Event handler for per_task monitors.
139
*
140
* Retry in case there is a race between getting and setting the next state,
141
* warn and reset the monitor if it runs out of retries. The monitor should be
142
* able to handle various orders.
143
*/
144
145
static inline bool da_event(struct da_monitor *da_mon, struct task_struct *tsk,
146
enum events event)
147
{
148
enum states curr_state, next_state;
149
150
curr_state = READ_ONCE(da_mon->curr_state);
151
for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) {
152
next_state = model_get_next_state(curr_state, event);
153
if (next_state == INVALID_STATE) {
154
react(curr_state, event);
155
CONCATENATE(trace_error_, MONITOR_NAME)(tsk->pid,
156
model_get_state_name(curr_state),
157
model_get_event_name(event));
158
return false;
159
}
160
if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {
161
CONCATENATE(trace_event_, MONITOR_NAME)(tsk->pid,
162
model_get_state_name(curr_state),
163
model_get_event_name(event),
164
model_get_state_name(next_state),
165
model_is_final_state(next_state));
166
return true;
167
}
168
}
169
170
trace_rv_retries_error(__stringify(MONITOR_NAME), model_get_event_name(event));
171
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS)
172
" retries reached for event %s, resetting monitor %s",
173
model_get_event_name(event), __stringify(MONITOR_NAME));
174
return false;
175
}
176
#endif /* RV_MON_TYPE */
177
178
#if RV_MON_TYPE == RV_MON_GLOBAL
179
/*
180
* Functions to define, init and get a global monitor.
181
*/
182
183
/*
184
* global monitor (a single variable)
185
*/
186
static struct da_monitor da_mon_this;
187
188
/*
189
* da_get_monitor - return the global monitor address
190
*/
191
static struct da_monitor *da_get_monitor(void)
192
{
193
return &da_mon_this;
194
}
195
196
/*
197
* da_monitor_reset_all - reset the single monitor
198
*/
199
static void da_monitor_reset_all(void)
200
{
201
da_monitor_reset(da_get_monitor());
202
}
203
204
/*
205
* da_monitor_init - initialize a monitor
206
*/
207
static inline int da_monitor_init(void)
208
{
209
da_monitor_reset_all();
210
return 0;
211
}
212
213
/*
214
* da_monitor_destroy - destroy the monitor
215
*/
216
static inline void da_monitor_destroy(void) { }
217
218
#elif RV_MON_TYPE == RV_MON_PER_CPU
219
/*
220
* Functions to define, init and get a per-cpu monitor.
221
*/
222
223
/*
224
* per-cpu monitor variables
225
*/
226
static DEFINE_PER_CPU(struct da_monitor, da_mon_this);
227
228
/*
229
* da_get_monitor - return current CPU monitor address
230
*/
231
static struct da_monitor *da_get_monitor(void)
232
{
233
return this_cpu_ptr(&da_mon_this);
234
}
235
236
/*
237
* da_monitor_reset_all - reset all CPUs' monitor
238
*/
239
static void da_monitor_reset_all(void)
240
{
241
struct da_monitor *da_mon;
242
int cpu;
243
244
for_each_cpu(cpu, cpu_online_mask) {
245
da_mon = per_cpu_ptr(&da_mon_this, cpu);
246
da_monitor_reset(da_mon);
247
}
248
}
249
250
/*
251
* da_monitor_init - initialize all CPUs' monitor
252
*/
253
static inline int da_monitor_init(void)
254
{
255
da_monitor_reset_all();
256
return 0;
257
}
258
259
/*
260
* da_monitor_destroy - destroy the monitor
261
*/
262
static inline void da_monitor_destroy(void) { }
263
264
#elif RV_MON_TYPE == RV_MON_PER_TASK
265
/*
266
* Functions to define, init and get a per-task monitor.
267
*/
268
269
/*
270
* The per-task monitor is stored a vector in the task struct. This variable
271
* stores the position on the vector reserved for this monitor.
272
*/
273
static int task_mon_slot = RV_PER_TASK_MONITOR_INIT;
274
275
/*
276
* da_get_monitor - return the monitor in the allocated slot for tsk
277
*/
278
static inline struct da_monitor *da_get_monitor(struct task_struct *tsk)
279
{
280
return &tsk->rv[task_mon_slot].da_mon;
281
}
282
283
static void da_monitor_reset_all(void)
284
{
285
struct task_struct *g, *p;
286
int cpu;
287
288
read_lock(&tasklist_lock);
289
for_each_process_thread(g, p)
290
da_monitor_reset(da_get_monitor(p));
291
for_each_present_cpu(cpu)
292
da_monitor_reset(da_get_monitor(idle_task(cpu)));
293
read_unlock(&tasklist_lock);
294
}
295
296
/*
297
* da_monitor_init - initialize the per-task monitor
298
*
299
* Try to allocate a slot in the task's vector of monitors. If there
300
* is an available slot, use it and reset all task's monitor.
301
*/
302
static int da_monitor_init(void)
303
{
304
int slot;
305
306
slot = rv_get_task_monitor_slot();
307
if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT)
308
return slot;
309
310
task_mon_slot = slot;
311
312
da_monitor_reset_all();
313
return 0;
314
}
315
316
/*
317
* da_monitor_destroy - return the allocated slot
318
*/
319
static inline void da_monitor_destroy(void)
320
{
321
if (task_mon_slot == RV_PER_TASK_MONITOR_INIT) {
322
WARN_ONCE(1, "Disabling a disabled monitor: " __stringify(MONITOR_NAME));
323
return;
324
}
325
rv_put_task_monitor_slot(task_mon_slot);
326
task_mon_slot = RV_PER_TASK_MONITOR_INIT;
327
}
328
#endif /* RV_MON_TYPE */
329
330
#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
331
/*
332
* Handle event for implicit monitor: da_get_monitor() will figure out
333
* the monitor.
334
*/
335
336
static inline void __da_handle_event(struct da_monitor *da_mon,
337
enum events event)
338
{
339
bool retval;
340
341
retval = da_event(da_mon, event);
342
if (!retval)
343
da_monitor_reset(da_mon);
344
}
345
346
/*
347
* da_handle_event - handle an event
348
*/
349
static inline void da_handle_event(enum events event)
350
{
351
struct da_monitor *da_mon = da_get_monitor();
352
bool retval;
353
354
retval = da_monitor_handling_event(da_mon);
355
if (!retval)
356
return;
357
358
__da_handle_event(da_mon, event);
359
}
360
361
/*
362
* da_handle_start_event - start monitoring or handle event
363
*
364
* This function is used to notify the monitor that the system is returning
365
* to the initial state, so the monitor can start monitoring in the next event.
366
* Thus:
367
*
368
* If the monitor already started, handle the event.
369
* If the monitor did not start yet, start the monitor but skip the event.
370
*/
371
static inline bool da_handle_start_event(enum events event)
372
{
373
struct da_monitor *da_mon;
374
375
if (!da_monitor_enabled())
376
return 0;
377
378
da_mon = da_get_monitor();
379
380
if (unlikely(!da_monitoring(da_mon))) {
381
da_monitor_start(da_mon);
382
return 0;
383
}
384
385
__da_handle_event(da_mon, event);
386
387
return 1;
388
}
389
390
/*
391
* da_handle_start_run_event - start monitoring and handle event
392
*
393
* This function is used to notify the monitor that the system is in the
394
* initial state, so the monitor can start monitoring and handling event.
395
*/
396
static inline bool da_handle_start_run_event(enum events event)
397
{
398
struct da_monitor *da_mon;
399
400
if (!da_monitor_enabled())
401
return 0;
402
403
da_mon = da_get_monitor();
404
405
if (unlikely(!da_monitoring(da_mon)))
406
da_monitor_start(da_mon);
407
408
__da_handle_event(da_mon, event);
409
410
return 1;
411
}
412
413
#elif RV_MON_TYPE == RV_MON_PER_TASK
414
/*
415
* Handle event for per task.
416
*/
417
418
static inline void __da_handle_event(struct da_monitor *da_mon,
419
struct task_struct *tsk, enum events event)
420
{
421
bool retval;
422
423
retval = da_event(da_mon, tsk, event);
424
if (!retval)
425
da_monitor_reset(da_mon);
426
}
427
428
/*
429
* da_handle_event - handle an event
430
*/
431
static inline void da_handle_event(struct task_struct *tsk, enum events event)
432
{
433
struct da_monitor *da_mon = da_get_monitor(tsk);
434
bool retval;
435
436
retval = da_monitor_handling_event(da_mon);
437
if (!retval)
438
return;
439
440
__da_handle_event(da_mon, tsk, event);
441
}
442
443
/*
444
* da_handle_start_event - start monitoring or handle event
445
*
446
* This function is used to notify the monitor that the system is returning
447
* to the initial state, so the monitor can start monitoring in the next event.
448
* Thus:
449
*
450
* If the monitor already started, handle the event.
451
* If the monitor did not start yet, start the monitor but skip the event.
452
*/
453
static inline bool da_handle_start_event(struct task_struct *tsk,
454
enum events event)
455
{
456
struct da_monitor *da_mon;
457
458
if (!da_monitor_enabled())
459
return 0;
460
461
da_mon = da_get_monitor(tsk);
462
463
if (unlikely(!da_monitoring(da_mon))) {
464
da_monitor_start(da_mon);
465
return 0;
466
}
467
468
__da_handle_event(da_mon, tsk, event);
469
470
return 1;
471
}
472
473
/*
474
* da_handle_start_run_event - start monitoring and handle event
475
*
476
* This function is used to notify the monitor that the system is in the
477
* initial state, so the monitor can start monitoring and handling event.
478
*/
479
static inline bool da_handle_start_run_event(struct task_struct *tsk,
480
enum events event)
481
{
482
struct da_monitor *da_mon;
483
484
if (!da_monitor_enabled())
485
return 0;
486
487
da_mon = da_get_monitor(tsk);
488
489
if (unlikely(!da_monitoring(da_mon)))
490
da_monitor_start(da_mon);
491
492
__da_handle_event(da_mon, tsk, event);
493
494
return 1;
495
}
496
#endif /* RV_MON_TYPE */
497
498
#endif
499
500