This self test is about analyzing a concurrent system in which a collection of agents, each with access to two sensor readings, computes the average sensor reading. An extension of the problem, given at the end of this page, considers a general case in which agents have access to arbitrary subsets of sensor readings. Later sections describe algorithms in which the state space is continuous and the state evolves over continuous time; we use differential equations to represent continuous state transions and Lyapunov functions to prove progress as opposed to discrete transitions and variant functions.
We are given a connected undirected graph in which each vertex represents a sensor and each edge represents an agent. Sensor \(j\) reading is a scalar value \(t_{j}\). Initially the value of \(t_{j}\) is \(t_{j}^{0}\) where \(t_{j}^{0}\) is a measurement made by sensor \(j\). The specification of the algorithm is that the computation must terminate, and at termination each sensor value must approximately equal the average of all the sensor readings.
Specification
We are given a positive constant \(\epsilon\) which determines the accuracy of the result. Let \(avg(X)\) be the average of the elements of \(X\). The specification is that at termination, the following predicates must hold, where \(t\) is the vector whose elements are sensor readings \(t_{j}\).\( avg(t) = avg(t^{0}) \)
\(t_{i}\) and \(t_{j}\) are sufficiently close for all edges \(i,j\):
\( \forall \; \textrm{edges} \; (i, j): \; |t_{i} - t_{j}| < \epsilon \)
\( \textbf{if} \; |t_{i} - t_{j}| \geq \epsilon \; \textbf{then} \; t_{i} = t_{j} = (t_{i} + t_{j})/2.0 \)
In this example, agents have no local variables; agents have no state. The state of the system is given by the values of the shared variables. Let \(t\) be the vector whose \(j\)-th element is \(t_{j}\). Then the system state is \(t\). The timeline diagram consists of lines for each shared variable.
The proof of the following invariant is straightforward.
\( avg(t) = avg(t^{0}) \)
Part 1: Invariant holds Initially
Trivially:\( avg(t^{0}) = avg(t^{0}) \)
Part 2: Invariant is Stable, i.e., it is maintained at every step
This is obvious because the sum of \(t_{i}, t_{j}\) remains unchanged when they are replaced by their midpoints. This level of informality is acceptable.For a more formal proof, we will prove the following Hoare triple for all \(i, j\) where the guard holds. (The triple holds even if the guard is False, but that is irrelevant.)
For all \(k\)
\(
\{t_{i} + t_{j} = k\} \quad t_{i}, t_{j} = avg(t_{i}, t_{j}), avg(t_{i},
t_{j}) \quad \{t_{i} + t_{j} = k\}
\)
Substitute \(avg(t_{i}, t_{j})\) for \(t_{i}\) and \(t_{j}\) in the post condition to get the weakest precondition. Therefore the weakest precondition is:
\( avg(t_{i}, t_{j}) + avg(t_{i}, t_{j}) = k \)
which simplifies to
\( t_{i} + t_{j} = k \)
The given precondition implies the weakest precondition (indeed, the given precondition is the weakest precondition) and so the Hoare triple holds.
A variant function \(f\) is:
\(f \; = \; \sum_{j} t_{j}^{2} /2 \)
This function has the following properties:A more rigorous proof is as follows. At termination all guards are false. Therefore, at termination, for all edges \(\{i, j\}\) in the graph,
\( |t_{i} - t_{j}| < \epsilon \)
K. Mani Chandy, Emeritus Simon Ramo Professor, California Institute of Technology