Multi-Round Heterogeneous Paxos

[isheff]

Extend Heterogeneous Paxos from making a single decision to making multiple decisions, necessary to decide on successive blocks. In its simplest form, this can just run the single-decision mode over and over, but we might want to think about what, if anything, we want to keep from previous rounds. TCP channels seem like a good thing to re-use, for example.

Prerequisites

• Add comments to HPaxos TLA Spec #34
• Heterogeneous Paxos Stateright Prototype  #45

Sub-Tasks

• Choose a proposer strategy: how do we choose who proposes, and what time-outs do we use?
• English Spec
• Formal Spec
• Prototype