On Wed, 2025-08-06 at 10:46 +0200, Nam Cao wrote: > On Wed, Aug 06, 2025 at 10:15:48AM +0200, Gabriele Monaco wrote: > > I didn't make it on time before your V2, I assume you solved > > already so > > you might ignore this. > > > > You kinda have something like the da_monitor_enabled: the > > rv_ltl_all_atoms_known > > > > I wonder if you could define LTL_RT_TASK_ENQUEUED only when you > > actually know it (or are reasonably sure based on your internal > > counter). Or at least not set all atoms until the monitor is fully > > set > > up. > > The rv_ltl_all_atoms_known() thingy is for situation where relevant > tracepoints have not been hit yet. > > This case is slightly different, the tracepoint has been hit. And it > is not clear how to implement the "reasonably sure based on your > internal counter" part. > > > Anyway reordering the tracepoints registration is likely necessary > > whatever you do, but I'm afraid a problem like this can occur > > pretty > > often with this type of monitors. > > What I have in v2 is a workaround only, by reordering the tracepoint > registrations. > > The root problem is not specific to this monitor, but all LTL > monitors. My idea for the real fix is the untested patch below. I > will send it separately. It is not urgent, so I can wait for your DA > macro removal patch to be merged first. >
Alright, I get it, let's continue with the workaround for now, I'm going to have a look at your V2. Thanks, Gabriele > As I'm sending the patch to you, I realized that the patch > effectively nullifies ltl_atoms_init(). So I will need to fix that > up.. > > Nam > > commit 7fbb9a99f1a95e5149d476fa3d83a60be1a9a579 > Author: Nam Cao <[email protected]> > Date: Tue Aug 5 22:47:49 2025 +0200 > > rv: Share the da_monitor_enabled_##name() function with LTL > > The LTL monitors also need the functionality that > da_monitor_enabled_##name() offers. > > This is useful to prevent the automaton from being executed > before the > monitor is completely enabled, preventing the situation where the > monitors run before all tracepoints are registered. This > situation can > cause a false positive error, because the monitors do not see > some > events and do not validate properly. > > Pull da_monitor_enabled_##name() to be in the common header, and > use > it for both LTL and DA. > > Signed-off-by: Nam Cao <[email protected]> > > diff --git a/include/linux/rv.h b/include/linux/rv.h > index 1aa01d98e390..8a885b3665a8 100644 > --- a/include/linux/rv.h > +++ b/include/linux/rv.h > @@ -119,6 +119,14 @@ int rv_register_monitor(struct rv_monitor > *monitor, struct rv_monitor *parent); > int rv_get_task_monitor_slot(void); > void rv_put_task_monitor_slot(int slot); > > +static inline bool rv_monitor_enabled(struct rv_monitor *monitor) > +{ > + if (unlikely(!rv_monitoring_on())) > + return 0; > + > + return likely(monitor->enabled); > +} > + > #ifdef CONFIG_RV_REACTORS > bool rv_reacting_on(void); > int rv_unregister_reactor(struct rv_reactor *reactor); > diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h > index 17fa4f6e5ea6..92b8a8c0b9b7 100644 > --- a/include/rv/da_monitor.h > +++ b/include/rv/da_monitor.h > @@ -74,29 +74,12 @@ static inline bool da_monitoring_##name(struct > da_monitor *da_mon) \ > return da_mon- > >monitoring; \ > } > \ > > \ > - > /* > \ > - * da_monitor_enabled_##name - checks if the monitor is > enabled \ > - > */ > \ > -static inline bool > da_monitor_enabled_##name(void) > \ > - > { > \ > - /* global switch > */ \ > - if > (unlikely(!rv_monitoring_on())) > \ > - return > 0; \ > - > > \ > - /* monitor enabled > */ \ > - if > (unlikely(!rv_##name.enabled)) > \ > - return > 0; \ > - > > \ > - return > 1; > \ > - > } > \ > - > > \ > /* > \ > * da_monitor_handling_event_##name - checks if the monitor is ready > to handle events \ > > */ > \ > static inline bool da_monitor_handling_event_##name(struct > da_monitor *da_mon) \ > { > \ > - > > \ > - if > (!da_monitor_enabled_##name()) > \ > + if > (!rv_monitor_enabled(&rv_##name)) > \ > return > 0; \ > > \ > /* monitor is actually monitoring > */ \ > @@ -390,7 +373,7 @@ static inline bool > da_handle_start_event_##name(enum events_##name > event) \ > { > \ > struct da_monitor > *da_mon; \ > > \ > - if > (!da_monitor_enabled_##name()) > \ > + if > (!rv_monitor_enabled(&rv_##name)) > \ > return > 0; \ > > \ > da_mon = > da_get_monitor_##name(); > \ > @@ -415,7 +398,7 @@ static inline bool > da_handle_start_run_event_##name(enum events_##name event) > { > \ > struct da_monitor > *da_mon; \ > > \ > - if > (!da_monitor_enabled_##name()) > \ > + if > (!rv_monitor_enabled(&rv_##name)) \ > return > 0; \ > > \ > da_mon = > da_get_monitor_##name(); > \ > @@ -475,7 +458,7 @@ da_handle_start_event_##name(struct task_struct > *tsk, enum events_##name event) > { > \ > struct da_monitor > *da_mon; \ > > \ > - if > (!da_monitor_enabled_##name()) > \ > + if > (!rv_monitor_enabled(&rv_##name)) > \ > return > 0; \ > > \ > da_mon = > da_get_monitor_##name(tsk); > \ > @@ -501,7 +484,7 @@ da_handle_start_run_event_##name(struct > task_struct *tsk, enum events_##name eve > { > \ > struct da_monitor > *da_mon; \ > > \ > - if > (!da_monitor_enabled_##name()) > \ > + if > (!rv_monitor_enabled(&rv_##name)) > \ > return > 0; \ > > \ > da_mon = > da_get_monitor_##name(tsk); > \ > diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h > index 29bbf86d1a52..85a3d07a0303 100644 > --- a/include/rv/ltl_monitor.h > +++ b/include/rv/ltl_monitor.h > @@ -16,6 +16,8 @@ > #error "Please include $(MODEL_NAME).h generated by rvgen" > #endif > > +#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME) > + > #if LTL_MONITOR_TYPE == LTL_TASK_MONITOR > > #define TARGET_PRINT_FORMAT "%s[%d]" > @@ -33,7 +35,6 @@ typedef unsigned int monitor_target; > #endif > > #ifdef CONFIG_RV_REACTORS > -#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME) > static struct rv_monitor RV_MONITOR_NAME; > > static struct ltl_monitor *ltl_get_monitor(monitor_target target); > @@ -156,6 +157,9 @@ static void ltl_attempt_start(monitor_target > target, struct ltl_monitor *mon) > > static inline void ltl_atom_set(struct ltl_monitor *mon, enum > ltl_atom atom, bool value) > { > + if (!rv_monitor_enabled(&RV_MONITOR_NAME)) > + return; > + > __clear_bit(atom, mon->unknown_atoms); > if (value) > __set_bit(atom, mon->atoms);
