Eine Programm-Logik für konkurrierende Objekte unter fairer Planung

Die bestehende Forschung zur Verifikation von konkurrierenden Objekten beschäftigt sich hauptsächlich nur mit Sicherheit, z. B. partielle Korrektheit oder Linearität. Obwohl es in letzter Zeit Arbeiten zur Verifikation der Lock-Freiheit von nicht-blockierenden Objekten gegeben hat, konzentrieren sich viel weniger Bemühungen auf Deadlock-Freiheit und Hunger-Freiheit, Fortschrittsmerkmale von blockierenden Objekten. Diese Eigenschaften sind schwieriger zu verifizieren als Lock-Freiheit, da sie den Fortschritt eines Threads vom Fortschritt eines anderen abhängen lassen, unter der Annahme fairer Planung. Wir schlagen LiLi vor, eine neue Rely-Guarantee-Style-Programmlogik zur Verifikation von Linearität und Fortschritt gemeinsam für konkurrierende Objekte unter fairer Planung. Die Rely-Guarantee-Style-Logik vereint thread-modulares Denken über sowohl Hunger-Freiheit als auch Deadlock-Freiheit in einem Rahmen. Sie etabliert auch eine fortschrittsbewusste Abstraktion für konkurrierende Objekte, die bei der Verifikation von Sicherheit und Lebendigkeit des Client-Codes angewendet werden kann. Wir haben die Logik erfolgreich angewendet, um die Hunger-Freiheit oder Deadlock-Freiheit repräsentativer Algorithmen wie Ticketlocks, Warteschlangenlocks, Lock-Coupling-Listen, optimistische Listen und latente Listen zu verifizieren.