Computations: FAQ

Exactly what is the difference between an event and a step of a computation?

An event is a 4-tuple which specifies a state transition. The same event can occur multiple times in a computation. Each occurrence of the event is a separate step of the computation. The following example illustrates the difference between a step and an event.

Consider an agent that receives numbers on an input channel and sends squares of the numbers on an output channel. The agent may receive the message 3 and send the message 9 multiple times in a computation. The specification of an execution of a receive function which receives 3 and sends 9 is specified by an event -- a 4-tuple. Each execution in which the agent receives 3 and sends 9 is the execution of the same event. Each execution in which the agent receives 3 and sends 9 is a different step of the computation.

Don't computations have to start in an initial state of the system?

We define computations as a sequence of state transitions that can start in any state. When we prove properties of a system we prove properties of computations that start in the initial state of the system. Some papers on distributed systems restrict computations to start in an initial state of the system but we don't do so in this course.

What is a loop invariant?

Read See Effective Theories in Programming Practice by Jayadev Misra for many beautiful examples. See the Wikipedia page and links from the page to sources on the web for a definition and many examples.

A loop invariant is a predicate (a boolean formula) that holds at the beginning and end of each step of a computation. The following example illustrates the concept.

The algorithm computes the GCD (greatest common divisor) of positive integers X and Y.

x, y = X, Y
# gcd(x, y) = gcd(X, Y)

while x != y:
   # gcd(x, y) = gcd(X, Y)

   if x > y: x = x- y
   if y > x: y = y - x

    # gcd(x, y) = gcd(X, Y)

return x

The invariant is:

gcd(x, y) = gcd(X, Y)

It holds before each step.

If the algorithm terminates then we have

x == y

and so at termination:

gcd(x, y) = gcd(x, x) = x = gcd(X, Y)

How does the idea of loop invariant work for a distributed computation when we don't know which event will be executed at each step?

The loop invariant for a distributed computation has the form

set up initial state of the system
# loop invariant holds

while there exists an event that can be executed:
   # loop invariant holds
   execute any executable event
   # loop invariant holds

So, we have to prove that the invariant holds in all initial states, and if the invariant holds before any event that is executable then it continues to hold after the event is executed.

What is a loop variant?

As with loop invariants please read the link to Wikipedia and links in the Wikipedia page. See Effective Theories in Programming Practice by Jayadev Misra for many beautiful examples. A loop variant is used to prove that execution of a loop terminates. More generally, we use the idea of loop variants to prove that a computation eventually reaches a goal.

A loop variant is a function of the state (variables) of a program. The value of the function decreases at each iteration of a loop. The function is bounded below, and so the value of the function cannot decrease forever. Therefore the loop terminates.

Let's look at the example given earlier to compute gcd(X, Y).

A loop variant is x + y. Each iteration of the loop decreases x + y. It is bounded below by 2 -- the bound doesn't matter as long as there is a bound.

Because it is bounded below and cannot decrease forever the loop terminates.

Computations shows how a while loop of a sequential program can be used to analyze distributed algorithms.