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