title: What is the inductive invariant of the simple concurrent program?
body: <p>Here is a simple concurrent program from the article <a href="http://research.microsoft.com/en-us/um/people/lamport/pubs/teaching-concurrency.pdf" rel="nofollow noreferrer">Teaching Concurrency</a> by Leslie Lamport.</p>
  <p>Consider <code>N</code> processes numbered from 0 through <code>N-1</code> in which each process <code>i</code> executes</p>
  <pre><code>x[i] := 1
  y[i] := x[(i - 1) % N]
  </code></pre>
  <p>and stops, where each <code>x[i]</code> initially equals 0. (The reads and writes of each <code>x[i]</code> are assumed to be atomic.)</p>
  <p>This algorithm satisfies the following property: after every process has stopped, <code>y[i]</code> equals 1 for at least
  one process <code>i</code>. It is easy to verify: The last process <code>i</code> to write <code>y[i]</code> must
  set it to 1.</p>
  <p>Then, Lamport remarks that</p>
  <blockquote>
  <p>But that process doesn't set <code>y[i]</code> to 1 because it was the last process to write <code>y</code>.</p>
  <p>The algorithm satisfies this property because it maintains an <strong>inductive invariant</strong>. Do you know what that invariant is? If not, then you do not completely understand why the algorithm satisfies this property.</p>
  </blockquote>
  <p>Therefore,</p>
  <blockquote>
  <p>What is the inductive invariant of the concurrent program?</p>
  </blockquote>