On Wed, Oct 5, 2022 at 12:07 PM Daniel Bristot de Oliveira <bristot@xxxxxxxxxx> wrote: > > On 10/3/22 22:35, Joel Fernandes wrote: > > Hi Daniel, > > I was thinking about your RV for a recent problem. > > > > Basically, we want to check for state transitions on a per-RCU > > callback basis. For example, we want to verify that for certain types > > of RCU callback, there is no chance of a scheduler wake up happening > > (provided such wake up happens for non-hardIRQ context). > > ack. > > > > > This means every RCU callback in flight needs its own automaton which > > is created when the callback is queued and destroyed when the callback > > is executed. > > do you have a "structure callback?" or could attach some extra info into it? Unfortunately no, we have rcu_head but the idea is to do this without having to grow it. In theory, you can do this with a hashtable maintained by RV and use the callback function as key, with value being automata. > There cannot be a single global automaton. And we have to > > make transitions for different automaton depending on their state. > > > > I bet you have already thought of something like this for tasks where > > you need a per-task automaton instead of a global one for some use > > case which requires tracking each task separately. > > Yep! we do have per task monitors (already). Nice. This depends on growing task_struct though right? > > We can implement this in RCU itself, however it will be ugly due to > > CONFIG options. And also we cannot do it easily in production. On the > > other hand, with RV, we could simply have RV watch the tracepoints and > > verify them. It will be clean. > > So, I am not sure if I got the problem here. So, you are saying that it will > be easier with RV. Right? > > If you need one monitor (automata) per task, we have support for it already. > If we need "another type of object," we can add. Yeah I was hoping that with RV, you could already allocate a new automata dynamically or something for a new task/callback/whatever, and then drive that automata using tracepoints. So RV can be a nice place to do this kind of stuff, without adding debugging code to other subsystems. > > This is just 1 usecase (wakeup) , we also want to extend something > > like this to more things, like making sure callbacks execute in a time > > bounded fashion. > > > I know verifying temporal properties doesn't directly > > fall under RV, > > temporal or order or temporal of time? For temporal order yep we have it (I > se an overload of this term here... haha). For time, we can add additional > structure to transform them into logical events. Yes, sorry I mean time. So time from when callback queued to when it is invoked falls within a bounded time period. But more urgently what we need is: For a certain type of callback that is invoked, check if the callback does a scheduler wake up. That is - doing a wake up when this type of callback is called is a BAD state. This can be done purely using tracepoints: - We have to add a new tracepoint to call_rcu() for the new callback type (the type being Lazy). - We have to add a new tracepoint for when callback invocation ends (for invocation start, we already have trace_rcu_invoke_callback). Then hook up RV to all of these, and verify that no scheduler_wakeup can happen during the invocation of a Lazy callback. But it has to be done on a per-callback basis. On the other hand, we can simplify it to a single automata by setting a per-cpu state for whenever a Lazy callback is invoked. But the problem is we have no idea that a callback is lazy when we are invoking it. Thanks.
|