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