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
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 $