include/rv/ltl_monitor.h

Source file repositories/reference/linux-study-clean/include/rv/ltl_monitor.h

File Facts

System
Linux kernel
Corpus path
include/rv/ltl_monitor.h
Extension
.h
Size
4335 bytes
Lines
175
Domain
Repository Root And Misc
Bucket
include
Inferred role
Repository Root And Misc: implementation source
Status
source implementation candidate

Why This File Exists

Top-level or miscellaneous repository surface. Use this as map coverage unless a later manual pass promotes the file into a deeper subsystem dossier.

Dependency Surface

Detected Declarations

Annotated Snippet

if (test_bit(i, mon->atoms)) {
			seq_buf_printf(&atoms, format_str, ltl_atom_str(i));
			format_str = ",%s";
		}
	}

	CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer, next);
}

static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)
{
	DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0};

	if (!rv_ltl_valid_state(mon))
		return;

	for (unsigned int i = 0; i < RV_NUM_BA_STATES; ++i) {
		if (test_bit(i, mon->states))
			ltl_possible_next_states(mon, i, next_states);
	}

	ltl_trace_event(task, mon, next_states);

	memcpy(mon->states, next_states, sizeof(next_states));

	if (!rv_ltl_valid_state(mon))
		ltl_illegal_state(task, mon);
}

static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)
{
	struct ltl_monitor *mon = ltl_get_monitor(task);

	ltl_atom_set(mon, atom, value);
	ltl_atoms_fetch(task, mon);

	if (!rv_ltl_valid_state(mon)) {
		ltl_attempt_start(task, mon);
		return;
	}

	ltl_validate(task, mon);
}

static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)
{
	struct ltl_monitor *mon = ltl_get_monitor(task);

	ltl_atom_update(task, atom, value);

	ltl_atom_set(mon, atom, !value);
	ltl_validate(task, mon);
}

Annotation

Implementation Notes