6.852: Distributed Algorithms Fall, 2009Today’s planWell, that was the plan for next time, but:Last timeAtomic sequencesCanonical atomic object automatonCanonical atomic object automatonAtomic objects vs. shared variablesCan use Trans to justify:Snapshot Atomic ObjectsSnapshot Atomic ObjectsVariable type for snapshot objectsImplementing snapshot atomic objectsIdea 1Idea 2 (Clever)In more detail:CorrectnessSerialization points for snapsCorrectness of serialization pointsComplexityAlgorithm using bounded variablesRead/Write Atomic ObjectsRead/write atomic objectsVitanyi-Awerbuch algorithmVitanyi-Awerbuch algorithmCorrectnessA useful lemmaProof of lemmaUsing lemma to show atomicity for [Vitanyi, Awerbuch] algorithmCondition 2Condition 2Condition 3ComplexityMore on read/write atomic objectsBloom algorithmBloom algorithmCorrectnessUnbounded-tag algorithmWhy the nondeterministic choice?Proof for integer algorithmE.g., Condition 2Proof of Condition 2, cont’dWhere are we?Simulation relation from BB to IBR is a simulation relationFirst key factSecond key factNow where are we?Next time…6.852: Distributed AlgorithmsFall, 2009Class 18Today’s plan• Atomic objects:– Atomic snapshots of shared memory: Snapshot atomic objects.– Read/write atomic objects• Reading: Sections 13.3-13.4• Next: – Wait-free synchronization.– Reading: • [Herlihy, Wait-free synchronization]• [Attiya, Welch, Chapter 15]Well, that was the plan for next time, but:• We have an amended plan: Move classes 21 and 22 before 19 and 20.• So really, next time:– Shared-memory multiprocessor computation– Techniques for implementing concurrent objects:− Coarse-grained mutual exclusion− Locking techniques− Lock-free algorithmsz Reading:− [Herlihy, Shavit] Chapter 9Last time• Defined Atomic Objects.z Atomic object of a given type is similar to an ordinary shared variable of that type, but it allows concurrent accesses by different processes. z Still looks “as if” operations occur one at a time, sequentially, in some order consistent with order of invocations and responses.z Correctness conditions:z Well-formedness, atomicity.z Fault-tolerance conditions:z Wait-free terminationz f-failure terminationAtomicObjectinvresprespinvrespinvAtomic sequences• Suppose β is any well-formed sequence of invocations and responses. Then β is atomicprovided that one can – Insert serialization points for all complete operations.– Select a subset Φ of incomplete operations.– For each operation in Φ, insert a serialization point somewhere after the invocation, and make up a response.In such a way that moving all matched invocations and their responses to the serialization points yields a trace of the variable type.AtomicObjectinvresprespinvrespinvCanonical atomic object automaton• Canonical object automaton keeps internal copy of the variable, plus delay buffers for invocations and responses.• 3 kinds of steps:– Invoke: Invocation arrives, gets put into in-buffer.– Perform: Invoked operation gets performed on the internal copy of the variable, response gets put into resp-buffer.– Respond: Response returned to user.• Perform step corresponds to serialization point.Canonical atomic object automaton• Equivalent to the original specification for a wait-free atomic object, in a precise sense.• Can be used to prove correctness of algorithms that implement atomic objects, e.g., using simulation relations.• Theorem 1: Every fair trace of the canonical automaton (with well-formed U) satisfies the properties that define a wait-free atomic object.• Theorem 2: Every trace allowed by a wait-free atomic object (with well-formed U) is a fair trace of the canonical automaton.Atomic objects vs. shared variables• Can substitute atomic objects for shared variables in a shared-memory system, and the resulting system “behaves the same”.• Theorem: For any execution α of Trans ×U, there is an execution α′ of A × U (the original shared-memory system) such that:– α | U = α′ | U (looks the same to the users), and–stopIevents occur for the same i in α and α′(same processes fail).p1p2pnx1x2A• Needs a technical assumption.• Construction also preserves liveness:– α fair implies α′ fair.– Provided that the atomic objects don’t introduce new blocking.• E.g., wait-free.• E.g., at most f failures for A and each atomic object guarantees f-failure termination.Can use Trans to justify:• Implementing fault-tolerant atomic objects using other fault-tolerant atomic objects.• Building shared-memory systems, including shared-memory implementations of fault-tolerant atomic objects, hierarchically.P1P2PnP1xP2xPnxP1xP2xPnxSnapshot Atomic ObjectsSnapshot Atomic Objects• Most common shared-memory model:– Single-writer multi-reader read/write shared variables,– Each process writes to one variable, others read it.• Limitation: Process can read only one variable at a time. • Atomic snapshot object adds capability for one process to read everyone’s variables in one step.p1p2pnx1x2AU1U2Unxn• We will:– Define atomic snapshot objects.– Show that they do not add any power: they can be implemented using only simple read/write shared variables, with wait-free termination!Variable type for snapshot objects• Assume a lower-level value domain W (for the individual processes to write), with initial value w0.• Value domain for the snapshot object: Vectors v of fixed length m, with values in W.• Initial value: (w0, w0, w0, …,w0).• Invocations and responses:– update(i,w):• Writes value w into component i.• Reponds “ack”.– snap:• Responds with the entire vector.• External interface: m “update ports”, p “snapshot ports”.• Each update port i is for updates of vector component i, update(i,w)i.updateportssnapshotports1m+1mm+p2m+2Implementing snapshot atomic objects•Goal:Implement an atomic snapshot object using a shared-memory system, one process per port, with only single-writer multi-reader shared variables.• Unbounded-variable algorithm [Afek, Attiya, Dolev, Gafni,…]• Also a bounded-variable version.• Shared variables:– For each update port i, shared variable x(i),written by update process i, read by everyone. – Each x(i) holds:•val, an element of W.• tag, a natural number.• Some other stuff, we’ll see shortly.• Processes use these separate read/write variables to implement a single snapshot atomic