Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
torvalds
GitHub Repository: torvalds/linux
Path: blob/master/include/rv/da_monitor.h
26278 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/da_monitor_synthesis.rst
12
*/
13
14
#include <rv/automata.h>
15
#include <linux/rv.h>
16
#include <linux/bug.h>
17
#include <linux/sched.h>
18
19
#ifdef CONFIG_RV_REACTORS
20
21
#define DECLARE_RV_REACTING_HELPERS(name, type) \
22
static void cond_react_##name(type curr_state, type event) \
23
{ \
24
if (!rv_reacting_on() || !rv_##name.react) \
25
return; \
26
rv_##name.react("rv: monitor %s does not allow event %s on state %s\n", \
27
#name, \
28
model_get_event_name_##name(event), \
29
model_get_state_name_##name(curr_state)); \
30
}
31
32
#else /* CONFIG_RV_REACTOR */
33
34
#define DECLARE_RV_REACTING_HELPERS(name, type) \
35
static void cond_react_##name(type curr_state, type event) \
36
{ \
37
return; \
38
}
39
#endif
40
41
/*
42
* Generic helpers for all types of deterministic automata monitors.
43
*/
44
#define DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
45
\
46
DECLARE_RV_REACTING_HELPERS(name, type) \
47
\
48
/* \
49
* da_monitor_reset_##name - reset a monitor and setting it to init state \
50
*/ \
51
static inline void da_monitor_reset_##name(struct da_monitor *da_mon) \
52
{ \
53
da_mon->monitoring = 0; \
54
da_mon->curr_state = model_get_initial_state_##name(); \
55
} \
56
\
57
/* \
58
* da_monitor_start_##name - start monitoring \
59
* \
60
* The monitor will ignore all events until monitoring is set to true. This \
61
* function needs to be called to tell the monitor to start monitoring. \
62
*/ \
63
static inline void da_monitor_start_##name(struct da_monitor *da_mon) \
64
{ \
65
da_mon->curr_state = model_get_initial_state_##name(); \
66
da_mon->monitoring = 1; \
67
} \
68
\
69
/* \
70
* da_monitoring_##name - returns true if the monitor is processing events \
71
*/ \
72
static inline bool da_monitoring_##name(struct da_monitor *da_mon) \
73
{ \
74
return da_mon->monitoring; \
75
} \
76
\
77
/* \
78
* da_monitor_enabled_##name - checks if the monitor is enabled \
79
*/ \
80
static inline bool da_monitor_enabled_##name(void) \
81
{ \
82
/* global switch */ \
83
if (unlikely(!rv_monitoring_on())) \
84
return 0; \
85
\
86
/* monitor enabled */ \
87
if (unlikely(!rv_##name.enabled)) \
88
return 0; \
89
\
90
return 1; \
91
} \
92
\
93
/* \
94
* da_monitor_handling_event_##name - checks if the monitor is ready to handle events \
95
*/ \
96
static inline bool da_monitor_handling_event_##name(struct da_monitor *da_mon) \
97
{ \
98
\
99
if (!da_monitor_enabled_##name()) \
100
return 0; \
101
\
102
/* monitor is actually monitoring */ \
103
if (unlikely(!da_monitoring_##name(da_mon))) \
104
return 0; \
105
\
106
return 1; \
107
}
108
109
/*
110
* Event handler for implicit monitors. Implicit monitor is the one which the
111
* handler does not need to specify which da_monitor to manipulate. Examples
112
* of implicit monitor are the per_cpu or the global ones.
113
*
114
* Retry in case there is a race between getting and setting the next state,
115
* warn and reset the monitor if it runs out of retries. The monitor should be
116
* able to handle various orders.
117
*/
118
#define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
119
\
120
static inline bool \
121
da_event_##name(struct da_monitor *da_mon, enum events_##name event) \
122
{ \
123
enum states_##name curr_state, next_state; \
124
\
125
curr_state = READ_ONCE(da_mon->curr_state); \
126
for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \
127
next_state = model_get_next_state_##name(curr_state, event); \
128
if (next_state == INVALID_STATE) { \
129
cond_react_##name(curr_state, event); \
130
trace_error_##name(model_get_state_name_##name(curr_state), \
131
model_get_event_name_##name(event)); \
132
return false; \
133
} \
134
if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \
135
trace_event_##name(model_get_state_name_##name(curr_state), \
136
model_get_event_name_##name(event), \
137
model_get_state_name_##name(next_state), \
138
model_is_final_state_##name(next_state)); \
139
return true; \
140
} \
141
} \
142
\
143
trace_rv_retries_error(#name, model_get_event_name_##name(event)); \
144
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \
145
" retries reached for event %s, resetting monitor %s", \
146
model_get_event_name_##name(event), #name); \
147
return false; \
148
} \
149
150
/*
151
* Event handler for per_task monitors.
152
*
153
* Retry in case there is a race between getting and setting the next state,
154
* warn and reset the monitor if it runs out of retries. The monitor should be
155
* able to handle various orders.
156
*/
157
#define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \
158
\
159
static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct *tsk, \
160
enum events_##name event) \
161
{ \
162
enum states_##name curr_state, next_state; \
163
\
164
curr_state = READ_ONCE(da_mon->curr_state); \
165
for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \
166
next_state = model_get_next_state_##name(curr_state, event); \
167
if (next_state == INVALID_STATE) { \
168
cond_react_##name(curr_state, event); \
169
trace_error_##name(tsk->pid, \
170
model_get_state_name_##name(curr_state), \
171
model_get_event_name_##name(event)); \
172
return false; \
173
} \
174
if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \
175
trace_event_##name(tsk->pid, \
176
model_get_state_name_##name(curr_state), \
177
model_get_event_name_##name(event), \
178
model_get_state_name_##name(next_state), \
179
model_is_final_state_##name(next_state)); \
180
return true; \
181
} \
182
} \
183
\
184
trace_rv_retries_error(#name, model_get_event_name_##name(event)); \
185
pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \
186
" retries reached for event %s, resetting monitor %s", \
187
model_get_event_name_##name(event), #name); \
188
return false; \
189
}
190
191
/*
192
* Functions to define, init and get a global monitor.
193
*/
194
#define DECLARE_DA_MON_INIT_GLOBAL(name, type) \
195
\
196
/* \
197
* global monitor (a single variable) \
198
*/ \
199
static struct da_monitor da_mon_##name; \
200
\
201
/* \
202
* da_get_monitor_##name - return the global monitor address \
203
*/ \
204
static struct da_monitor *da_get_monitor_##name(void) \
205
{ \
206
return &da_mon_##name; \
207
} \
208
\
209
/* \
210
* da_monitor_reset_all_##name - reset the single monitor \
211
*/ \
212
static void da_monitor_reset_all_##name(void) \
213
{ \
214
da_monitor_reset_##name(da_get_monitor_##name()); \
215
} \
216
\
217
/* \
218
* da_monitor_init_##name - initialize a monitor \
219
*/ \
220
static inline int da_monitor_init_##name(void) \
221
{ \
222
da_monitor_reset_all_##name(); \
223
return 0; \
224
} \
225
\
226
/* \
227
* da_monitor_destroy_##name - destroy the monitor \
228
*/ \
229
static inline void da_monitor_destroy_##name(void) \
230
{ \
231
return; \
232
}
233
234
/*
235
* Functions to define, init and get a per-cpu monitor.
236
*/
237
#define DECLARE_DA_MON_INIT_PER_CPU(name, type) \
238
\
239
/* \
240
* per-cpu monitor variables \
241
*/ \
242
static DEFINE_PER_CPU(struct da_monitor, da_mon_##name); \
243
\
244
/* \
245
* da_get_monitor_##name - return current CPU monitor address \
246
*/ \
247
static struct da_monitor *da_get_monitor_##name(void) \
248
{ \
249
return this_cpu_ptr(&da_mon_##name); \
250
} \
251
\
252
/* \
253
* da_monitor_reset_all_##name - reset all CPUs' monitor \
254
*/ \
255
static void da_monitor_reset_all_##name(void) \
256
{ \
257
struct da_monitor *da_mon; \
258
int cpu; \
259
for_each_cpu(cpu, cpu_online_mask) { \
260
da_mon = per_cpu_ptr(&da_mon_##name, cpu); \
261
da_monitor_reset_##name(da_mon); \
262
} \
263
} \
264
\
265
/* \
266
* da_monitor_init_##name - initialize all CPUs' monitor \
267
*/ \
268
static inline int da_monitor_init_##name(void) \
269
{ \
270
da_monitor_reset_all_##name(); \
271
return 0; \
272
} \
273
\
274
/* \
275
* da_monitor_destroy_##name - destroy the monitor \
276
*/ \
277
static inline void da_monitor_destroy_##name(void) \
278
{ \
279
return; \
280
}
281
282
/*
283
* Functions to define, init and get a per-task monitor.
284
*/
285
#define DECLARE_DA_MON_INIT_PER_TASK(name, type) \
286
\
287
/* \
288
* The per-task monitor is stored a vector in the task struct. This variable \
289
* stores the position on the vector reserved for this monitor. \
290
*/ \
291
static int task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT; \
292
\
293
/* \
294
* da_get_monitor_##name - return the monitor in the allocated slot for tsk \
295
*/ \
296
static inline struct da_monitor *da_get_monitor_##name(struct task_struct *tsk) \
297
{ \
298
return &tsk->rv[task_mon_slot_##name].da_mon; \
299
} \
300
\
301
static void da_monitor_reset_all_##name(void) \
302
{ \
303
struct task_struct *g, *p; \
304
int cpu; \
305
\
306
read_lock(&tasklist_lock); \
307
for_each_process_thread(g, p) \
308
da_monitor_reset_##name(da_get_monitor_##name(p)); \
309
for_each_present_cpu(cpu) \
310
da_monitor_reset_##name(da_get_monitor_##name(idle_task(cpu))); \
311
read_unlock(&tasklist_lock); \
312
} \
313
\
314
/* \
315
* da_monitor_init_##name - initialize the per-task monitor \
316
* \
317
* Try to allocate a slot in the task's vector of monitors. If there \
318
* is an available slot, use it and reset all task's monitor. \
319
*/ \
320
static int da_monitor_init_##name(void) \
321
{ \
322
int slot; \
323
\
324
slot = rv_get_task_monitor_slot(); \
325
if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT) \
326
return slot; \
327
\
328
task_mon_slot_##name = slot; \
329
\
330
da_monitor_reset_all_##name(); \
331
return 0; \
332
} \
333
\
334
/* \
335
* da_monitor_destroy_##name - return the allocated slot \
336
*/ \
337
static inline void da_monitor_destroy_##name(void) \
338
{ \
339
if (task_mon_slot_##name == RV_PER_TASK_MONITOR_INIT) { \
340
WARN_ONCE(1, "Disabling a disabled monitor: " #name); \
341
return; \
342
} \
343
rv_put_task_monitor_slot(task_mon_slot_##name); \
344
task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT; \
345
return; \
346
}
347
348
/*
349
* Handle event for implicit monitor: da_get_monitor_##name() will figure out
350
* the monitor.
351
*/
352
#define DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type) \
353
\
354
static inline void __da_handle_event_##name(struct da_monitor *da_mon, \
355
enum events_##name event) \
356
{ \
357
bool retval; \
358
\
359
retval = da_event_##name(da_mon, event); \
360
if (!retval) \
361
da_monitor_reset_##name(da_mon); \
362
} \
363
\
364
/* \
365
* da_handle_event_##name - handle an event \
366
*/ \
367
static inline void da_handle_event_##name(enum events_##name event) \
368
{ \
369
struct da_monitor *da_mon = da_get_monitor_##name(); \
370
bool retval; \
371
\
372
retval = da_monitor_handling_event_##name(da_mon); \
373
if (!retval) \
374
return; \
375
\
376
__da_handle_event_##name(da_mon, event); \
377
} \
378
\
379
/* \
380
* da_handle_start_event_##name - start monitoring or handle event \
381
* \
382
* This function is used to notify the monitor that the system is returning \
383
* to the initial state, so the monitor can start monitoring in the next event. \
384
* Thus: \
385
* \
386
* If the monitor already started, handle the event. \
387
* If the monitor did not start yet, start the monitor but skip the event. \
388
*/ \
389
static inline bool da_handle_start_event_##name(enum events_##name event) \
390
{ \
391
struct da_monitor *da_mon; \
392
\
393
if (!da_monitor_enabled_##name()) \
394
return 0; \
395
\
396
da_mon = da_get_monitor_##name(); \
397
\
398
if (unlikely(!da_monitoring_##name(da_mon))) { \
399
da_monitor_start_##name(da_mon); \
400
return 0; \
401
} \
402
\
403
__da_handle_event_##name(da_mon, event); \
404
\
405
return 1; \
406
} \
407
\
408
/* \
409
* da_handle_start_run_event_##name - start monitoring and handle event \
410
* \
411
* This function is used to notify the monitor that the system is in the \
412
* initial state, so the monitor can start monitoring and handling event. \
413
*/ \
414
static inline bool da_handle_start_run_event_##name(enum events_##name event) \
415
{ \
416
struct da_monitor *da_mon; \
417
\
418
if (!da_monitor_enabled_##name()) \
419
return 0; \
420
\
421
da_mon = da_get_monitor_##name(); \
422
\
423
if (unlikely(!da_monitoring_##name(da_mon))) \
424
da_monitor_start_##name(da_mon); \
425
\
426
__da_handle_event_##name(da_mon, event); \
427
\
428
return 1; \
429
}
430
431
/*
432
* Handle event for per task.
433
*/
434
#define DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type) \
435
\
436
static inline void \
437
__da_handle_event_##name(struct da_monitor *da_mon, struct task_struct *tsk, \
438
enum events_##name event) \
439
{ \
440
bool retval; \
441
\
442
retval = da_event_##name(da_mon, tsk, event); \
443
if (!retval) \
444
da_monitor_reset_##name(da_mon); \
445
} \
446
\
447
/* \
448
* da_handle_event_##name - handle an event \
449
*/ \
450
static inline void \
451
da_handle_event_##name(struct task_struct *tsk, enum events_##name event) \
452
{ \
453
struct da_monitor *da_mon = da_get_monitor_##name(tsk); \
454
bool retval; \
455
\
456
retval = da_monitor_handling_event_##name(da_mon); \
457
if (!retval) \
458
return; \
459
\
460
__da_handle_event_##name(da_mon, tsk, event); \
461
} \
462
\
463
/* \
464
* da_handle_start_event_##name - start monitoring or handle event \
465
* \
466
* This function is used to notify the monitor that the system is returning \
467
* to the initial state, so the monitor can start monitoring in the next event. \
468
* Thus: \
469
* \
470
* If the monitor already started, handle the event. \
471
* If the monitor did not start yet, start the monitor but skip the event. \
472
*/ \
473
static inline bool \
474
da_handle_start_event_##name(struct task_struct *tsk, enum events_##name event) \
475
{ \
476
struct da_monitor *da_mon; \
477
\
478
if (!da_monitor_enabled_##name()) \
479
return 0; \
480
\
481
da_mon = da_get_monitor_##name(tsk); \
482
\
483
if (unlikely(!da_monitoring_##name(da_mon))) { \
484
da_monitor_start_##name(da_mon); \
485
return 0; \
486
} \
487
\
488
__da_handle_event_##name(da_mon, tsk, event); \
489
\
490
return 1; \
491
} \
492
\
493
/* \
494
* da_handle_start_run_event_##name - start monitoring and handle event \
495
* \
496
* This function is used to notify the monitor that the system is in the \
497
* initial state, so the monitor can start monitoring and handling event. \
498
*/ \
499
static inline bool \
500
da_handle_start_run_event_##name(struct task_struct *tsk, enum events_##name event) \
501
{ \
502
struct da_monitor *da_mon; \
503
\
504
if (!da_monitor_enabled_##name()) \
505
return 0; \
506
\
507
da_mon = da_get_monitor_##name(tsk); \
508
\
509
if (unlikely(!da_monitoring_##name(da_mon))) \
510
da_monitor_start_##name(da_mon); \
511
\
512
__da_handle_event_##name(da_mon, tsk, event); \
513
\
514
return 1; \
515
}
516
517
/*
518
* Entry point for the global monitor.
519
*/
520
#define DECLARE_DA_MON_GLOBAL(name, type) \
521
\
522
DECLARE_AUTOMATA_HELPERS(name, type) \
523
DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
524
DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
525
DECLARE_DA_MON_INIT_GLOBAL(name, type) \
526
DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
527
528
/*
529
* Entry point for the per-cpu monitor.
530
*/
531
#define DECLARE_DA_MON_PER_CPU(name, type) \
532
\
533
DECLARE_AUTOMATA_HELPERS(name, type) \
534
DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
535
DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \
536
DECLARE_DA_MON_INIT_PER_CPU(name, type) \
537
DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
538
539
/*
540
* Entry point for the per-task monitor.
541
*/
542
#define DECLARE_DA_MON_PER_TASK(name, type) \
543
\
544
DECLARE_AUTOMATA_HELPERS(name, type) \
545
DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
546
DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \
547
DECLARE_DA_MON_INIT_PER_TASK(name, type) \
548
DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)
549
550