A Paxos implementation

Andre Henriques

Basis of the implentation

Structure Steps

Steps

receive do
  {:leader_elector, proc} -> ...
  {:propose, inst, value, t, pid_to_inform} -> ...
  {:prepare, proc, inst, ballot} -> ...
  {:nack, inst, ballot} -> ...
  {:prepared, inst, ballot, accepted_ballot, accepted_value} -> ...
  {:accept, inst, ballot, value} -> ...
  {:accepted, inst, ballot} -> ...
  {:decide, inst, value} -> ...
end

Step 1 - "Requirements"

center

Step 2 - "Prepare"

center

Step 3 - "Accept"

center

Step 4 - "Leader Crash"

center

Application

Atomas

center top-m

Safety

  • If a game state exists, then it was created by a user
  • The game state can not divert.

Liveness

  • Eventually all users will have the same game state

Questions?