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