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 "ltl_pertask" 11 12 /* 13 * XXX: include required tracepoint headers, e.g., 14 * #include <trace/events/sched.h> 15 */ 16 #include <rv_trace.h> 17 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 "ltl_pertask.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 ltl_atom_set(mon, LTL_EVENT_A, true/false); 48 ltl_atom_set(mon, LTL_EVENT_B, true/false); 49 } 50 51 /* 52 * This is the instrumentation part of the monitor. 53 * 54 * This is the section where manual work is required. Here the kernel events 55 * are translated into model's event. 56 */ 57 static void handle_example_event(void *data, /* XXX: fill header */) 58 { 59 ltl_atom_update(task, LTL_EVENT_A, true/false); 60 } 61 62 static int enable_ltl_pertask(void) 63 { 64 int retval; 65 66 retval = ltl_monitor_init(); 67 if (retval) 68 return retval; 69 70 rv_attach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event); 71 72 return 0; 73 } 74 75 static void disable_ltl_pertask(void) 76 { 77 rv_detach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event); 78 79 ltl_monitor_destroy(); 80 } 81 82 /* 83 * This is the monitor register section. 84 */ 85 static struct rv_monitor rv_this = { 86 .name = "ltl_pertask", 87 .description = "auto-generated", 88 .enable = enable_ltl_pertask, 89 .disable = disable_ltl_pertask, 90 }; 91 92 static int __init register_ltl_pertask(void) 93 { 94 return rv_register_monitor(&rv_this, NULL); 95 } 96 97 static void __exit unregister_ltl_pertask(void) 98 { 99 rv_unregister_monitor(&rv_this); 100 } 101 102 module_init(register_ltl_pertask); 103 module_exit(unregister_ltl_pertask); 104 105 MODULE_LICENSE("GPL"); 106 MODULE_AUTHOR("rvgen: auto-generated"); 107 MODULE_DESCRIPTION("ltl_pertask: auto-generated"); 108