previous up next
Go backward to Correctness Theorem
Go up to B.5 Verification
Go forward to Program Properties
RISC-Linz logo

Invariants

In order to formulate the program invariants from which the correctness theorem can be proved, we need to refer to the all the messages that have been ever sent through a channel:

Definition. [Channel Trace] The trace of channel c is a triple (C, inposc, outposc) such that C is an array that holds the stream of all messages that have been sent through c, the next message that will be read by the receiver is stored in C[inposc], and the next message sent by the sender will be written into C[outposc] with inposc <= outposc.

Apparently, a channel c is empty if inposc = outposc.

We may think of a channel trace as an additional data structure where inposc and outposc are initialized as zero; the data structure is updated by every operation c.send(v) as follows:

C[outpos_c] = v;
outpos_c++
In addition the operation v = c.receive() has the effect
inpos_c++

We may then introduce a derived notion:

Definition. [Trace Value] The trace value tvalue(c, from, to) of a channel c in interval [from,to[ is the sum of the values of the messages in the trace of c between (including) `from` and (not including) `to`:
tvalue(c, from, to) := Sumfrom <=k < to mvalue(C[k])

This notion can be used to express the value of a network as follows:

Theorem. [Network Value] The value of a network equals the sum of all initial node deposits plus the sum of the values of all messages being processed by some node plus the sum of the values of the messages received by each node minus the sum of the values of the messages left by each node:
valuenet =
    Sumi (di + mvalue(messagei)) +
    Sumc tvalue(c, inposc, outposc))

Proof: The result follows from the fact that the network value remains constant by the operation of the program; the proof of this proceeds analogously to the proof in Section A.

We now characterize the behavior of the program by the following set of propositions which we have to prove as invariants:

Definition. [Invariants] For every node i, we define the following propositions:
  1. Di (Deposit): the node deposit is non-negative and equals the initial deposit value plus (potentially) the value of the message just received plus the current trace value of all input channels minus the current trace value of all output channels:
    depositi >= 0,
    depositi = di
        + Sumc in ini tvalue(c, 0, inposc)
        - Sumc in outi tvalue(c, 0, outposc)
  2. Mi (Snap Messages): if node i is in mode RUNNING, it has not yet sent a snap message to any of its output channels and it has not yet received a snap message from any of its input channels:
    modei = RUNNING =>
        forall c in outi forall k (~C[k] instanceOf SnapMessage)
        forall c in ini forall k < inposc (~C[k] instanceOf SnapMessage)
    If the node is not in mode RUNNING any more, it has sent exactly one snap message to every of its output channels and it has received exactly one snap message in every input channel where the snapped flag is set:
    modei /= RUNNING =>
        forall c in outi exists ! snap (C[snap] instanceOf SnapMessage)
        forall c in ini forall h ((c = ini(h), snappedi[h]) =>
            exists ! snap < inposc (C[snap] instanceOf SnapMessage))
    If a node is not in mode RUNNING and c is an input or output channel of this node, we denote by snapc the unique position of the snap message in the trace of c.
  3. Si (Snapping): if node i is not in mode RUNNING any more, the snap value equals the deposit plus the trace value of all output channels from the position of their snap messages sent by the node minus the trace value of all input channels from the position of their snap messages received by the node (if such a snap message was received); missingSnaps denotes the number of outstanding snap messages:
    modei /= RUNNING =>
        snapValuei = depositi
            + Sumc in outi tvalue(c, snapc, outposc)
            - Sumc in ini, c = in_i(h), snapped_i[h] tvalue(c, snapc, inposc),
        missingSnaps = Sumh, ~snapped[h] 1
  4. Bi (Broadcasting): if node i is in one of the modes BROADCASTING or TERMINATED, then its totalValue equals the sum of all received snapValues and missingValues denotes the number of all not yet received snapValues:
    modei in {BROADCASTING, TERMINATED} =>
        forall j, done[j] modej in {BROADCASTING, TERMINATED},
        forall c in ini forall h (c = in(h) => snapped[h])
        totalValue = Sumj, done[j] snapValuei
        missingValues = Sumj, ~done[j] 1
  5. Ti (Terminated): if the node is in mode TERMINATED, no snap values are missing any more:
    modei = TERMINATED =>
        missingValuesi = 0.
Distributed Snapshots: Proof
 

Let I be the conjunction of all propositions above (for all i). Assuming that I is a program invariant, we can proof Theorem B.5 as follows (see also Figure B.5):

Proof of Correctness Theorem: When node i is in mode TERMINATED, we know by Ti that missingValuesi = 0. By Bi, this means that totalValuei = Sumj snapValuej, that every node j is in one of the modes BROADCASTING or TERMINATED, and that snapped[k] for every index k of an input channel. Together with Sj for every node j, we thus have

Sumj snapValuej = Sumj
    depositj
        + Sumc in outj tvalue(c, snapc, outposc)
        - Sumc in inj tvalue(c, snapc, inposc)
From Sj for every node j, we know for every channel c that 0 <= snapc < inposc <= outposc. Since every channel has exactly one sender and one receiver node, we then have
Sumj snapValuej
= Sumj depositj
    + Sumc tvalue(c, snapc, outposc)
    - Sumc tvalue(c, snapc, inposc)
= Sumj depositj + Sumc tvalue(c, inposc, outposc)
By Di, we know
Sumj depositj + Sumc tvalue(c, inposc, outposc) = Sumj dj
and, by Theorem B.5,
Sumj dj = valuenet
which completes the proof.
Maintainer: Wolfgang Schreiner
Last Modification: November 14, 1997

previous up next