Back to home page

OSCL-LXR

 
 

    


0001 /* SPDX-License-Identifier: GPL-2.0 */
0002 /*
0003  * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
0004  *
0005  * Deterministic automata (DA) monitor functions, to be used together
0006  * with automata models in C generated by the dot2k tool.
0007  *
0008  * The dot2k tool is available at tools/verification/dot2k/
0009  *
0010  * For further information, see:
0011  *   Documentation/trace/rv/da_monitor_synthesis.rst
0012  */
0013 
0014 #include <rv/automata.h>
0015 #include <linux/rv.h>
0016 #include <linux/bug.h>
0017 
0018 #ifdef CONFIG_RV_REACTORS
0019 
0020 #define DECLARE_RV_REACTING_HELPERS(name, type)                         \
0021 static char REACT_MSG_##name[1024];                             \
0022                                                 \
0023 static inline char *format_react_msg_##name(type curr_state, type event)            \
0024 {                                               \
0025     snprintf(REACT_MSG_##name, 1024,                            \
0026          "rv: monitor %s does not allow event %s on state %s\n",            \
0027          #name,                                     \
0028          model_get_event_name_##name(event),                        \
0029          model_get_state_name_##name(curr_state));                  \
0030     return REACT_MSG_##name;                                \
0031 }                                               \
0032                                                 \
0033 static void cond_react_##name(char *msg)                            \
0034 {                                               \
0035     if (rv_##name.react)                                    \
0036         rv_##name.react(msg);                               \
0037 }                                               \
0038                                                 \
0039 static bool rv_reacting_on_##name(void)                             \
0040 {                                               \
0041     return rv_reacting_on();                                \
0042 }
0043 
0044 #else /* CONFIG_RV_REACTOR */
0045 
0046 #define DECLARE_RV_REACTING_HELPERS(name, type)                         \
0047 static inline char *format_react_msg_##name(type curr_state, type event)            \
0048 {                                               \
0049     return NULL;                                        \
0050 }                                               \
0051                                                 \
0052 static void cond_react_##name(char *msg)                            \
0053 {                                               \
0054     return;                                         \
0055 }                                               \
0056                                                 \
0057 static bool rv_reacting_on_##name(void)                             \
0058 {                                               \
0059     return 0;                                       \
0060 }
0061 #endif
0062 
0063 /*
0064  * Generic helpers for all types of deterministic automata monitors.
0065  */
0066 #define DECLARE_DA_MON_GENERIC_HELPERS(name, type)                      \
0067                                                 \
0068 DECLARE_RV_REACTING_HELPERS(name, type)                             \
0069                                                 \
0070 /*                                              \
0071  * da_monitor_reset_##name - reset a monitor and setting it to init state           \
0072  */                                             \
0073 static inline void da_monitor_reset_##name(struct da_monitor *da_mon)               \
0074 {                                               \
0075     da_mon->monitoring = 0;                                 \
0076     da_mon->curr_state = model_get_initial_state_##name();                  \
0077 }                                               \
0078                                                 \
0079 /*                                              \
0080  * da_monitor_curr_state_##name - return the current state                  \
0081  */                                             \
0082 static inline type da_monitor_curr_state_##name(struct da_monitor *da_mon)          \
0083 {                                               \
0084     return da_mon->curr_state;                              \
0085 }                                               \
0086                                                 \
0087 /*                                              \
0088  * da_monitor_set_state_##name - set the new current state                  \
0089  */                                             \
0090 static inline void                                      \
0091 da_monitor_set_state_##name(struct da_monitor *da_mon, enum states_##name state)        \
0092 {                                               \
0093     da_mon->curr_state = state;                             \
0094 }                                               \
0095                                                 \
0096 /*                                              \
0097  * da_monitor_start_##name - start monitoring                           \
0098  *                                              \
0099  * The monitor will ignore all events until monitoring is set to true. This         \
0100  * function needs to be called to tell the monitor to start monitoring.             \
0101  */                                             \
0102 static inline void da_monitor_start_##name(struct da_monitor *da_mon)               \
0103 {                                               \
0104     da_mon->curr_state = model_get_initial_state_##name();                  \
0105     da_mon->monitoring = 1;                                 \
0106 }                                               \
0107                                                 \
0108 /*                                              \
0109  * da_monitoring_##name - returns true if the monitor is processing events          \
0110  */                                             \
0111 static inline bool da_monitoring_##name(struct da_monitor *da_mon)              \
0112 {                                               \
0113     return da_mon->monitoring;                              \
0114 }                                               \
0115                                                 \
0116 /*                                              \
0117  * da_monitor_enabled_##name - checks if the monitor is enabled                 \
0118  */                                             \
0119 static inline bool da_monitor_enabled_##name(void)                      \
0120 {                                               \
0121     /* global switch */                                 \
0122     if (unlikely(!rv_monitoring_on()))                          \
0123         return 0;                                   \
0124                                                 \
0125     /* monitor enabled */                                   \
0126     if (unlikely(!rv_##name.enabled))                           \
0127         return 0;                                   \
0128                                                 \
0129     return 1;                                       \
0130 }                                               \
0131                                                 \
0132 /*                                              \
0133  * da_monitor_handling_event_##name - checks if the monitor is ready to handle events       \
0134  */                                             \
0135 static inline bool da_monitor_handling_event_##name(struct da_monitor *da_mon)          \
0136 {                                               \
0137                                                 \
0138     if (!da_monitor_enabled_##name())                           \
0139         return 0;                                   \
0140                                                 \
0141     /* monitor is actually monitoring */                            \
0142     if (unlikely(!da_monitoring_##name(da_mon)))                        \
0143         return 0;                                   \
0144                                                 \
0145     return 1;                                       \
0146 }
0147 
0148 /*
0149  * Event handler for implicit monitors. Implicit monitor is the one which the
0150  * handler does not need to specify which da_monitor to manipulate. Examples
0151  * of implicit monitor are the per_cpu or the global ones.
0152  */
0153 #define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)                   \
0154                                                 \
0155 static inline bool                                      \
0156 da_event_##name(struct da_monitor *da_mon, enum events_##name event)                \
0157 {                                               \
0158     type curr_state = da_monitor_curr_state_##name(da_mon);                 \
0159     type next_state = model_get_next_state_##name(curr_state, event);           \
0160                                                 \
0161     if (next_state != INVALID_STATE) {                          \
0162         da_monitor_set_state_##name(da_mon, next_state);                \
0163                                                 \
0164         trace_event_##name(model_get_state_name_##name(curr_state),         \
0165                    model_get_event_name_##name(event),              \
0166                    model_get_state_name_##name(next_state),         \
0167                    model_is_final_state_##name(next_state));            \
0168                                                 \
0169         return true;                                    \
0170     }                                           \
0171                                                 \
0172     if (rv_reacting_on_##name())                                \
0173         cond_react_##name(format_react_msg_##name(curr_state, event));          \
0174                                                 \
0175     trace_error_##name(model_get_state_name_##name(curr_state),             \
0176                model_get_event_name_##name(event));                 \
0177                                                 \
0178     return false;                                       \
0179 }                                               \
0180 
0181 /*
0182  * Event handler for per_task monitors.
0183  */
0184 #define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)                   \
0185                                                 \
0186 static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct *tsk,      \
0187                    enum events_##name event)                    \
0188 {                                               \
0189     type curr_state = da_monitor_curr_state_##name(da_mon);                 \
0190     type next_state = model_get_next_state_##name(curr_state, event);           \
0191                                                 \
0192     if (next_state != INVALID_STATE) {                          \
0193         da_monitor_set_state_##name(da_mon, next_state);                \
0194                                                 \
0195         trace_event_##name(tsk->pid,                            \
0196                    model_get_state_name_##name(curr_state),         \
0197                    model_get_event_name_##name(event),              \
0198                    model_get_state_name_##name(next_state),         \
0199                    model_is_final_state_##name(next_state));            \
0200                                                 \
0201         return true;                                    \
0202     }                                           \
0203                                                 \
0204     if (rv_reacting_on_##name())                                \
0205         cond_react_##name(format_react_msg_##name(curr_state, event));          \
0206                                                 \
0207     trace_error_##name(tsk->pid,                                \
0208                model_get_state_name_##name(curr_state),             \
0209                model_get_event_name_##name(event));                 \
0210                                                 \
0211     return false;                                       \
0212 }
0213 
0214 /*
0215  * Functions to define, init and get a global monitor.
0216  */
0217 #define DECLARE_DA_MON_INIT_GLOBAL(name, type)                          \
0218                                                 \
0219 /*                                              \
0220  * global monitor (a single variable)                               \
0221  */                                             \
0222 static struct da_monitor da_mon_##name;                             \
0223                                                 \
0224 /*                                              \
0225  * da_get_monitor_##name - return the global monitor address                    \
0226  */                                             \
0227 static struct da_monitor *da_get_monitor_##name(void)                       \
0228 {                                               \
0229     return &da_mon_##name;                                  \
0230 }                                               \
0231                                                 \
0232 /*                                              \
0233  * da_monitor_reset_all_##name - reset the single monitor                   \
0234  */                                             \
0235 static void da_monitor_reset_all_##name(void)                           \
0236 {                                               \
0237     da_monitor_reset_##name(da_get_monitor_##name());                   \
0238 }                                               \
0239                                                 \
0240 /*                                              \
0241  * da_monitor_init_##name - initialize a monitor                        \
0242  */                                             \
0243 static inline int da_monitor_init_##name(void)                          \
0244 {                                               \
0245     da_monitor_reset_all_##name();                              \
0246     return 0;                                       \
0247 }                                               \
0248                                                 \
0249 /*                                              \
0250  * da_monitor_destroy_##name - destroy the monitor                      \
0251  */                                             \
0252 static inline void da_monitor_destroy_##name(void)                      \
0253 {                                               \
0254     return;                                         \
0255 }
0256 
0257 /*
0258  * Functions to define, init and get a per-cpu monitor.
0259  */
0260 #define DECLARE_DA_MON_INIT_PER_CPU(name, type)                         \
0261                                                 \
0262 /*                                              \
0263  * per-cpu monitor variables                                    \
0264  */                                             \
0265 DEFINE_PER_CPU(struct da_monitor, da_mon_##name);                       \
0266                                                 \
0267 /*                                              \
0268  * da_get_monitor_##name - return current CPU monitor address                   \
0269  */                                             \
0270 static struct da_monitor *da_get_monitor_##name(void)                       \
0271 {                                               \
0272     return this_cpu_ptr(&da_mon_##name);                            \
0273 }                                               \
0274                                                 \
0275 /*                                              \
0276  * da_monitor_reset_all_##name - reset all CPUs' monitor                    \
0277  */                                             \
0278 static void da_monitor_reset_all_##name(void)                           \
0279 {                                               \
0280     struct da_monitor *da_mon;                              \
0281     int cpu;                                        \
0282     for_each_cpu(cpu, cpu_online_mask) {                            \
0283         da_mon = per_cpu_ptr(&da_mon_##name, cpu);                  \
0284         da_monitor_reset_##name(da_mon);                        \
0285     }                                           \
0286 }                                               \
0287                                                 \
0288 /*                                              \
0289  * da_monitor_init_##name - initialize all CPUs' monitor                    \
0290  */                                             \
0291 static inline int da_monitor_init_##name(void)                          \
0292 {                                               \
0293     da_monitor_reset_all_##name();                              \
0294     return 0;                                       \
0295 }                                               \
0296                                                 \
0297 /*                                              \
0298  * da_monitor_destroy_##name - destroy the monitor                      \
0299  */                                             \
0300 static inline void da_monitor_destroy_##name(void)                      \
0301 {                                               \
0302     return;                                         \
0303 }
0304 
0305 /*
0306  * Functions to define, init and get a per-task monitor.
0307  */
0308 #define DECLARE_DA_MON_INIT_PER_TASK(name, type)                        \
0309                                                 \
0310 /*                                              \
0311  * The per-task monitor is stored a vector in the task struct. This variable            \
0312  * stores the position on the vector reserved for this monitor.                 \
0313  */                                             \
0314 static int task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT;                 \
0315                                                 \
0316 /*                                              \
0317  * da_get_monitor_##name - return the monitor in the allocated slot for tsk             \
0318  */                                             \
0319 static inline struct da_monitor *da_get_monitor_##name(struct task_struct *tsk)         \
0320 {                                               \
0321     return &tsk->rv[task_mon_slot_##name].da_mon;                       \
0322 }                                               \
0323                                                 \
0324 static void da_monitor_reset_all_##name(void)                           \
0325 {                                               \
0326     struct task_struct *g, *p;                              \
0327                                                 \
0328     read_lock(&tasklist_lock);                              \
0329     for_each_process_thread(g, p)                               \
0330         da_monitor_reset_##name(da_get_monitor_##name(p));              \
0331     read_unlock(&tasklist_lock);                                \
0332 }                                               \
0333                                                 \
0334 /*                                              \
0335  * da_monitor_init_##name - initialize the per-task monitor                 \
0336  *                                              \
0337  * Try to allocate a slot in the task's vector of monitors. If there                \
0338  * is an available slot, use it and reset all task's monitor.                   \
0339  */                                             \
0340 static int da_monitor_init_##name(void)                             \
0341 {                                               \
0342     int slot;                                       \
0343                                                 \
0344     slot = rv_get_task_monitor_slot();                          \
0345     if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT)                   \
0346         return slot;                                    \
0347                                                 \
0348     task_mon_slot_##name = slot;                                \
0349                                                 \
0350     da_monitor_reset_all_##name();                              \
0351     return 0;                                       \
0352 }                                               \
0353                                                 \
0354 /*                                              \
0355  * da_monitor_destroy_##name - return the allocated slot                    \
0356  */                                             \
0357 static inline void da_monitor_destroy_##name(void)                      \
0358 {                                               \
0359     if (task_mon_slot_##name == RV_PER_TASK_MONITOR_INIT) {                 \
0360         WARN_ONCE(1, "Disabling a disabled monitor: " #name);               \
0361         return;                                     \
0362     }                                           \
0363     rv_put_task_monitor_slot(task_mon_slot_##name);                     \
0364     task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT;                    \
0365     return;                                         \
0366 }
0367 
0368 /*
0369  * Handle event for implicit monitor: da_get_monitor_##name() will figure out
0370  * the monitor.
0371  */
0372 #define DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)                 \
0373                                                 \
0374 static inline void __da_handle_event_##name(struct da_monitor *da_mon,              \
0375                         enum events_##name event)               \
0376 {                                               \
0377     bool retval;                                        \
0378                                                 \
0379     retval = da_event_##name(da_mon, event);                        \
0380     if (!retval)                                        \
0381         da_monitor_reset_##name(da_mon);                        \
0382 }                                               \
0383                                                 \
0384 /*                                              \
0385  * da_handle_event_##name - handle an event                         \
0386  */                                             \
0387 static inline void da_handle_event_##name(enum events_##name event)             \
0388 {                                               \
0389     struct da_monitor *da_mon = da_get_monitor_##name();                    \
0390     bool retval;                                        \
0391                                                 \
0392     retval = da_monitor_handling_event_##name(da_mon);                  \
0393     if (!retval)                                        \
0394         return;                                     \
0395                                                 \
0396     __da_handle_event_##name(da_mon, event);                        \
0397 }                                               \
0398                                                 \
0399 /*                                              \
0400  * da_handle_start_event_##name - start monitoring or handle event              \
0401  *                                              \
0402  * This function is used to notify the monitor that the system is returning         \
0403  * to the initial state, so the monitor can start monitoring in the next event.         \
0404  * Thus:                                            \
0405  *                                              \
0406  * If the monitor already started, handle the event.                        \
0407  * If the monitor did not start yet, start the monitor but skip the event.          \
0408  */                                             \
0409 static inline bool da_handle_start_event_##name(enum events_##name event)           \
0410 {                                               \
0411     struct da_monitor *da_mon;                              \
0412                                                 \
0413     if (!da_monitor_enabled_##name())                           \
0414         return 0;                                   \
0415                                                 \
0416     da_mon = da_get_monitor_##name();                           \
0417                                                 \
0418     if (unlikely(!da_monitoring_##name(da_mon))) {                      \
0419         da_monitor_start_##name(da_mon);                        \
0420         return 0;                                   \
0421     }                                           \
0422                                                 \
0423     __da_handle_event_##name(da_mon, event);                        \
0424                                                 \
0425     return 1;                                       \
0426 }                                               \
0427                                                 \
0428 /*                                              \
0429  * da_handle_start_run_event_##name - start monitoring and handle event             \
0430  *                                              \
0431  * This function is used to notify the monitor that the system is in the            \
0432  * initial state, so the monitor can start monitoring and handling event.           \
0433  */                                             \
0434 static inline bool da_handle_start_run_event_##name(enum events_##name event)           \
0435 {                                               \
0436     struct da_monitor *da_mon;                              \
0437                                                 \
0438     if (!da_monitor_enabled_##name())                           \
0439         return 0;                                   \
0440                                                 \
0441     da_mon = da_get_monitor_##name();                           \
0442                                                 \
0443     if (unlikely(!da_monitoring_##name(da_mon)))                        \
0444         da_monitor_start_##name(da_mon);                        \
0445                                                 \
0446     __da_handle_event_##name(da_mon, event);                        \
0447                                                 \
0448     return 1;                                       \
0449 }
0450 
0451 /*
0452  * Handle event for per task.
0453  */
0454 #define DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)                 \
0455                                                 \
0456 static inline void                                      \
0457 __da_handle_event_##name(struct da_monitor *da_mon, struct task_struct *tsk,            \
0458              enum events_##name event)                      \
0459 {                                               \
0460     bool retval;                                        \
0461                                                 \
0462     retval = da_event_##name(da_mon, tsk, event);                       \
0463     if (!retval)                                        \
0464         da_monitor_reset_##name(da_mon);                        \
0465 }                                               \
0466                                                 \
0467 /*                                              \
0468  * da_handle_event_##name - handle an event                         \
0469  */                                             \
0470 static inline void                                      \
0471 da_handle_event_##name(struct task_struct *tsk, enum events_##name event)           \
0472 {                                               \
0473     struct da_monitor *da_mon = da_get_monitor_##name(tsk);                 \
0474     bool retval;                                        \
0475                                                 \
0476     retval = da_monitor_handling_event_##name(da_mon);                  \
0477     if (!retval)                                        \
0478         return;                                     \
0479                                                 \
0480     __da_handle_event_##name(da_mon, tsk, event);                       \
0481 }                                               \
0482                                                 \
0483 /*                                              \
0484  * da_handle_start_event_##name - start monitoring or handle event              \
0485  *                                              \
0486  * This function is used to notify the monitor that the system is returning         \
0487  * to the initial state, so the monitor can start monitoring in the next event.         \
0488  * Thus:                                            \
0489  *                                              \
0490  * If the monitor already started, handle the event.                        \
0491  * If the monitor did not start yet, start the monitor but skip the event.          \
0492  */                                             \
0493 static inline bool                                      \
0494 da_handle_start_event_##name(struct task_struct *tsk, enum events_##name event)         \
0495 {                                               \
0496     struct da_monitor *da_mon;                              \
0497                                                 \
0498     if (!da_monitor_enabled_##name())                           \
0499         return 0;                                   \
0500                                                 \
0501     da_mon = da_get_monitor_##name(tsk);                            \
0502                                                 \
0503     if (unlikely(!da_monitoring_##name(da_mon))) {                      \
0504         da_monitor_start_##name(da_mon);                        \
0505         return 0;                                   \
0506     }                                           \
0507                                                 \
0508     __da_handle_event_##name(da_mon, tsk, event);                       \
0509                                                 \
0510     return 1;                                       \
0511 }
0512 
0513 /*
0514  * Entry point for the global monitor.
0515  */
0516 #define DECLARE_DA_MON_GLOBAL(name, type)                           \
0517                                                 \
0518 DECLARE_AUTOMATA_HELPERS(name, type)                                \
0519 DECLARE_DA_MON_GENERIC_HELPERS(name, type)                          \
0520 DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)                       \
0521 DECLARE_DA_MON_INIT_GLOBAL(name, type)                              \
0522 DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
0523 
0524 /*
0525  * Entry point for the per-cpu monitor.
0526  */
0527 #define DECLARE_DA_MON_PER_CPU(name, type)                          \
0528                                                 \
0529 DECLARE_AUTOMATA_HELPERS(name, type)                                \
0530 DECLARE_DA_MON_GENERIC_HELPERS(name, type)                          \
0531 DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)                       \
0532 DECLARE_DA_MON_INIT_PER_CPU(name, type)                             \
0533 DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)
0534 
0535 /*
0536  * Entry point for the per-task monitor.
0537  */
0538 #define DECLARE_DA_MON_PER_TASK(name, type)                         \
0539                                                 \
0540 DECLARE_AUTOMATA_HELPERS(name, type)                                \
0541 DECLARE_DA_MON_GENERIC_HELPERS(name, type)                          \
0542 DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)                       \
0543 DECLARE_DA_MON_INIT_PER_TASK(name, type)                            \
0544 DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)