In a previous colloquium, we presented a new and efficient readers-writer lock with no resource contention between readers, called the Busy-Forbidden Protocol.

For its verification, specifications of its implementation and its less complex external behavior are provided.

However, we are unable to prove the equivalence of these models for more than 7 concurrent threads using mCRL2, due to the statespaces becoming too large to work with.

We now give a general equivalence proof using our new extension of the cones and foci proof framework for divergence-preserving branching bisimilarity.