1 // SPDX-License-Identifier: GPL-2.0 2 #include <linux/ftrace.h> 3 #include <linux/tracepoint.h> 4 #include <linux/kernel.h> 5 #include <linux/module.h> 6 #include <linux/init.h> 7 #include <linux/rv.h> 8 #include <rv/instrumentation.h> 9 10 #define MODULE_NAME "%%MODEL_NAME%%" 11 12 /* 13 * XXX: include required tracepoint headers, e.g., 14 * #include <trace/events/sched.h> 15 */ 16 #include <rv_trace.h> 17 %%INCLUDE_PARENT%% 18 19 /* 20 * This is the self-generated part of the monitor. Generally, there is no need 21 * to touch this section. 22 */ 23 #include "%%MODEL_NAME%%.h" 24 #include <rv/ltl_monitor.h> 25 26 static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) 27 { 28 /* 29 * This is called everytime the Buchi automaton is triggered. 30 * 31 * This function could be used to fetch the atomic propositions which 32 * are expensive to trace. It is possible only if the atomic proposition 33 * does not need to be updated at precise time. 34 * 35 * It is recommended to use tracepoints and ltl_atom_update() instead. 36 */ 37 } 38 39 static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) 40 { 41 /* 42 * This should initialize as many atomic propositions as possible. 43 * 44 * @task_creation indicates whether the task is being created. This is 45 * false if the task is already running before the monitor is enabled. 46 */ 47 %%ATOMS_INIT%% 48 } 49 50 /* 51 * This is the instrumentation part of the monitor. 52 * 53 * This is the section where manual work is required. Here the kernel events 54 * are translated into model's event. 55 */ 56 %%TRACEPOINT_HANDLERS_SKEL%% 57 static int enable_%%MODEL_NAME%%(void) 58 { 59 int retval; 60 61 retval = ltl_monitor_init(); 62 if (retval) 63 return retval; 64 65 %%TRACEPOINT_ATTACH%% 66 67 return 0; 68 } 69 70 static void disable_%%MODEL_NAME%%(void) 71 { 72 %%TRACEPOINT_DETACH%% 73 74 ltl_monitor_destroy(); 75 } 76 77 /* 78 * This is the monitor register section. 79 */ 80 static struct rv_monitor rv_this = { 81 .name = "%%MODEL_NAME%%", 82 .description = "%%DESCRIPTION%%", 83 .enable = enable_%%MODEL_NAME%%, 84 .disable = disable_%%MODEL_NAME%%, 85 }; 86 87 static int __init register_%%MODEL_NAME%%(void) 88 { 89 return rv_register_monitor(&rv_this, %%PARENT%%); 90 } 91 92 static void __exit unregister_%%MODEL_NAME%%(void) 93 { 94 rv_unregister_monitor(&rv_this); 95 } 96 97 module_init(register_%%MODEL_NAME%%); 98 module_exit(unregister_%%MODEL_NAME%%); 99 100 MODULE_LICENSE("GPL"); 101 MODULE_AUTHOR("rvgen: auto-generated"); 102 MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); 103