Static Analysis of Memory Models for SMT Encodings

on YouTube ↗18m

" summary

A static analysis computes per-execution upper and relativized lower bounds on memory-model relations (program order, coherence, read-from) and propagates them bidirectionally through CAT-style derived relations to eliminate impossible edges. The implementation in the datan bounded model checker simplifies SMT encodings (notably acyclicity checks), imports program-level constraints, and fixes many relation edges; evaluation on ARM, RISC-V and Linux-kernel code shows faster verification (up to 40% reduction in time) and enables checking safety, liveness, and data-race properties.

AI-written summary · about

" chapters (16)

1. 0:00Introduction
2. 0:23BMC verification approach
3. 1:06Concurrent semantics challenges
4. 2:12Execution graphs and memory models
5. 4:17Memory models and CAT language
6. 6:45Sequential consistency models
7. 7:27Static analysis of execution relations
8. 9:14Relation bounds with control flow
9. 10:17Abstract computation and propagation
10. 11:23Relation bounds in simple program
11. 13:11Single vs concurrent programs
12. 13:31Datan tool implementation
13. 14:14Evaluation on locks and Linux kernel
14. 15:17Summary
15. 15:39Q&A: What is verified
16. 16:41Q&A: Loops and recursion