da_monitor.h 17 KB

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