rv/ltl_monitor.h is the template file used by all LTL monitors. But only
per-task monitor is supported.
Prepare to support for other monitor types:
- Change the monitored target type into an opaque type which will be
defined differently depending on the monitor type. This type is only
defined as struct task_struct * for now.
- Separate out the per-task-specific printf format and arguments, so that
rv_cond_react() can be shared with other monitor types.
No functional change intended.
Signed-off-by: Nam Cao <nam...@linutronix.de>
---
include/linux/rv.h | 1 +
include/rv/ltl_monitor.h | 85 +++++++++++--------
.../trace/rv/monitors/pagefault/pagefault.h | 2 +
kernel/trace/rv/monitors/sleep/sleep.h | 2 +
4 files changed, 55 insertions(+), 35 deletions(-)
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 14410a42faef..175438a22641 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -28,6 +28,7 @@ struct da_monitor {
#ifdef CONFIG_RV_LTL_MONITOR
+#define LTL_TASK_MONITOR 0
/*
* In the future, if the number of atomic propositions or the size of Buchi
* automaton is larger, we can switch to dynamic allocation. For now, the code
diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
index 67031a774e3d..466155fd53e6 100644
--- a/include/rv/ltl_monitor.h
+++ b/include/rv/ltl_monitor.h
@@ -16,49 +16,63 @@
#error "Please include $(MODEL_NAME).h generated by rvgen"
#endif
+#if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
+
+#define TARGET_PRINT_FORMAT "%s[%d]"
+#define TARGET_PRINT_ARGS(task) task->comm, task->pid
+
+typedef struct task_struct *monitor_target;
+
+#endif
+
#ifdef CONFIG_RV_REACTORS
#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
static struct rv_monitor RV_MONITOR_NAME;
-static void rv_cond_react(struct task_struct *task)
+static void rv_cond_react(monitor_target target)
{
if (!rv_reacting_on() || !RV_MONITOR_NAME.react)
return;
- RV_MONITOR_NAME.react("rv: "__stringify(MONITOR_NAME)": %s[%d]:
violation detected\n",
- task->comm, task->pid);
+
+ RV_MONITOR_NAME.react(
+ "rv: "__stringify(MONITOR_NAME)": "TARGET_PRINT_FORMAT":
violation detected\n",
+ TARGET_PRINT_ARGS(target));
}
#else
-static void rv_cond_react(struct task_struct *task)
+static void rv_cond_react(monitor_target target)
{
}
#endif
-static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
+static void ltl_atoms_fetch(monitor_target target, struct ltl_monitor *mon);
+static void ltl_atoms_init(monitor_target target, struct ltl_monitor *mon,
bool target_creation);
-static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
-static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon,
bool task_creation);
+#if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
+static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
-static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
+static struct ltl_monitor *ltl_get_monitor(monitor_target target)
{
- return &task->rv[ltl_monitor_slot].ltl_mon;
+ return &target->rv[ltl_monitor_slot].ltl_mon;
}
+#endif
-static void ltl_task_init(struct task_struct *task, bool task_creation)
+static void ltl_target_init(monitor_target target, bool target_creation)
{
- struct ltl_monitor *mon = ltl_get_monitor(task);
+ struct ltl_monitor *mon = ltl_get_monitor(target);
memset(&mon->states, 0, sizeof(mon->states));
for (int i = 0; i < LTL_NUM_ATOM; ++i)
__set_bit(i, mon->unknown_atoms);
- ltl_atoms_init(task, mon, task_creation);
- ltl_atoms_fetch(task, mon);
+ ltl_atoms_init(target, mon, target_creation);
+ ltl_atoms_fetch(target, mon);
}
+#if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
static void handle_task_newtask(void *data, struct task_struct *task, unsigned
long flags)
{
- ltl_task_init(task, true);
+ ltl_target_init(task, true);
}
static int ltl_monitor_init(void)
@@ -77,10 +91,10 @@ static int ltl_monitor_init(void)
read_lock(&tasklist_lock);
for_each_process_thread(g, p)
- ltl_task_init(p, false);
+ ltl_target_init(p, false);
for_each_present_cpu(cpu)
- ltl_task_init(idle_task(cpu), false);
+ ltl_target_init(idle_task(cpu), false);
read_unlock(&tasklist_lock);
@@ -94,17 +108,18 @@ static void ltl_monitor_destroy(void)
rv_put_task_monitor_slot(ltl_monitor_slot);
ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
}
+#endif
-static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor
*mon)
+static void ltl_illegal_state(monitor_target target, struct ltl_monitor *mon)
{
- CONCATENATE(trace_error_, MONITOR_NAME)(task);
- rv_cond_react(task);
+ CONCATENATE(trace_error_, MONITOR_NAME)(target);
+ rv_cond_react(target);
}
-static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor
*mon)
+static void ltl_attempt_start(monitor_target target, struct ltl_monitor *mon)
{
if (rv_ltl_all_atoms_known(mon))
- ltl_start(task, mon);
+ ltl_start(target, mon);
}
static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom,
bool value)
@@ -117,7 +132,7 @@ static inline void ltl_atom_set(struct ltl_monitor *mon,
enum ltl_atom atom, boo
}
static void
-ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned
long *next_state)
+ltl_trace_event(monitor_target target, struct ltl_monitor *mon, unsigned long
*next_state)
{
const char *format_str = "%s";
DECLARE_SEQ_BUF(atoms, 64);
@@ -137,10 +152,10 @@ ltl_trace_event(struct task_struct *task, struct
ltl_monitor *mon, unsigned long
}
}
- CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer,
next);
+ CONCATENATE(trace_event_, MONITOR_NAME)(target, states, atoms.buffer,
next);
}
-static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)
+static void ltl_validate(monitor_target target, struct ltl_monitor *mon)
{
DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0};
@@ -152,35 +167,35 @@ static void ltl_validate(struct task_struct *task, struct
ltl_monitor *mon)
ltl_possible_next_states(mon, i, next_states);
}
- ltl_trace_event(task, mon, next_states);
+ ltl_trace_event(target, mon, next_states);
memcpy(mon->states, next_states, sizeof(next_states));
if (!rv_ltl_valid_state(mon))
- ltl_illegal_state(task, mon);
+ ltl_illegal_state(target, mon);
}
-static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool
value)
+static void ltl_atom_update(monitor_target target, enum ltl_atom atom, bool
value)
{
- struct ltl_monitor *mon = ltl_get_monitor(task);
+ struct ltl_monitor *mon = ltl_get_monitor(target);
ltl_atom_set(mon, atom, value);
- ltl_atoms_fetch(task, mon);
+ ltl_atoms_fetch(target, mon);
if (!rv_ltl_valid_state(mon)) {
- ltl_attempt_start(task, mon);
+ ltl_attempt_start(target, mon);
return;
}
- ltl_validate(task, mon);
+ ltl_validate(target, mon);
}
-static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum
ltl_atom atom, bool value)
+static void __maybe_unused ltl_atom_pulse(monitor_target target, enum ltl_atom
atom, bool value)
{
- struct ltl_monitor *mon = ltl_get_monitor(task);
+ struct ltl_monitor *mon = ltl_get_monitor(target);
- ltl_atom_update(task, atom, value);
+ ltl_atom_update(target, atom, value);
ltl_atom_set(mon, atom, !value);
- ltl_validate(task, mon);
+ ltl_validate(target, mon);
}
diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.h
b/kernel/trace/rv/monitors/pagefault/pagefault.h
index c580ec194009..cc825be51ffc 100644
--- a/kernel/trace/rv/monitors/pagefault/pagefault.h
+++ b/kernel/trace/rv/monitors/pagefault/pagefault.h
@@ -11,6 +11,8 @@
#define MONITOR_NAME pagefault
+#define LTL_MONITOR_TYPE LTL_TASK_MONITOR
+
enum ltl_atom {
LTL_PAGEFAULT,
LTL_RT,
diff --git a/kernel/trace/rv/monitors/sleep/sleep.h
b/kernel/trace/rv/monitors/sleep/sleep.h
index 2ab46fd218d2..c3752bc9f93f 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.h
+++ b/kernel/trace/rv/monitors/sleep/sleep.h
@@ -11,6 +11,8 @@
#define MONITOR_NAME sleep
+#define LTL_MONITOR_TYPE LTL_TASK_MONITOR
+
enum ltl_atom {
LTL_ABORT_SLEEP,
LTL_BLOCK_ON_RT_MUTEX,
--
2.39.5
