Das undichte Semikolon
Author
Venue
Tagungsband der ACM zu Programmiersprachen 2021
Abstract
Programmlogik und Semantik erzählen eine schöne Geschichte über sequenzielle Komposition: Bei der Ausführung von (S1; S2) führen wir zuerst S1 und dann S2 aus. Um die Leistung zu verbessern, führen Prozessoren Befehle jedoch in ungeordneter Reihenfolge aus, und Compiler ordnen Programme noch drastischer neu. Single-Thread-Systeme können diese Umordnungen aufgrund ihrer Konstruktion nicht beobachten; Multi-Thread-Systeme hingegen schon, was die Geschichte deutlich weniger schön macht. Ein formaler Versuch, das daraus resultierende Durcheinander zu verstehen, ist als „relaxed memory model“ bekannt. Frühere Modelle versäumen es entweder, die sequenzielle Komposition direkt zu behandeln, schränken Prozessoren und Compiler übermäßig ein oder lassen unsinnige, aus der Luft gegriffene Verhaltensweisen zu, die in der Praxis nicht beobachtbar sind. Um die sequenzielle Komposition zu unterstützen und gleichzeitig moderne Hardware anzusprechen, erweitern wir den standardmäßigen ereignisbasierten Ansatz um Vorbedingungen und Familien von Prädikatstransformatoren. Bei der Berechnung der Bedeutung von (S1;S2) wird der auf die Vorbedingung eines Ereignisses e aus S2 angewendete Prädikatstransformator auf der Grundlage der Menge der Ereignisse in S1 ausgewählt, von denen e abhängt. Wir wenden diesen Ansatz auf zwei bestehende Speichermodelle an.
