PerSeVerE: Persistency Semantics for Verification under Ext4

on YouTube ↗28m

" summary

Formal semantics for ext4 are derived from the kernel implementation and stress tests and integrated with C/C++ weak-memory models; a model-checker then explores persistency behaviors. The tool PerSeVerE framework model checks real programs and found bugs in emacs vim nano — notably a replace-by-truncate bug that corrupts files (demonstrated with a 128 MB experiment). A minimal fsync-after-write fix is verified and merged into nano, making it crash-safe on ext4.

AI-written summary · about

" chapters (11)

1. 0:00Start
2. 0:23Writing a Text Editor
3. 2:10What Doesman Say?
4. 5:50Desiderata
5. 7:09Contributions
6. 8:09Filesystem operations
7. 12:401/0 Stack
8. 14:53Persistency Semantics
9. 24:36Full model
10. 26:02Editor Bugs
11. 27:30Conclusions