1 /* SPDX-License-Identifier: GPL-2.0 */
28 			      task->comm, task->pid);  in rv_cond_react()
38 static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
39 static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation);
43 	return &task->rv[ltl_monitor_slot].ltl_mon;  in ltl_get_monitor()
48 	struct ltl_monitor *mon = ltl_get_monitor(task);  in ltl_task_init()  local
50 	memset(&mon->states, 0, sizeof(mon->states));  in ltl_task_init()
52 	for (int i = 0; i < LTL_NUM_ATOM; ++i)  in ltl_task_init()
53 		__set_bit(i, mon->unknown_atoms);  in ltl_task_init()
55 	ltl_atoms_init(task, mon, task_creation);  in ltl_task_init()
56 	ltl_atoms_fetch(task, mon);  in ltl_task_init()
70 	if (ret < 0)  in ltl_monitor_init()
87 	return 0;  in ltl_monitor_init()
98 static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon)  in ltl_illegal_state()  argument
104 static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon)  in ltl_attempt_start()  argument
106 	if (rv_ltl_all_atoms_known(mon))  in ltl_attempt_start()
107 		ltl_start(task, mon);  in ltl_attempt_start()
110 static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value)  in ltl_atom_set()  argument
112 	__clear_bit(atom, mon->unknown_atoms);  in ltl_atom_set()
114 		__set_bit(atom, mon->atoms);  in ltl_atom_set()
116 		__clear_bit(atom, mon->atoms);  in ltl_atom_set()
120 ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state)  in ltl_trace_event()  argument
130 	snprintf(states, sizeof(states), "%*pbl", RV_MAX_BA_STATES, mon->states);  in ltl_trace_event()
133 	for (i = 0; i < LTL_NUM_ATOM; ++i) {  in ltl_trace_event()
134 		if (test_bit(i, mon->atoms)) {  in ltl_trace_event()
143 static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)  in ltl_validate()  argument
145 	DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0};  in ltl_validate()
147 	if (!rv_ltl_valid_state(mon))  in ltl_validate()
150 	for (unsigned int i = 0; i < RV_NUM_BA_STATES; ++i) {  in ltl_validate()
151 		if (test_bit(i, mon->states))  in ltl_validate()
152 			ltl_possible_next_states(mon, i, next_states);  in ltl_validate()
155 	ltl_trace_event(task, mon, next_states);  in ltl_validate()
157 	memcpy(mon->states, next_states, sizeof(next_states));  in ltl_validate()
159 	if (!rv_ltl_valid_state(mon))  in ltl_validate()
160 		ltl_illegal_state(task, mon);  in ltl_validate()
165 	struct ltl_monitor *mon = ltl_get_monitor(task);  in ltl_atom_update()  local
167 	ltl_atom_set(mon, atom, value);  in ltl_atom_update()
168 	ltl_atoms_fetch(task, mon);  in ltl_atom_update()
170 	if (!rv_ltl_valid_state(mon)) {  in ltl_atom_update()
171 		ltl_attempt_start(task, mon);  in ltl_atom_update()
175 	ltl_validate(task, mon);  in ltl_atom_update()
180 	struct ltl_monitor *mon = ltl_get_monitor(task);  in ltl_atom_pulse()  local
184 	ltl_atom_set(mon, atom, !value);  in ltl_atom_pulse()
185 	ltl_validate(task, mon);  in ltl_atom_pulse()