Forschung
Programmiersprachen und Tools Lab
IMM: Compilation Correctness for Relaxed Memory Models
Das IMM-Framework vereinfacht den Nachweis der Korrektheit der Kompilierung von programmiersprachlichen Speichermodellen (wie Promising und Weakestmo) zu Hardware-Speichermodellen (x86, Power, Arm, RISC-V). Der Rahmen ist in Coq mechanisiert.
Wir entwickeln ein Zwischenmodell für schwachen Speicher, IMM, um die Korrektheitsnachweise für die Kompilierung von nebenläufigen Programmiersprachen mit schwacher Speicherkonsistenzsemantik für gängige Mehrkernarchitekturen wie POWER und ARM zu modularisieren. Wir verwenden das IMM, um die Korrektheit der Kompilierung von mehreren neuen Programmiersprachen-Speichermodellen (hauptsächlich diejenigen, die Probleme aus dem Nichts beheben sollen) zu Hardware-Speichermodellen wie POWER, ARMv7, ARMv8, RISC-V und x86-TSO zu beweisen. Unsere Ergebnisse werden in Coq mechanisiert, und unseres Wissens nach sind dies die ersten maschinenverifizierten Kompilierungskorrektheitsergebnisse für Modelle, die schwächer sind als x86-TSO.
