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