Flashix II: Incremental verification of non-local refinements
Final Report Abstract
Ausgangspunkt des Flashix-Gesamtprojekts war die zunehmende Verbreitung von Flash-Speichern, die sowohl in Consumer-Geräten (PCs, Tablets etc.) als auch in sicherheitskritischen, eingebetteten Systemen immer mehr eingesetzt werden. Im Rahmen von Flashix I wurde ein POSIX-konformes Dateisystem für Flash-Speicher entwickelt, das die spezielle Schreibcharakteristik von Flash-Speicher effizient ausnutzt. Es besteht aus 10 sequenziell programmierten Komponenten, die eine Verfeinerungshierarchie bilden. Es wurden Konzepte entwickelt, mit denen sich die Verifikation von funktionaler Korrektheit und Crash-Sicherheit (Stromausfälle führen zu einem konsistenten Dateisystem, mit klar definiertem Effekt) auf den Nachweis von Beweisverpflichtungen für einzelne Komponenten reduzieren ließ. Diese wurden mit dem interaktiven Theorembeweiser KIV generiert und interaktiv verifiziert. In Flashix II haben wir erfolgreich ein Konzept zur Modellierung und Verifikation entwickelt, das es ermöglicht, verschiedene neue effizienzkritische Aspekte inkrementell durch Modifikation der Verfeinerungshierarchie (horizontal) hinzuzufügen. Das Konzept der nicht-lokalen Verfeinerung ermöglicht es, sich bei der Verifikation auf die neuen Aspekte zu konzentrieren. Die Beweise für die alten Komponenten werden dabei nicht ungültig und können wiederverwendet werden. Die hinzugefügten Aspekte waren: 1) Nebenläufigkeit der Toplevel Dateisystem-Aufrufe. 2) Nebenläufige Hintergrundprozesse für Wear Leveling und Garbage Collection (erforderlich wegen der Charakteristik von Flash-Speicher) 3) Reihenfolgetreue Caches, die den Inhalt auf die Größe einer Seite (page) puffern, so dass kein unnötiger Speicherverschnitt entsteht. 4) Caches, die den Inhalt von Dateien puffern, so dass mehrfaches Schreiben einer Datei nur zu einer Modifikation des Flash-Speichers führt. Die nicht-lokale Verfeinerungstheorie für Nebenläufigkeit und Caching ist sehr generisch und kann auf beliebige Verfeinerungshierarchien angewandt werden. Für Nebenläufigkeit wurde Ownership verwendet, um Nebenläufigkeit an Schnittstellen so einzuschränken, dass Linearisierbarkeit gezeigt werden kann. Für Caches ergeben sich jeweils unterschiedliche Definitionen des Effekts von Crashes. Die Erweiterungen führen alle zu zusätzlichen Beweisverpflichtungen, für Nebenläufigkeit wurde eine Beweistechnik entwickelt, die Rely-Guarantee-Beweise mit Reduktion (nach Lipton) kombiniert. Alle Beweisverpflichtungen werden von KIV generiert, und konnten für die Fallstudie verifiziert werden. Insgesamt haben wir das erste voll verifizierte, realistische Dateisystem für Flash-Speicher bereitgestellt. Es umfasst 18k Zeilen verifizierten Codes, und entspricht dem aktuellen methodischen und technologischen Stand bei Flash-Dateisystemen. Es kann daher als Referenz für zukünftige Entwicklungen dienen.
Publications
- Inside a Verified Flash File System: Transactions & Garbage Collection. In Proc. of Verified Software: Theories, Tools, Experiments (VSTTE), volume 9593 of LNCS, pages 73–93. Springer, 2015
G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif
(See online at https://doi.org/10.1007/978-3-319-29613-5_5) - Verification of B+ Trees by Integration of Shape Analysis and Interactive Theorem Proving. Software & Systems Modeling, 14(1):27 – 44, 2015
G. Ernst, G. Schellhorn, and W. Reif
(See online at https://doi.org/10.1007/s10270-013-0320-1) - Modular, Crash-Safe Refinement for ASMs with Submachines. Science of Computer Programming, 131:3 – 21, 2016
G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif
(See online at https://doi.org/10.1016/j.scico.2016.04.009) - Modular Verification of Order-Preserving Write-Back Caches. In IFM: 13th International Conference, 2017, Proceedings, volume 10510 of LNCS, pages 375–390. Springer, 2017
J. Pfähler, G. Ernst, S. Bodenmüller, G. Schellhorn, and W. Reif
(See online at https://doi.org/10.1007/978-3-319-66845-1_25) - A Modular Verification Methodology for Caching and Lock-Based Concurrency in File Systems. Dissertation, Universität Augsburg, Fakultät für Informatik, 2018
Jörg Pfähler
- FastLane is Opaque – A Case Study in Mechanized Proofs of Opacity. In Proc. SEFM, volume 10886 of LNCS, pages 105–120. Springer, 2018
G. Schellhorn M. Wedel O. Travkin J. König H. Wehrheim
(See online at https://doi.org/10.1007/978-3-319-92970-5_7) - Verifying Correctness of Persistent Concurrent Data Structures. In FM, volume 11800 of LNCS, pages 179–195. Springer, 2019
J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim
(See online at https://doi.org/10.1007/978-3-030-30942-8_12) - Adding Concurrency to a Sequential Refinement Tower. In Rigorous State-Based Methods, volume 12071 of LNCS, pages 6–23. Springer, 2020
G. Schellhorn, S. Bodenmüller, J. Pfähler, and W. Reif.
(See online at https://doi.org/10.1007/978-3-030-48077-6_2) - Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. In FORTE, volume 12136 of LNCS, pages 39–58. Springer, 2020
E. Bila, S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim
(See online at https://doi.org/10.1007/978-3-030-50086-3_3) - Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch. In IFM: 16th International Conference, 2020, Proceedings. Springer, 2020
S. Bodenmüller, G. Schellhorn, and W. Reif
(See online at https://doi.org/10.1007/978-3-030-63461-2_12)
