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 "test_ltl" 11 12 /* 13 * XXX: include required tracepoint headers, e.g., 14 * #include <trace/events/sched.h> 15 */ 16 #include <rv_trace.h> 17 #include <monitors/ltl_parent/ltl_parent.h> 18 19 20 /* 21 * This is the self-generated part of the monitor. Generally, there is no need 22 * to touch this section. 23 */ 24 #include "test_ltl.h" 25 #include <rv/ltl_monitor.h> 26 27 static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) 28 { 29 /* 30 * This is called everytime the Buchi automaton is triggered. 31 * 32 * This function could be used to fetch the atomic propositions which 33 * are expensive to trace. It is possible only if the atomic proposition 34 * does not need to be updated at precise time. 35 * 36 * It is recommended to use tracepoints and ltl_atom_update() instead. 37 */ 38 } 39 40 static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) 41 { 42 /* 43 * This should initialize as many atomic propositions as possible. 44 * 45 * @task_creation indicates whether the task is being created. This is 46 * false if the task is already running before the monitor is enabled. 47 */ 48 ltl_atom_set(mon, LTL_EVENT_A, true/false); 49 ltl_atom_set(mon, LTL_EVENT_B, true/false); 50 } 51 52 /* 53 * This is the instrumentation part of the monitor. 54 * 55 * This is the section where manual work is required. Here the kernel events 56 * are translated into model's event. 57 */ 58 static void handle_example_event(void *data, /* XXX: fill header */) 59 { 60 ltl_atom_update(task, LTL_EVENT_A, true/false); 61 } 62 63 static int enable_test_ltl(void) 64 { 65 int retval; 66 67 retval = ltl_monitor_init(); 68 if (retval) 69 return retval; 70 71 rv_attach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event); 72 73 return 0; 74 } 75 76 static void disable_test_ltl(void) 77 { 78 rv_detach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event); 79 80 ltl_monitor_destroy(); 81 } 82 83 /* 84 * This is the monitor register section. 85 */ 86 static struct rv_monitor rv_this = { 87 .name = "test_ltl", 88 .description = "Simple description", 89 .enable = enable_test_ltl, 90 .disable = disable_test_ltl, 91 }; 92 93 static int __init register_test_ltl(void) 94 { 95 return rv_register_monitor(&rv_this, &rv_ltl_parent); 96 } 97 98 static void __exit unregister_test_ltl(void) 99 { 100 rv_unregister_monitor(&rv_this); 101 } 102 103 module_init(register_test_ltl); 104 module_exit(unregister_test_ltl); 105 106 MODULE_LICENSE("GPL"); 107 MODULE_AUTHOR("rvgen: auto-generated"); 108 MODULE_DESCRIPTION("test_ltl: Simple description"); 109