I had been searching for this algorithm after I encountered it in lecture 7 of Prof PK Biswas's NPTEL course on OS (who left its analysis as an exercise, without providing the name). Didn't know that it's a Galvin exercise, but thanks to the name of the algorithm, I was able to look it up on Wikipedia, which has a much more intuitive description of the pseudocode.
https://en.wikipedia.org/wiki/Eisenberg_%26_McGuire_algorithm
1. Mutual exclusion: Lines 6-12 in the Wikipedia code guarantee ME. Ensures that only one process gets a turn at the critical section and others are made to wait.
2. Progress: Once some Pj is done with the CS, one of the processes Pi will be able to exit the code section on L6-12, and after checking that no other process is in CS in L18-26, will be able to enter CS while the other processes wait. Only the processes that wish to enter CS will be considered; others will have been marked idle and not considered in the decision.
3. Bounded waiting: We consider all eligible processes in a circular fashion, so any waiting process Pi is bound to get its turn at some point. Although I am not sure of what happens if a process gets stuck in the CS while others wait.