19 lines
2.1 KiB
Markdown
19 lines
2.1 KiB
Markdown
栈式页面置换算法不会出现belady现象的证明
|
||
=====================================
|
||
|
||
## LRU算法
|
||
|
||
对于`最近最久未使用算法(LRU, Least Recently Used)`，是不会出现`belady`异常(belady anomaly)的，证明如下：
|
||
|
||
设分配给当前进程的页面数量为`n`，令$S_n$为当前时刻`t`，某个进程驻留在内存中的所有页面的集合。要证明`LRU`不会出现`belady`异常，即证对于任意的`k > 0`，给进程分配的页面数量为`n + k`时，对于同一个页面访问序列，$S_n$总是$S_{n+k}$的一个子集。不妨简单地令`k = 1`，`k > 1`的情况同理。以下归纳地证明该结论。
|
||
|
||
- `t = 1`时，$S_n$和$S_{n+1}$都只包含同一个页面，结论成立。
|
||
- 假设$t < t_{k - 1}$时，该结论成立。
|
||
- 当$t = t_k$时，设此时访问的页面为$c_k$。以下分为三种情况讨论：
|
||
+ $c_k \in S_n$，则显然$c_k \in S_{n+1}$，访问$c_k$不会引发缺页异常，因此访问$c_k$后假设显然成立。
|
||
+ $c_k \in S_{n+1}$但是$c_k \notin S_n$，此时对于序列$S_n$会引发一次缺页异常，导致其中一个页面被换出以及$c_k$被换入，此时仍然保持$S_n \subset S_{n+1}$，假设成立。
|
||
+ $c_k \notin S_n$并且$c_k \notin S_{n+1}$，此时两个集合都会产生缺页异常。假设此时$S_n$中被换出的页面为$x_1$，若$S_{n+1}$被换出的页面也是$x_1$，则假设仍然成立；否则，设$S_{n+1}$中被换出的页面为$x_2, x_2 \neq x_1$，由于是采用`LRU`算法，则$x_2$必然是比$x_1$`更久未被使用`的页面，倘若$x_2 \in S_n$，则$S_n$中被换出的页面也应该是$x_2$，而不是使用相对频繁的$x_1$，这与假设矛盾，故$x_2 \notin S_n$，缺页异常处理完毕后原假设仍然成立。
|
||
|
||
证毕。
|
||
|
||
实际上，对于`最优置换算法`(OPT)，以及`恢复计数`的`最不常用算法`(LFU, Least Frequently Used)，都可以类似地证明不会出现`belady`异常。然而，其他的页面置换算法，包括`FIFO`，`时钟置换算法`(clock)以及`改进的时钟置换算法`，`不恢复计数`的`最不常用算法`，则都可以构造出出现`belady`异常的实例。 |