E.9 Summary

Promela is a very powerful tool for validating small parallel algorithms. It is a useful tool in the parallel kernel hacker's toolbox, but it should not be the only tool. The QRCU experience is a case in point: given the Promela validation, the proof of correctness, and several rcutorture runs, I now feel reasonably confident in the QRCU algorithm and its implementation. But I would certainly not feel so confident given only one of the three!

Nevertheless, if your code is so complex that you find yourself relying too heavily on validation tools, you should carefully rethink your design. For example, a complex implementation of the dynticks interface for preemptible RCU that was presented in Section [*] turned out to have a much simpler alternative implementation, as discussed in Section [*]. All else being equal, a simpler implementation is much better than a mechanical proof for a complex implementation!


Paul E. McKenney 2011-12-16