The Future of Concurrency and Parallelism
summary
Panelists contrast concrete methods and hard surprises: mechanized proofs in Coq/Agda and concurrent separation logic are used to prove deadlock freedom and verify optimizations, while session types model protocol adherence and non‑interference for message‑passing systems; a production graph engine (Katana Graph) validates the move from dense to sparse/irregular data and shows real customers use it; remaining gaps include Byzantine adversaries breaking optimistic concurrency, cache effects like false sharing dropping performance by orders of magnitude, and the open challenge of predicting time and memory via learned models.
AI-written summary · about
chapters (11)
- 0:00Start
- 9:11Research Agenda
- 13:28Dense to Sparse
- 16:25Concurrent Separation Logic
- 18:26Concurrent Perspective on Smart Contracts
- 19:58What Are the Biggest Unsolved Problems in this Subject of Concurrency and Parallelism
- 32:28How To Teach Concrete Programming
- 39:08What's the State of Verification in Sequential Programs
- 54:54What Limits the Performance of Most Programs
- 56:25Data Movement
- 59:12Closing Remarks
related talks
59m“Is Parallel Programming still hard? PART 1 of 2”
01h 16mConcurrency Approaches: Past, Present, and Future
39mConcurrent Languages are Functional
01h 01mRoundtable: Concurrency
44mConcurrent Affairs: Procedural Programming Unlocked
54mReasoning about Progress of Concurrent Objects
24mA Concurrent Program Logic with a Future and History
36mHow Do People Handle Concurrency?