The PAXOS Theorem
--- ----- -------

Theorem: If d is the proposal of the first committing
         instance in a PAXOS execution, then d must be
	 the proposal of every later proposing instance.

Corollary: If d is the proposal of the first committing
           instance of a PAXOS execution, then d must be
	   the proposal of any instance that sends final
	   (F) messages.


Definitions:

PAXOS execution
    The sequence of events as described in the problem.

Proposing Event
    An event is proposing for an instance if it includes
    the sending of proposal (P) messages by the instance
    master.  The decision proposed is the d value in the
    proposal (P) messages of this event.

Instance Proposing / Proposal of Instance
    An instance proposes only during a proposing event
    for the instance.  The decision proposed in this
    event is the proposal of the instance.

Committing Event
    An event is committing for an instance if the event
    includes the reception of the m-1'st proposal (P)
    message of the instance that is not ignored.

Instance Committing
    An instance commits only during a committing event
    for the instance.


Proof of Theorem:

1. Consider the messages a process sends or receives and
   does not ignore.  Then the order of the process's
   sending or receiving events for these messages is
   compatible with the order of the instances of these
   messages.

   In other words, after sending or receiving and not
   ignoring a message with instance i, a process CANNOT
   send or receive and not ignore a message with
   instance j < i.

2. If an acknowledgment (A) message includes the values
   (pd,pi), and pd is not X, then pd is the proposal of
   instance pi.

3. Given that a process sends or receives and does not
   ignore a proposal (P) message for instance i, the pi
   value for that process whenever it sends any message
   for an instance j > i is such that j >= pi >= i.

4. If instance i is committing, there are m processes
   which have the property that whenever they send any
   any message for an instance j > i, their pi value is
   such that j >= pi >= i.

5. An instance cannot propose until m-1 new instance (N)
   messages for the instance have been received and not
   ignored, and the m-1 acknowledgment (A) messages sent
   in response have also been received and not ignored.

6. The intersection of two sets S1 and S2 each contain-
   ing m processes is NOT empty.

7. If instance i is committing and instance j > i is
   proposing, at least one of the (pd,pi) pairs that
   instance j uses in step (9c) to choose a decision
   will have j > pi >= i.

8. If instance i is committing and instance j > i is
   proposing, and if all proposing instances k with
   j > k >= i have proposed the same decision as
   instance i, then instance j proposes the same deci-
   sion as instance i.

9. QED of theorem by induction on 8.


File:	   paxos_theorem.txt
Author:	   Bob Walton <walton@deas.harvard.edu>
Date:	   Thu Dec  4 04:29:33 EST 2008

The authors have placed this file in the public domain;
they make no warranty and accept no liability for this
file.

RCS Info (may not be true date or author):

    $Author: walton $
    $Date: 2008/12/04 09:41:31 $
    $RCSfile: paxos_theorem.txt,v $
    $Revision: 1.2 $