Deadlock and starvation free reentrant readers–writers: A case study combining model checking with theorem proving

The classic readers–writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures each starting and ending with a lock operation. Allowing nesting makes it possible for these procedures to call each other.We considered an existing widely used industrial implementation of the reentrant readers–writers problem. Staying close to the original code, we modelled and analyzed it using a model checker resulting in the detection of a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a specification that was proven with a theorem prover. Furthermore, we studied starvation. Using model checking we found a starvation problem. We have fixed the problem and checked the solution. Combining model checking with theorem proving appeared to be very effective in reducing the time of the verification process.