베이커리 알고리즘(Bakery Algorithm)에 대한 증명

1. 알고리즘 설명

상점에 들어온 고객들은 대기번호를 하나씩 받는다. 가장 낮은 대기번호를 갖고 있는 고객이 다음번에 빵을 살 수 있다.
불행하게도 베이커리 알고리즘은 두개의 프로세스가 똑같은 번호를 받지 않을 것이란 걸 보장하지 못한다.(두개의 프로세스가 같은 번호를 받을 수 있다.) 이 경우 낮은 이름을 갖고 있는 프로세스가 먼저 처리된다. 즉 대기번호는 같을지라도 프로세스 id가 더 낮은 프로세스가 먼저 생성된 거라고 말할 수 있기에 먼저 처리되는 것이다. 프로세스 id는 유니크하며 전체적으로 순서를 이룬다.
boolean choosing[]
int number[]
CS에 진입하고자 하는 프로세스는 자기 choosing을 true로 세팅하고 자기 number를 다른 프로세스들이 갖고 있는 number값 중에서 가장 큰 값에 1 더한 값으로 세팅한다. 그리고 다시 choosing을 false로 전환한다.(choosing은 대기번호 number를 부여받는 중임을 다른 프로세스에게 알리는 역할을 한다.) 그리고 일일이 다른 프로세스들을 조사하면서 대기하는데, 모든 프로세스의 choosing이 false가 될 때까지(다른 프로세스들이 자기의 대기번호를 받을 때까지 대…(생략)

2. 알고리즘 증명

1) 상호 배제(Mutual exclusion) : 한 프로세스가 자신의 임계구역에서 수행 중이면, 다른 프로세스들은 자신의 임계구역에 들어갈 수 없다.

2) 진행(Progress) : 임계구역에서 실행되는 프로세스가 없는 상태에서 임계구역으로 진입하려고 하는 프로세스들이 있다면, 잔류구역에서 실행되지 않고 있는 프로세스들만 다음에 임계구역으로 진입할 수 있는 대상이 되며, 이 구역은 무한하게 연기할 수 없다.