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) \ 21static char REACT_MSG_##name[1024]; \ 22 \ 23static 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 \ 33static void cond_react_##name(char *msg) \ 34{ \ 35 if (rv_##name.react) \ 36 rv_##name.react(msg); \ 37} \ 38 \ 39static 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) \ 47static inline char *format_react_msg_##name(type curr_state, type event) \ 48{ \ 49 return NULL; \ 50} \ 51 \ 52static void cond_react_##name(char *msg) \ 53{ \ 54 return; \ 55} \ 56 \ 57static 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 \ 68DECLARE_RV_REACTING_HELPERS(name, type) \ 69 \ 70/* \ 71 * da_monitor_reset_##name - reset a monitor and setting it to init state \ 72 */ \ 73static 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 */ \ 82static 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 */ \ 90static inline void \ 91da_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 */ \ 102static 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 */ \ 111static 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 */ \ 119static 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 */ \ 135static 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 \ 155static inline bool \ 156da_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 \ 186static 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 */ \ 222static struct da_monitor da_mon_##name; \ 223 \ 224/* \ 225 * da_get_monitor_##name - return the global monitor address \ 226 */ \ 227static 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 */ \ 235static 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 */ \ 243static 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 */ \ 252static 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 */ \ 265static DEFINE_PER_CPU(struct da_monitor, da_mon_##name); \ 266 \ 267/* \ 268 * da_get_monitor_##name - return current CPU monitor address \ 269 */ \ 270static 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 */ \ 278static 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 */ \ 291static 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 */ \ 300static 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 */ \ 314static 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 */ \ 319static 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 \ 324static 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 */ \ 340static 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 */ \ 357static 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 \ 374static 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 */ \ 387static 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 */ \ 409static 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 */ \ 434static 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 \ 456static 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 */ \ 470static inline void \ 471da_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 */ \ 493static inline bool \ 494da_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 \ 518DECLARE_AUTOMATA_HELPERS(name, type) \ 519DECLARE_DA_MON_GENERIC_HELPERS(name, type) \ 520DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \ 521DECLARE_DA_MON_INIT_GLOBAL(name, type) \ 522DECLARE_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 \ 529DECLARE_AUTOMATA_HELPERS(name, type) \ 530DECLARE_DA_MON_GENERIC_HELPERS(name, type) \ 531DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \ 532DECLARE_DA_MON_INIT_PER_CPU(name, type) \ 533DECLARE_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 \ 540DECLARE_AUTOMATA_HELPERS(name, type) \ 541DECLARE_DA_MON_GENERIC_HELPERS(name, type) \ 542DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \ 543DECLARE_DA_MON_INIT_PER_TASK(name, type) \ 544DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type) 545