DisLog: A Separation Logic for Disentanglement

Explore a 17-minute conference talk from POPL 2024 introducing DisLog, a novel separation logic for verifying disentanglement in parallel programs. Delve into the first static approach for ensuring memory access patterns are disentangled, facilitating task-local reasoning and enabling high-performance parallel memory management. Discover how DisLog enriches concurrent separation logic with fork-join reasoning, and learn about DisLog+, a simplified version for programs that are disentangled by construction. Examine case studies, including parallel deduplication implementations, to see practical applications of these logics. Gain insights into the mechanization of results using the Coq proof assistant and Iris, and understand the implications for optimizing parallel program performance and correctness.

[POPL'24] DisLog: A Separation Logic for Disentanglement