Report

Reduction Theorems for Proving Serializability with Application to RCU-Based Synchronization Hagit Attiya Technion Work with Ramalingam and Rinetzky (POPL 2010) and work in progress with Maya Arbel Sequential Reductions Design and verify concurrent data structures E.g., linked list with hand-over-hand locking [Kedem & Sliberschatz ‘76] [Smadi ‘76] [Bayer & Scholnick ‘77] t1 t2 t1 t1 H Dagstuhl, Feberuary 2013 Sequential Reductions Design and verify concurrent data structures E.g., linked list with hand-over-hand locking [Kedem & Sliberschatz ‘76] [Smadi ‘76] [Bayer & Scholnick ‘77] t2 t2 t1 t1 H Consider only sequential executions, but conclude that properties hold in all executions Dagstuhl, Feberuary 2013 Serializability [Papadimitriou ‘79] interleaved execution operation ~~ ~~ ~~ Locally observed by threads complete non-interleaved execution Dagstuhl, Feberuary 2013 Serializability Yields Sequential Reduction Concurrent code M If M is serializable, then a local property φ holds in all executions of M iff φ holds in all complete non-interleaved executions Easily derived from [Papadimitriou ‘79] A small subset of all executions How to check M is serializable, w/o considering all executions? Dagstuhl, Feberuary 2013 Disciplined Programming with Locks Locking protocol ensures conflict serializability – two-phase locking (2PL), tree locking (TL), (dynamic) DAG locking Verify that M follows a local locking protocols – Depending only on thread’s local variables & global variables locked by it – Not a centralized concurrency control monitor! Local property of an execution holds in every execution indistinguishable from it Dagstuhl, Feberuary 2013 Reduction Theorem: Easy Step complete non-interleaved executions of M A local conflict serializable locking policy is respected in all executions iff it is respected in all non-interleaved executions A local property holds in all executions iff it holds in all non-interleaved executions Dagstuhl, Feberuary 2013 Reduction to non-interleaved executions: Proof idea σ is the shortest execution that does not follow LP σ’ follows LP, guarantees conflict-serializability (t,e) σ σ’ Dagstuhl, Feberuary 2013 Reduction to non-interleaved executions: Proof idea σ is the shortest execution that does not follow LP σ’ follows LP, guarantees conflict-serializability non-interleaved execution σ’ni “indistinguishable” from σ’ (t,e) σ σ’ σ’ni Dagstuhl, Feberuary 2013 Reduction to non-interleaved executions: Proof idea σ is the shortest execution that does not follow LP σ’ follows LP, guarantees conflict-serializability non-interleaved execution σ’ni “indistinguishable” from σ’ (t,e) σ σ’ σni (t,e) non-interleaved execution “indistinguishable” from σ’ where LP is violated Dagstuhl, Feberuary 2013 Further Reduction Almost-complete non-interleaved executions A local conflict serializable locking policy is respected in all executions iff it is respected in all almost-complete non-interleaved executions Need to argue about termination Dagstuhl, Feberuary 2013 Acni-reduction: Proof ideas Start from a ni-execution (use previous reduction) Create its equivalent completion, if possible Does not access variables accessed by later threads Not always possible, e.g., t1:lock(v), t1:lock(u), t2:lock(u) Dagstuhl, Feberuary 2013 v u Read-Copy-Update (RCU) Allows read-only operations (transactions) to read data, even when locked for updates Update operations (transactions) synchronize with each other using locks, and with read-only operations using synchronize_rcu RCU usage in the Linux kernel (from Paul McKenney) Dagstuhl, Feberuary 2013 RCU-Based Synchronization Not well-understood, especially when there are concurrent update operations RCU-based scan of a list concurrently with two updates yields an inconsistent view – Consistency of two reads contains on a sorted list has one critical read Dagstuhl, Feberuary 2013 Wait-Free “Contains” [Heller, Herlihy, Luchangco, Moir, Scherer, Shavit, OPODIS 2005] • Wait-free search operation reads the list unprotected (regardless of locks)… t1 t1 H • Lazy write operations start locking only after finding the relevant item Dagstuhl, Feberuary 2013 Principled RCU-Based Synchronization RCU-based linked list similar to pessimistic / optimistic / lazy list, which has been verified [Vafeiadis, Herlihy, Hoare, Shapiro, PPoPP 2006] But proof is not simple & what about other data structures, like search trees? Dagstuhl, Feberuary 2013 Our Approach • Apply sequential reduction to the sub-execution with only update operations – Read-only transactions do not modify the data – Pessimistic list follows dynamic tree locking • Prove structural properties / sortedness in almostcomplete non-interleaved executions (easy) Dagstuhl, Feberuary 2013 Our Approach • Then superimpose individual steps of the readonly operations onto the almost-complete noninterleaved executions • Complete the proof by focusing on the single critical read Dagstuhl, Feberuary 2013 What’s Now? Concurrent updates in search trees RCU-based balanced search trees, but they • Pessimistically disallow concurrent updates, using a big lock (Bonsai) [Clements, Kaashoek, Zeldovich, ASPLOS 2012] • Optimistically avoid concurrent updates, using TM (Red/black trees) [Howard, Walpole 2011?] Dagstuhl, Feberuary 2013 What’s Now? • Handle optimistic / lazy hand-over-hand locking, by extending the reduction to – Shared (read) locks – Initial failure and retry – Speculative “contains” beginning the update Dagstuhl, Feberuary 2013 Teaching Help… • Eran Yahav and I are planning a seminar on papers in the intersection of PL and DC • Please offer suggestions… • Don’t be shy about your own work. • You are also welcome to come and give a talk… Dagstuhl, Feberuary 2013