545 lines · c
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 together6 * 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.rst12 */13 14#include <rv/automata.h>15#include <linux/rv.h>16#include <linux/bug.h>17 18#ifdef CONFIG_RV_REACTORS19 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#endif62 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 the150 * handler does not need to specify which da_monitor to manipulate. Examples151 * 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 out370 * 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