Self Tests: Earliest Meeting Time

A student wants to schedule a doctoral thesis examination. She wants to find the earliest day at which the professors on her thesis committee can meet.

Associated with professor \(j\) is a function \(f_{j}\) where \(f_{j}(d)\) is the earliest day at, or after, day \(d\) that professor \(j\) can meet. The student starts scheduling on day 0.

Some professors don't talk to others, and some don't listen while others talk. The set of professors form a directed graph in which there is an edge \((j, k)\) exactly when professor \(k\) can read professor \(j\)'s state. We assume that there is an edge \((j, j)\) for all \(j\) because professors do like to hear themselves talk. The graph is strongly connected, i.e, there is directed path from each professor to every professor.

Day \(d\) is a possible meeting time exactly when all professors can meet on day \(d\):
\( \forall j:\; d_{j} = d \)

Professors are busy; so scheduling a thesis committee is difficult. Assume that there is some day, perhaps in the far distant future, at which all professors can meet. Let \(m\) be the earliest possible meeting time.

Specification

Associated with each agent \(j\) is an integer variable \(d_{j}\). Prove that the following iteration terminates in a state in which for all \(j\): \(d_{j} = m\), where \(m\) is the earliest meeting time.

Agent Actions

Initially: \(d_{j} = 0\)

For all edges \((j,k)\):

\( d_{k} < f_{k}(d_{j}) \; \rightarrow \; d_{k} = f_{k}(d_{j}) \)

Self Test: Proof of Correctness

Test 1

Give and prove an invariant of the loop.

Test 2

Prove that the loop terminates by giving a variant function for the loop.

Test 3

Show that the specification holds upon termination of the loop.

Answers

Answer 1

The invariant is: For all \(j\):

\( d_{j} \leq m \)

This condition holds initially because \(m \geq 0\).

If this condition holds when a guarded command with a true guard is executed then the condition continues to hold after the command is executed. The proof is straightforward.

Answer 2

A variant function \(f\) is the sum over all professors \(j\) of the number of days remaining to reach the earliest meeting time from the professor's current estimate of \(d_{j}\):

\( \sum_{j} (m - d_{j}) \)

This function is bounded below. This function takes on integer values. An execution of a guarded command with a true guard reduces the value of this function because it increases \(d_{j}\) for some \(j\).

Answer 3

We are required to show that if the invariant holds and all guards are false then the specification is satisfied.

If all the guards are false then you can show, quite easily, that all the \(d_{j}\) are identical. Let \(d\) be the common value of \(d_{j}\). Because there is an edge from \(j\) back to itself, \(f_{j}(d) = d\). Therefore, \(d\) is a possible meeting time.

From the invariant there exists no meeting time before \(d\), and so the result follows.

---

K. Mani Chandy, Emeritus Simon Ramo Professor, California Institute of Technology