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