我正忙着研究 n 线程互斥的过滤器锁定算法,我似乎无法理解代码的第 17 行。我知道它在一个条件下旋转,但不完全确定这些条件是什么。更具体地说, (∃k != me) 意味着什么。
1 class Filter implements Lock {
2 int[] level;
3 int[] victim;
4 public Filter(int n) {
5 level = new int[n];
6 victim = new int[n]; // use 1..n-1
7 for (int i = 0; i < n; i++) {
8 level[i] = 0;
9 }
10 }
11 public void lock() {
12 int me = ThreadID.get();
13 for (int i = 1; i < n; i++) { //attempt level 1
14 level[me] = i;
15 victim[i] = me;
16 // spin while conflicts exist
17 while ((∃k != me) (level[k] >= i && victim[i] == me)) {};
18 }
19 }
20 public void unlock() {
21 int me = ThreadID.get();
22 level[me] = 0;
23 }
24 }