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). 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. 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. 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. 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, 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
|