include/rv/da_monitor.h

   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)