Invited Talk: Bridging Safety and Performance
summary
Claims that safe, declarative parallel programs match optimized imperative code by combining a proof-backed memory model and automatic runtime management. A disentanglement theorem (2020) motivates a tree-of-heaps memory layout and lock-free local garbage collection with an efficiency proof (2021). A single-par primitive added to Standard ML yields the Maple system; on 72 cores it achieves ~30x speedup vs C/C++ sequential, uses ~20% less memory than C, is within ~2x of hand-tuned C/C++, and automatic heartbeat scheduling gets within ~25% of manual tuning and even beats OpenMP by ~50%.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 3:59Imperative versus declarative
- 10:26Memory bottlenecks
- 13:19Disentanglement for safe parallelism
- 18:39Heap hierarchy and garbage collection
- 23:14Maple compiler design
- 26:01Performance results
- 36:15Automatic granularity control
- 43:26Automatic vs manual optimizations
- 45:55Church and Turing theories
- 47:01Q&A
related talks
01h 04mWe Live in Interesting Times
42mAdventures in Efficiency and Performance
25mResponsive Parallelism with Synchronization
19mPete's Footprints
56m“High Performance Code 201: Hybrid Data Structures"
51mDesigning for Performance
01h 03mPrinciples of Persistent Programming
01h 15mFunctional Mechanical Sympathy