1 /* SPDX-License-Identifier: GPL-2.0 */ 2 /** 3 * This file must be combined with the $(MODEL_NAME).h file generated by 4 * tools/verification/rvgen. 5 */ 6 7 #include <linux/args.h> 8 #include <linux/rv.h> 9 #include <linux/stringify.h> 10 #include <linux/seq_buf.h> 11 #include <rv/instrumentation.h> 12 #include <trace/events/task.h> 13 #include <trace/events/sched.h> 14 15 #ifndef MONITOR_NAME 16 #error "Please include $(MODEL_NAME).h generated by rvgen" 17 #endif 18 19 static struct rv_monitor rv_this; 20 21 static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; 22 23 static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon); 24 static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation); 25 26 static struct ltl_monitor *ltl_get_monitor(struct task_struct *task) 27 { 28 return &task->rv[ltl_monitor_slot].ltl_mon; 29 } 30 31 static void ltl_task_init(struct task_struct *task, bool task_creation) 32 { 33 struct ltl_monitor *mon = ltl_get_monitor(task); 34 35 memset(&mon->states, 0, sizeof(mon->states)); 36 37 for (int i = 0; i < LTL_NUM_ATOM; ++i) 38 __set_bit(i, mon->unknown_atoms); 39 40 ltl_atoms_init(task, mon, task_creation); 41 ltl_atoms_fetch(task, mon); 42 } 43 44 static void handle_task_newtask(void *data, struct task_struct *task, u64 flags) 45 { 46 ltl_task_init(task, true); 47 } 48 49 static int ltl_monitor_init(void) 50 { 51 struct task_struct *g, *p; 52 int ret, cpu; 53 54 ret = rv_get_task_monitor_slot(); 55 if (ret < 0) 56 return ret; 57 58 ltl_monitor_slot = ret; 59 60 rv_attach_trace_probe(name, task_newtask, handle_task_newtask); 61 62 read_lock(&tasklist_lock); 63 64 for_each_process_thread(g, p) 65 ltl_task_init(p, false); 66 67 for_each_present_cpu(cpu) 68 ltl_task_init(idle_task(cpu), false); 69 70 read_unlock(&tasklist_lock); 71 72 return 0; 73 } 74 75 static void ltl_monitor_destroy(void) 76 { 77 rv_detach_trace_probe(name, task_newtask, handle_task_newtask); 78 79 tracepoint_synchronize_unregister(); 80 rv_put_task_monitor_slot(ltl_monitor_slot); 81 ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; 82 } 83 84 static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon) 85 { 86 CONCATENATE(trace_error_, MONITOR_NAME)(task); 87 rv_react(&rv_this, "rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n", 88 task->comm, task->pid); 89 } 90 91 static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon) 92 { 93 if (rv_ltl_all_atoms_known(mon)) 94 ltl_start(task, mon); 95 } 96 97 static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value) 98 { 99 __clear_bit(atom, mon->unknown_atoms); 100 if (value) 101 __set_bit(atom, mon->atoms); 102 else 103 __clear_bit(atom, mon->atoms); 104 } 105 106 static void 107 ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state) 108 { 109 const char *format_str = "%s"; 110 DECLARE_SEQ_BUF(atoms, 64); 111 char states[32], next[32]; 112 int i; 113 114 if (!CONCATENATE(CONCATENATE(trace_event_, MONITOR_NAME), _enabled)()) 115 return; 116 117 snprintf(states, sizeof(states), "%*pbl", RV_MAX_BA_STATES, mon->states); 118 snprintf(next, sizeof(next), "%*pbl", RV_MAX_BA_STATES, next_state); 119 120 for (i = 0; i < LTL_NUM_ATOM; ++i) { 121 if (test_bit(i, mon->atoms)) { 122 seq_buf_printf(&atoms, format_str, ltl_atom_str(i)); 123 format_str = ",%s"; 124 } 125 } 126 127 CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer, next); 128 } 129 130 static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon) 131 { 132 DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0}; 133 134 if (!rv_ltl_valid_state(mon)) 135 return; 136 137 for (unsigned int i = 0; i < RV_NUM_BA_STATES; ++i) { 138 if (test_bit(i, mon->states)) 139 ltl_possible_next_states(mon, i, next_states); 140 } 141 142 ltl_trace_event(task, mon, next_states); 143 144 memcpy(mon->states, next_states, sizeof(next_states)); 145 146 if (!rv_ltl_valid_state(mon)) 147 ltl_illegal_state(task, mon); 148 } 149 150 static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value) 151 { 152 struct ltl_monitor *mon = ltl_get_monitor(task); 153 154 ltl_atom_set(mon, atom, value); 155 ltl_atoms_fetch(task, mon); 156 157 if (!rv_ltl_valid_state(mon)) { 158 ltl_attempt_start(task, mon); 159 return; 160 } 161 162 ltl_validate(task, mon); 163 } 164 165 static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value) 166 { 167 struct ltl_monitor *mon = ltl_get_monitor(task); 168 169 ltl_atom_update(task, atom, value); 170 171 ltl_atom_set(mon, atom, !value); 172 ltl_validate(task, mon); 173 } 174