# Proof of Manna-Pnueli algorithm for mutual exclusion being incorrect

Suppose we have the Manna-Pnueli algorithm for mutual exclusion:

I was trying to find a sequence that violates mutual exclusion and I came up with this:

1. q1, q3; wantq=-1
2. p1
3. q4, q5; wantq=0
4. q1
5. p2; wantp=-1
6. p4
7. q3; wantq=-1
8. q4
9. p and q in critical section


Is my reasoning correct, supposing if is not atomic?

Also, were it atomic, how would I prove it to be correct? Should I just list all the possible combinations?