DOC PREVIEW
Berkeley COMPSCI 294 - Lecture Notes

This preview shows page 1-2-3-4-5-6 out of 19 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

CS 294-8 Consensus http://www.cs.berkeley.edu/~yelick/294AgendaAdministriviaCourse OverviewSlide 5Highly Available ComputingReplicated State MachinesState Machine ApproachPropertiesSafety PropertiesLiveness PropertiesSafety and LivenessVisible BehaviorImplementsSlide 15Use of ConsensusPaxos AssumptionsSlide 18SummaryCS294, Yelick Consensus, p1CS 294-8Consensushttp://www.cs.berkeley.edu/~yelick/294CS294, Yelick Consensus, p2Agenda•Overview and Administrivia•Specifications and verification•Consensus•Practical Issues in Consensus•Note: due in part to unreliable network and lack of reliability in ppt, most slides are stolen from Lamport.CS294, Yelick Consensus, p3Administrivia•So far: readings in distributed and fault tolerant systems•Next: specifying and reasoning about these systems•Readings for next few weeks will be set by Thursday•For Thursday:–SmartBridge (for talk)–Frangiapani (for discussion)CS294, Yelick Consensus, p4Course Overview•So far: reading “systems” papers•Next few weeks: reading papers on algorithms and proofs•Why? –I know my algorithm works, but…–I found a missing case when I was implementing…–My advisor (or the PC) doesn’t believe me…CS294, Yelick Consensus, p5Agenda•Overview and Administrivia•Specifications and verification•Consensus•Practical Issues in ConsensusCS294, Yelick Consensus, p6Highly Available Computing•High availability means either perfection or redundancy.–The system can work even when some parts are broken.•The simplest redundancy is replication:–Several copies of each part.–Each non-faulty copy does the same thing.•Every computing system works as a state machine.•So a replicated state machine can do highly available computing.CS294, Yelick Consensus, p7Replicated State Machines•If a state machine is deterministic, then feeding two copies the same inputs will produce the same outputs and states.–We call each copy a process.–So all we need is to agree on the inputs. •Examples:–Replicated storage with Read(a) and Write(a, d) steps.–Airplane flight control system with ReadInstrument(i) and RaiseFlaps(d) steps.CS294, Yelick Consensus, p8State Machine Approach•A distributed system is:–A finite set of processes•A process is: –A set of states, with one initial state–A set of events or actions•An execution is a possibly infinite sequence of alternating states/actions s0 s1 s20 1 2CS294, Yelick Consensus, p9Properties•A stuttering transition has the form s s•A property is a set of executions closed under stuttering [Abadi, Lamport 1990]–The clock still ticks after a program temrinates–Stuttering is also a useful in mapping between levels of abstraction0CS294, Yelick Consensus, p10Safety Properties•Informally: A safety properties is one that says something bad doesn’t happen•Formally: A property P is a safety property iff:–If  is in P then any finite prefix of  is in P•Additionally, –If  is not in P then there is some finite prefix of  that is not in P •There is a point at which an illegal transition occurred–Safety properties can be finitely refuted.CS294, Yelick Consensus, p11Liveness Properties•Informally: A liveness property says something good eventually happens•Formally: A property P is a liveness property iff:–If every finite behavior is a prefix of some behavior in P •Additionally, –Can always “complete” a finite behavior into one that is in P–Safety properties cannot be finitely refuted.CS294, Yelick Consensus, p12Safety and Liveness•Every property (I.e., every set of behaviors) is the conjunction of:–A safety property and–A liveness property•Due to Alpern and Schneider, based on basic results from TopologyCS294, Yelick Consensus, p13Visible Behavior•A specification identifies a subset of its actions (or its state variables) as externally visible.•A state machine defines a set of allowable executions:–state: a set of values, usually divided into named variables.–actions: named changes in the state; internal and external.•They may be nondeterministic–In fact, Lampson encourages this in specs to allow flexibility in implementationsCS294, Yelick Consensus, p14Implements•Y implements X if –every external behavior of Y is an external behavior of X,•This expresses the idea that Y implements X if you can’t tell Y apart from X by looking only at the external actions •Examples: abstract data types, databases, distributed systems•Note: Lampson implicitly deals with finite behaviors, and therefore states the liveness property separately. (Doesn’t treat liveness in the proofs.)CS294, Yelick Consensus, p15Agenda•Overview and Administrivia•Specifications and verification•Consensus•Practical Issues in ConsensusCS294, Yelick Consensus, p16Use of Consensus•Agreeing on some value is called consensus.•A replicated state machine needs to agree on a sequence of values:–Input 1 Write(x, 3)–Input 2 Read(x)–. . .CS294, Yelick Consensus, p17Paxos Assumptions•Each legislator has –A ledger (stable storage)–An hourglasses for time•Communication–Point-to-point, fully connected network –Unreliable: loss and delay allowed•Failures–Legislators may come and go (processor failure)–They are honest – no byzantine failuresCS294, Yelick Consensus, p18Agenda•Overview and Administrivia•Specifications and verification•Consensus•Practical Issues in ConsensusCS294, Yelick Consensus, p19Summary•How to build a highly available system using consensus.–Run a replicated deterministic state machine, and get consensus on each input.–Use leases to replace most of the consensus steps with actions by one process.•The most fault-tolerant algorithm for consensus without real-time guarantees.–Lamport’s “Paxos” algorithm, based on •How to design and understand a concurrent, fault-tolerant system.–Write a simple spec as a state machine.–Define abstract function and show


View Full Document

Berkeley COMPSCI 294 - Lecture Notes

Documents in this Course
"Woo" MAC

"Woo" MAC

11 pages

Pangaea

Pangaea

14 pages

Load more
Download Lecture Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?