title: Filter Lock Algorithm
body: <p>I'm busy looking at the filter lock algorithm for n-thread mutual exclusion and I can't seem to understand line 17 of the code. I understand that it is spinning on a condition but not entirely sure what those conditions are. More specifically what (∃k != me) entails.</p>
  
  <pre><code>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 &lt; n; i++) {
  8         level[i] = 0;
  9     }
  10 }
  11 public void lock() {
  12     int me = ThreadID.get();
  13     for (int i = 1; i &lt; n; i++) { //attempt level 1
  14     level[me] = i;
  15     victim[i] = me;
  16     // spin while conflicts exist
  17     while ((∃k != me) (level[k] &gt;= i &amp;&amp; victim[i] == me)) {};
  18     }
  19 }
  20 public void unlock() {
  21     int me = ThreadID.get();
  22     level[me] = 0;
  23 }
  24 }
  </code></pre>