Exclusive queue problem

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)
followerQueue = Semaphore(0)
rendezvous = Semaphore(0)

mutex.wait()
if followers > 0:
followers--
followerQueue.signal()
else:
mutex.signal()

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

mutex.wait()
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)
follower_rendezvous=Semaphore(0)

follower_rendezvous.wait()
dance()

follower_mutex.wait()
follower_rendezvous.signal()
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?

• We discourage "please check whether my answer is correct" questions, as only "yes/no" answers are possible, which won't help you or future visitors. See here and here. Can you edit your post to ask about a specific conceptual issue you're uncertain about? As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. If you just need someone to check your work, you might seek out a friend, classmate, or teacher. Commented Mar 26, 2016 at 16:37
• @Raphael Should I just add "Could you prove that my solution is correct?" to the question so it is no more "check-my-answer" question? And Ariel answer is more than "yes". Commented Mar 26, 2016 at 17:21
• That would make your question a different kind of bad. You should a specific question about the "original" solution, your solution, or the difference. What was your idea which you think is simpler? Why do you think it is correct? Why do you think the "original" solution is unnecessarily complex? Commented Mar 27, 2016 at 7:45

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.

• Thank you for your proof, but it does not mention that a leader can't be followed by a leader. (So, for example, there can't be three consecutive dance calls from a leader) Or is it obvious? Commented Mar 26, 2016 at 14:12
• See claim 2. Both dancers have to finish before another couple takes the floor. Commented Mar 26, 2016 at 14:17