da_monitor.h 17 KB

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