Exclusive queue problem

Question

There is the exclusive queue problem in The Little Book of Semaphores, which is stated as follows:

Imagine that threads represent ballroom dancers and that two kinds of dancers, leaders and followers, wait in two queues before entering the dance floor. When a leader arrives, it checks to see if there is a follower waiting. If so, they can both proceed. Otherwise it waits. Similarly, when a follower arrives, it checks for a leader and either proceeds or waits, accordingly. Also, there is a constraint that each leader can invoke dance concurrently with only one follower, and vice versa.

The author's solution:

leaders = followers = 0
mutex = Semaphore(1)
leaderQueue = Semaphore(0)
followerQueue = Semaphore(0)
rendezvous = Semaphore(0)

def leader_thread():
   mutex.wait()
   if followers > 0:
      followers--
      followerQueue.signal()
   else:
      leaders++
      mutex.signal()
      leaderQueue.wait()

   dance()
   rendezvous.wait()
   mutex.signal()

def follower_thread():
   mutex.wait()
   if leaders > 0:
      leaders--
      leaderQueue.signal()
   else:
      followers++
      mutex.signal()
      followerQueue.wait()

   dance()
   rendezvous.signal()

However, I think there is a simpler solution:

leader_mutex=Semaphore(1)
follower_mutex=Semaphore(1)
leader_rendezvous=Semaphore(0)
follower_rendezvous=Semaphore(0)

def leader_thread():
   leader_mutex.wait()
   leader_rendezvous.signal()
   follower_rendezvous.wait()
   dance()
   leader_mutex.signal()

def follower_thread():
   follower_mutex.wait()
   follower_rendezvous.signal()
   leader_rendezvous.wait()
   dance()
   follower_mutex.signal()

It is quite obvious and very similar to the queue problem solution mentioned in this book, so I wonder why it was not included in the book. Is there something wrong with my solution? Could you prove that my solution is correct?

Answer 1

If you suspect that your solution is right, then try to prove it (since we are not dealing with foundations, e.g. how exactly is time represented in our system, the proof will be somewhat informal, but it is still a good way to convince yourself).

Claim 1: No more than one pair of follower and dancer can be at the dance floor concurrently.

This is obvious, since if we have one dancer and one follower dancing then both locks are acquired, and thus no more dancers are able to continue.

Claim 2: If a pair $(f,l)$ is dancing ($f,l$ are follower and leader correspondingly), no other dancers will be able to dance until both $f,l$ are done.

Obviously at least one of the dancers $f,l$ has to finish for others to be able to join (we need to release at least one lock). Suppose $l$ finishes first. More followers cant join unless $f$ is done (lock), so the next dancer has to be a leader. However, the next leader will be stuck waiting for follower_rendezvous, which will only be signaled when a new follower comes, and for that $f$ must finish dancing as well (to release the lock).

Claims 1,2, together with the observation that a pair of follower and dancer are able to dance concurrently, concludes the proof.