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? 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). > 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. > > 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. -- Daniel but hey we can extend it somehow :) . i.e. we reach the > final state in bounded time. > > Let me know your thoughts and thanks! > > - Joel >
|