为了验证哲学家就餐问题解决方法的正确性,需枚举所有可能的访问情况。以方案三为例,方案三伪代码如下:
void philosopher(int i) // 哲学家编号:0 - 4
while(TRUE) {
think( ); // 哲学家在思考
if (i%2 == 0) {
P(fork[i]); // 去拿左边的叉子
P(fork[(i + 1) % N]); // 去拿右边的叉子
} else {
P(fork[(i + 1) % N]); // 去拿右边的叉子
P(fork[i]); // 去拿左边的叉子
}
eat( ); // 吃面条中….
V(fork[i]); // 放下左边的叉子
V(fork[(i + 1) % N]); // 放下右边的叉子
}
按照某一时刻停止思考开始拿叉子的哲学家人数n来分类:
n=0时,不会出现死锁。
n=1时,不会出现死锁。
n=2时,若两人不相邻,则不会出现死锁
若两人相邻,
若两人序号是(0,1)或(2,3),则先拿第一个叉子的人吃面,另一人等待前一人吃完面放下叉子后吃面,不会出现死锁;
若两人序号是(1,2)或(3,4),则先拿第二个叉子的人吃面,另一人等待前一人吃完面放下叉子后吃面,不会出现死锁;
若两人序号是(4,0),
若0号拿第二把叉子先于4号拿第一把叉子,则0号先吃面,4号等待0号吃完面放下叉子后吃面,不会出现死锁;
若0号拿第二把叉子晚于4号拿第一把叉子,则4号先吃面,0号等待4号吃完面放下叉子后吃面,不会出现死锁;
n=3时,若3个人连续,则每相邻两人间的吃面顺序同n=2的情况,由于未构成环路,因此不会出现死锁;
否则2个人连续1人不连续,不连续的人可以吃面,连续的两个人吃面顺序同n=2的情况,不会出现死锁;
n=4时,4个人必连续,每相邻两人间的吃面顺序同n=2的情况,由于未构成环路,因此不会出现死锁;
n=5时,若有一个人同时拿到两把叉子,则该哲学家可以吃面,吃完面后同n=4的情况,不会出现死锁;
若无人同时拿到两把叉子,由于0号先拿左叉子,1号先拿右叉子,因此0号与1号无法同时拿一把叉子,同理2号与3号无法同时拿一把叉子。
若1号与2号中至少有一个人拿到了第一把叉子,则1号与2号必有一人可以拿到1号与2号中间那把叉子,即必有一人可以拿到两把叉子,该哲学家可以吃面,吃完面后同n=4的情况,不会出现死锁;
否则1号与2号均未拿到叉子,而0号与3号拿到一把叉子,此时4号左右还剩两把叉子。
若4号拿到这两把叉子则该哲学家可以吃面,吃完面后同n=4的情况,不会出现死锁;
否则0号或3号必有一人可以拿到第二把叉子,该哲学家可以吃面,吃完面后同n=4的情况,不会出现死锁;
综上所述,枚举所有情况后方案三均不会产生死锁,说明方案三为正确的解决方案。