To ensure that all computers in a distributed system agree on a single input or value

It allows the system to operate normally even if some computers fail, by ensuring agreement on inputs

An algorithm where a leader proposes values, acceptors agree, and a majority is required for choosing a value

Choosing a new leader when the current one fails, which is as hard as the original consensus problem

No asynchronous algorithm can implement consensus if even a single process can fail by stopping

As an abstract program with a single variable "chosen" representing the set of chosen values

(chosen = {}) ∧ (∃ v ∈ Value : chosen' = {v})

A non-distributed multiprocess algorithm that is refined to create the Paxos algorithm

votes and maxBal

A function assigning to each acceptor a set of pairs <b,v> representing votes cast

A function assigning to each acceptor the highest ballot number in which it will participate

An attempt by a leader to get a particular value chosen

When a majority of acceptors have voted for it in a particular ballot

v) in the Voting algorithm?

For any vote cast, SafeAt(b,v) must be true for that ballot number and value

It doesn't explicitly model failures - a failed process simply stops taking actions

Increase its maxBal value, or vote for a value in a ballot

With a variable "msgs" containing the set of all sent messages

It abstracts away concepts like channels and message ordering, focusing only on message existence

It doesn't distinguish between lost messages and messages that are never received

It allowed focusing on the core consensus problem, revealing what leaders should do and what messages were needed

A way of implementing a higher-level program with a lower-level one, often involving both step and data refinement

It implements the "chosen" set using the votes cast by acceptors

It shows how the lower-level program implements the higher-level one

By maintaining the invariant that SafeAt(b,v) is true for any vote cast

It prevents acceptors from voting in old ballots that might contradict more recent decisions

By using ballot numbers and ensuring that older ballots cannot override newer ones

It ensures that any two majorities have at least one acceptor in common, preserving knowledge of chosen values

Paxos doesn't rely on a single fixed leader and can handle multiple concurrent leader attempts

Paxos prioritizes safety (never choosing conflicting values) over liveness (eventually choosing a value)

It assumes processes maintain state in stable storage, so a restart is equivalent to a pause

v) predicate in Paxos?

By maintaining the SafeAt(b,v) invariant for all votes

To prevent the acceptor from voting in outdated ballots

Other leaders can start new ballots, and the protocol ensures safety is maintained

It provides a total ordering of ballot attempts

It doesn't - ensuring progress (liveness) requires additional mechanisms beyond the basic safety properties

They propose values and coordinate the voting process among acceptors

It ensures that once a value is chosen, no conflicting value can be chosen in later ballots

To learn about any values that may have already been chosen or proposed in earlier ballots

v) condition is maintained when casting a vote?

It allowed focusing on the core consensus logic before dealing with distribution issues

It maintains safety regardless of network conditions - partitions only affect liveness

Paxos implements the Voting algorithm in a distributed setting using message passing

It prioritizes safety in its core protocol and relies on external mechanisms for ensuring progress

It allows for clearer, more abstract reasoning about core problems and their solutions

A safety property is a condition that must always be true throughout the execution of a program. It asserts that 'nothing bad ever happens'.

Mutual exclusion is a safety property: no two processes should be in their critical sections simultaneously.

A liveness property asserts that 'something good eventually happens'. It ensures that the program makes progress and doesn't get stuck.

Starvation freedom is a liveness property: every process that requests to enter its critical section will eventually be granted access.

Safety properties are typically expressed using the 'always' (□) operator in temporal logic. For example, □(not (crit1 and crit2)) expresses mutual exclusion.

Liveness properties often use the 'eventually' (◇) operator. For instance, ◇(requested → ◇granted) expresses that a request will eventually be granted.

Safety properties specify that bad things never happen, while liveness properties specify that good things eventually happen. Safety is about maintaining invariants, liveness is about making progress.

Yes, some properties can be expressed as both safety and liveness. For example, termination can be expressed as a safety property (the program is not in the running state) or a liveness property (the program eventually terminates).

Weak fairness (also called justice) states that if an action becomes continuously enabled, it will eventually be executed. It prevents infinite procrastination.

Strong fairness (also called compassion) states that if an action is infinitely often enabled, it will eventually be executed. It's a stronger condition than weak fairness.

In a system where a process can lose and regain the ability to make progress repeatedly, weak fairness might not ensure progress, but strong fairness would.

In TLA+, weak fairness for an action A is expressed as WF_v(A), where v is the tuple of variables that A may change.

In TLA+, strong fairness for an action A is expressed as SF_v(A), where v is the tuple of variables that A may change.

