Taming x86-TSO Persistency

on YouTube ↗26m

" summary

Proposes a new synchronous PTSO model that eagerly persists writes and proves it reaches the same non‑volatile states as the asynchronous POPL’20 model — a formal equivalent reachable states theorem. Introduces a simpler persistent sequentially consistent model (store buffers removed), gives a DRF theorem that data‑race‑free programs enjoy SC persistency, supplies a conservative compilation scheme from PSC to PTSO, and provides declarative and finite‑state formulations used in the mechanical proofs.

AI-written summary · about

" chapters (15)

1. 0:00Intro
2. 0:30Memory hierarchy
3. 3:00There is a gap
4. 4:32Programmers like to assume Sequential Programming Consistency
5. 5:48Research questions & answers
6. 7:11Persistent programming
7. 10:37PTSOSYN by example (2)
8. 12:42POPL'20 by example
9. 16:23Persistency with an illusion of SC instead of x86-TSO
10. 17:47Persistent SC
11. 18:05PTSOSYN to PSC, formally
12. 18:51New Data Races
13. 22:00Mapping PSC to PTSOSYN
14. 23:56More in the paper
15. 24:43Summary