Re: [PATCH v2 13/22] rv: Add support for LTL monitors

Nam Cao
2025-04-11T14:15:24Z

On Fri, Apr 11, 2025 at 01:17:30PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > +struct ltl_monitor {
> > +#ifdef CONFIG_RV_LTL_MONITOR
> > + DECLARE_BITMAP(states, RV_MAX_BA_STATES);
> > + DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
> > + DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
> > +#endif
> > +};
>
> Mmh, we have a lot of those ifdefs in quite inappropriate places, but I
> think we can do better than this.
>
> What about something like:
>
> #ifdef CONFIG_RV_LTL_MONITOR
>
> struct ltl_monitor {
> DECLARE_BITMAP(states, RV_MAX_BA_STATES);
> DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
> DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
> };
>
> static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
> {
> ...
> }
>
> static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
> {
> ...
> }
>
> #else
>
> /*
> * Leave the struct empty not to use up space
> * In a later patch we could do the same for DAs..
> */
> struct ltl_monitor { };
>
> #endif

I have no preference for either, so sure!

> > diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
> > new file mode 100644
> > index 000000000000..78f5a1197665
> > --- /dev/null
> > +++ b/include/rv/ltl_monitor.h
>
> You hate macros don't you? :)

YES!

> Anyway I really like your approach, very neat.

Thank you! I'm very happy to have found a way to escape the macros.

> > +static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
> > +{
> > + return &task->rv[ltl_monitor_slot].ltl_mon;
> > +}
>
> This means ltl monitors only support per-task, right?

Yes.

> It shouldn't take much effort putting an ifdef chain here and defining e.g.
> PER_CPU in the header file to choose a different get_monitor.
> Or directly an ltl_monitor_implicit.h

Yes, either can work.

> I think this patch is ready without it, just trying to brainstorm how we could
> potentially extend this.
>
> I need more time to play with these, but it looks promising.

Thank you,
Nam