ltl_monitor.h

  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)
 20static struct rv_monitor RV_MONITOR_NAME;
 21
 22static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
 23
 24static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
 25static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation);
 26
 27static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
 28{
 29	return &task->rv[ltl_monitor_slot].ltl_mon;
 30}
 31
 32static 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
 45static void handle_task_newtask(void *data, struct task_struct *task, u64 flags)
 46{
 47	ltl_task_init(task, true);
 48}
 49
 50static 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
 76static void ltl_monitor_destroy(void)
 77{
 78	rv_detach_trace_probe(name, task_newtask, handle_task_newtask);
 79
 80	rv_put_task_monitor_slot(ltl_monitor_slot);
 81	ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
 82}
 83
 84static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon)
 85{
 86	CONCATENATE(trace_error_, MONITOR_NAME)(task);
 87	rv_react(&RV_MONITOR_NAME, "rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n",
 88		 task->comm, task->pid);
 89}
 90
 91static 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
 97static 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
106static void
107ltl_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
130static 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
150static 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
165static 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}