During my presentation entitled Verifying Parallel Software: Can Theory Meet Practice? at the Verification of Concurrent Data-Structures (Verico) workshop in late January 2011, I was asked a number of interesting questions:
My answers, in some cases with l'esprit d'escalier embellishments, are listed below.
Yes, there are, for example, in the upcoming user-level RCU paper in IEEE Transactions on Parallel and Distributed Systems.
However, in a later talk, Victor Luchangco noted that although some transactional-memory implementations had been model-checked, none had yet been proven correct. It is therefore quite possible that our proofs would not pass muster in the research crowd.
Although I can prove an algorithm by hand, I am not going prove much of anything by hand about the full 10+MLOC of the Linux kernel source code. Automated validation therefore has an important role to play in large source bases. Richard Bornat's name came up, just as it did in an earlier posting.
Of course, anyone who has used RCU knows that the answer to this question must be “no” — after all, you need some synchronization mechanism to coordinate RCU updates. Furthermore, there are more than 20 times as many uses of locking in the Linux kernel as there are of RCU. So, if locking is the hammer in the Linux kernel hacker's toolbox, then RCU is the screwdriver.
The semantics shown on slide 16 of my presentation gives the fundamental property of RCU. Additional properties are shown in the user-level RCU paper in IEEE Transactions on Parallel and Distributed Systems.