How does this swap instruction achieves mutual exclusion, progress and bounded waiting if it does?

Question

do 

{
key=true;
while(key==true)
{
swap(&lock,&key);
}
critical section
lock=false;
Remainder Section
}while(true);

void swap(boolean *a, boolean *b)
{
boolean temp=*a;
*a=*b;
*b=temp;
}

How do I prove if it satisfied mutual exclusion, progress and bounded waiting?

The swap is built into hardware and is atomic.

1. Mutual Exclusion

Definition:

No two cooperating processes can enter into their critical section at the same time. For example, if a process P1 is executing in its critical section, no other cooperating process can enter in the critical section until P1 finishes with it.

2. Progress

Definition:

If no process is in its CS and there are one or more processes that wish to enter their CS, this selection cannot be postponed indefinitely.

No process in remainder section can participate in this decision.

3. Bounded Waiting

Definition:

After a prcess P has made a request to enter its CS, there is a limit on the number of times that the other processes are allowed to enter their CS, before P's request is granted.

Tests

Mutual Exclusion is achieved in my opinion.

P0 tries to enter CS.
Sets key=true
swaps lock and key; now key=false and lock=true(LOCKED)
since key=false, it gets to CS.

Say P1 context switched appeared and wants to enter CS.
Sets key=true.
Swaps lock and key. Both are true as CS is locked at the moment.

So, mutual exclusion is achieved.



Progress is achieved in my opinion.
Say P0 is in remainder section.
lock=false
P1 wants to enter CS.
key=true
Swap lock with key
lock=true and key=false
Loop breaks and P1 enter CS

Bounded waiting is not achieve in my opinion.
P0 exits CS. 
lock=false
P0 wants to enter CS again.
It can enter forever.

Correct me if I'm wrong. And please share better ways to prove it if you've them. These are some tough concepts of computer science and it'd be great if we could make this even 1% easy to future learners.

Answer 1

1. Mutual exclusion: the while loop is only executed with key=true so it can only set lock=true. As the swap is atomic, only one process can get a false, which is immediately "consumed". Only at the end of the critical section is the false restored. That false acts as a unique token.

2. Progress: if lock=false, the first process that performs a swap will enter.

3. Bounded waiting: the other processes can indeed lock out the given process by always taking the token first when it is available.