Andre Henriques
4d1ca919ef
All checks were successful
continuous-integration/drone/push Build is passing
2.0 KiB
2.0 KiB
style |
---|
img[alt~="center"] { display: block; margin: 0 auto; } h3 { font-size: 1.2em; position: fixed; top: 1em; left: 50%; transform: translateX(-50%); } h4 { text-align: center; font-size: 1.2em; text-align: center; } img[alt~="top-m"] { margin-top: 40px; } |
A Paxos Implementation
Andre Henriques, Seoeun Lee
Basis of the implentation
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"
Step 1 - "Requirements" non-trivial aspects
receive do
{:propose, inst, value, t, pid_to_inform} ->
...
broadcast({:other_propose, inst, value})
...
{:other_propose, inst, value} -> ...
end
Step 2 - "Prepare"
Step 2 - "Prepare" non-trivial aspects
receive do
{:nack, inst, ballot, new_ballot} ->
...
broadcast({:abort, inst, ballot})
...
{:abort, inst, ballot} -> ...
end
Step 3 - "Accept"
Step 3 - "Accept" non-trivial aspects
receive do
{:accepted, inst, ballot} ->
...
broadcast({:decide, inst, value})
...
{:decide, inst, value} -> ...
end
Step 4 - "Leader Crash"
Application
Atomas
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