Fairness conditions are often used to ensure liveness properties. They guarantee that certain actions will eventually occur, which can lead to the 'good things' specified by liveness properties.

Weak fairness in mutual exclusion guarantees that if a process is continuously trying to enter its critical section, it will eventually succeed.

Refinement is the process of transforming a high-level, abstract specification of a program into a more concrete, implementable version while preserving its essential properties.

The two main types of refinement are data refinement and step refinement.

Data refinement involves changing the representation of data in a program. It replaces abstract data structures with more concrete ones that can be efficiently implemented.

Step refinement (also called action refinement) involves breaking down high-level atomic actions into sequences of more fine-grained steps.

Replacing a mathematical set in a high-level specification with a hash table or binary search tree in the implementation is an example of data refinement.

Breaking down an atomic 'send message' action in a high-level spec into 'prepare message', 'allocate buffer', 'copy to buffer', and 'transmit' steps is an example of step refinement.

A refinement mapping is a function that maps states of the concrete system to states of the abstract system, showing how the concrete system implements the abstract one.

Proving refinement ensures that properties proven for the abstract specification still hold for the concrete implementation, allowing for modular verification and stepwise development.

Refinement often involves proving that the concrete system maintains invariants that correspond to those of the abstract system, possibly expressed in terms of the concrete state.

Refinement should preserve both safety and liveness properties. The concrete system should not allow any behaviors that violate the safety properties of the abstract system, and it should ensure all the liveness properties are still satisfied.

A real-time program is one where correctness depends not only on logical results but also on the time at which those results are produced. It must respond to inputs within specified time constraints.

In hard real-time systems, missing a deadline is considered a system failure. In soft real-time systems, missing a deadline is undesirable but doesn't constitute a failure.

Time constraints are often represented using a global clock variable that increases monotonically, and by adding timing conditions to actions or state transitions.

A timed automaton is a finite state machine extended with clock variables. It can be used to model and verify real-time systems.

Safety properties for real-time systems often involve time bounds. For example: 'The system always responds within 5 milliseconds of receiving a request.'

A liveness property for a real-time system might be: 'Every request will eventually receive a response within 10 milliseconds.'

Verifying liveness properties for real-time systems often requires proving that certain actions occur within bounded time, which can be more complex than untimed liveness properties.

In real-time systems, fairness conditions often need to be strengthened with time bounds. For example, weak fairness might be replaced with a guarantee that an enabled action is taken within a specific time limit.

Paxos is a protocol for solving consensus in a network of unreliable processors. It allows a distributed system to agree on a single value even in the presence of failures.

The Paxos algorithm was invented by Leslie Lamport.

The main roles in Paxos are proposers (who propose values), acceptors (who vote on proposals), and learners (who learn the agreed-upon value).

A round in Paxos is a attempt to reach consensus, consisting of two phases: a prepare phase and an accept phase.

In the prepare phase, a proposer sends a prepare request with a round number to a majority of acceptors. Each acceptor promises not to accept proposals with lower round numbers and returns any previously accepted proposal.

In the accept phase, if the proposer received responses from a majority of acceptors, it sends an accept request to a majority of acceptors with the highest-numbered proposal it received, or its own value if it received none.

Paxos ensures safety by requiring a proposer to adopt the value of the highest-numbered proposal it sees in the prepare phase, ensuring that once a value is chosen, no conflicting value can be chosen in future rounds.

Paxos provides liveness by allowing new rounds to be started at any time. If a sufficient period of synchrony occurs (messages are delivered in a timely manner), consensus will be reached.

The FLP result states that no deterministic consensus algorithm can guarantee termination in an asynchronous system with even one faulty process. Paxos sidesteps this by providing probabilistic termination.

Paxos can tolerate failures of less than half of the acceptors. It can also handle message losses and delays, as well as proposer failures, as long as at least one proposer remains operational.

Multi-Paxos is an optimization of Paxos for reaching consensus on a sequence of values. It allows the prepare phase to be skipped in subsequent rounds if the proposer remains the same.

Raft is designed to be more understandable than Paxos, but both solve the consensus problem. Raft separates leader election and log replication, while these are more integrated in Paxos.

Paxos requires that certain operations (prepare and accept) must be completed by a majority (more than half) of the acceptors. This ensures that there's always an overlap between any two majorities.

Paxos handles concurrent proposals through its round numbering system. Higher-numbered rounds take precedence, and the protocol ensures that if a value is chosen in a lower-numbered round, it will be preserved in higher-numbered rounds.

Basic Paxos requires two round trips to reach consensus. Fast Paxos is an optimization that allows decisions to be reached in fewer message delays under favorable conditions, but may require more messages in some scenarios.