CS 294-8 Time, Clocks, and Snapshots in Distributed Systems http://www.cs.berkeley.edu/~yelick/294AgendaCommon Approach #1Happens Before RelationHappens Before ExampleCommon Approach #2State Machine ApproachComparison of ModelsCommon Notions of CorrectnessVariations on CorrectnessClosed World AssumptionClock ConditionMutual ExclusionClock SynchronizationClock Synchronization AlgorithmsSlide 16Stable PropertiesSafety and LivenessSnapshot AlgorithmSlide 20Related AlgorithmsBackup Example SlidesUsing State Machines to Model Parallel SystemsAtomicitySpecifications and ImplementationsCorrectness of Serial TypesLinearizabilitySome Queue HistoriesExecution Model DetailsHistoriesOrdering in HistoriesSlide 32Observations on LinearizabilityRelaxed Consistency ModelCorrectnessSafety and Liveness ExamplesProving Safety and LivenessMethods for Proving Correctness (Safety)Existence of Abstraction FunctionsExample 1: Locked QueueSimple Abstraction FunctionExample 2: Statistical DB TypeNeed for History VariablesExample 2: Queue ImplementationQueue Example NotesNeed for Prophecy VariablesAbstraction RelationKey idea in Queue ProofSlide 49Generalizing Linearizability to Relaxed ConsistencyCS294, Yelick Time, p1CS 294-8Time, Clocks, and Snapshots in Distributed Systemshttp://www.cs.berkeley.edu/~yelick/294CS294, Yelick Time, p2Agenda•Concurrency models–Partial orders, state machines,•Correctness conditions–Serializability, …–Safety and liveness•Clock synchronization•Bag of tricks for distributed alg’s–Timestamps, markers,CS294, Yelick Time, p3Common Approach #1•Reasoning about a concurrent system: partially order events in which you can observe the ordering–Messages, memory operations, events•Consider all possible topological sorts to serialize•Each of those serial “histories” must be “correct.”CS294, Yelick Time, p4Happens Before Relation•System is a set of processes•Each process is a sequence of events (a total ordering) on events•Happens before, denoted ->, is defined as the smallest relation s.t.:–1) if a and b are in the same process, and a is before b, then a -> b–2) If a is a message send and b is the matching receive, then a -> b–3) if a->b and b->c then a->c (transitive)CS294, Yelick Time, p5Happens Before Example•What if processes are multithreaded?•How to we determine the events?–Send message, receive message, what else?–What about read/write? Nonblocking opns?•Does this help if we’re trying to reason about a program or an algorithm?timeCS294, Yelick Time, p6Common Approach #2•Reasoning about a concurrent system: View the system as a state machine that produces serial executions:–Invocation/response events, send/receive message (with explicit model of network between)•Each of the global serial executions must be “correct.”CS294, Yelick Time, p7State Machine Approach•A distributed system is:–A finite set of processes–A finite set of channels (network links)•A channel is–Reliable, order-preserving, and with infinite buffer space•A process is: –A set of states, with one initial state–A set of events•Models differ on specific detailsCS294, Yelick Time, p8Comparison of Models•Which approach (partial orders vs. state machines) is better?•Is one lower level than the other?•Is one for shared memory and the other for message?CS294, Yelick Time, p9Common Notions of Correctness•Serializability, strong serializability•Sequential consistency, total store ordering, weak ordering, …•Linearizability (used in wait-free)•All of these are based on the idea that operations (transactions) must appear to happen in some serial order•Which of these (or others) are useful?CS294, Yelick Time, p10Variations on Correctness•Why are there so many notions?–Do all processes observe the same “serial” order, or can some see different views?–Are the specifications of each operation deterministic? Can processes see different “correct” behaviors?–Are all operations executed by a process ordered? E.g., read x -> read y doesn’t matter.–Is the observed order consistent with real time?CS294, Yelick Time, p11Closed World Assumption•Most of these correctness ideas assume that all communication is part of the system. •Anomalies come from:–Phone calls between users–A second “external” network•How does one prevent these anomalies?CS294, Yelick Time, p12Clock Condition•A logical clock assigns a timestamp C<a> to each event a.•Clock Condition: For any events a, b:–If a->b then C<a> < C<b>•To implement a clock–Increment clock between each pair of events within a process–When you send a message, append current time–When you receive a message, update own clock with max(timestamp, my-current-time) +1CS294, Yelick Time, p13Mutual Exclusion•Lamport defines a total order => as the clock ordering with ties broken by PID•“Clocks” are not synchronized a priori–Loosely synchronized within algorithm•Uses for mutual exclusion algorithm–How useful is this algorithm?–Is the specification useful?CS294, Yelick Time, p14Clock Synchronization•Two notions of synchronization:–External: Within some bound of UTC (Universal Coordinated Time)–Internal: Within some bound of other clocks in the system•Huge literature on clock synch. under various models (e.g., PODC).–Impossible in general due to message delays –Many algorithms synchronize clocks with high probability (within some bound)•Are synchronized clocks useful? For fault tolerance or in general?CS294, Yelick Time, p15Clock Synchronization Algorithms•Christian [89] describes a centralized time server approach–Set time = t_server + t_round_trip/2–No fault tolerance to server failure•Berkeley Algorithm [89]: –Master polls slaves and records round_trip time to estimate local times –Averages “non faulty” clocks–Send delta (not new time) to slaves–Master can be re-electedCS294, Yelick Time, p16Clock Synchronization Algorithms•Network Time Protocol (NTP) [Mills 95] meant for wide area:–Uses statistical techniques to filter clock data–Servers can reconfigure after faults–Protected (authentication used)•Design:–Primary servers connected to radio clock–Secondary servers synchronize with primaries, with distance from primary defining stata–Modes: Multicast, Procedure call, Symmetric–1-10s of milliseconds accuracy reportedCS294, Yelick Time, p17Stable Properties•Termination detection,
View Full Document
Unlocking...