Programmiersprachen und Tools Lab

PwT: Compositional Semantics for Relaxed-Memory Concurrency

Pomsets with Preconditions, PwT, zielt darauf ab, ein denotationales Speichermodell für Programmiersprachen bereitzustellen, das Probleme aus dem Nichts ohne Leistungseinbußen auf modernen CPUs löst. Dies könnte als Ersatz für das C++-Speichermodell verwendet werden.

Die Programmlogik und -semantik erzählen eine nette Geschichte über die sequentielle Komposition: Bei der Ausführung von (𝑆1; 𝑆2) führen wir zuerst 𝑆1 und dann 𝑆2 aus. Um die Leistung zu verbessern, führen Prozessoren die Befehle jedoch in umgekehrter Reihenfolge aus, und Compiler ordnen die Programme sogar noch drastischer um. Single-Thread-Systeme können diese Umordnung nicht beobachten, Multiple-Thread-Systeme hingegen schon, was die Sache wesentlich unangenehmer macht. Ein formaler Versuch, das daraus resultierende Chaos zu verstehen, ist als "entspanntes Speichermodell" bekannt.

Frühere Modelle gehen nicht direkt auf die sequenzielle Komposition ein, schränken Prozessoren und Compiler zu sehr ein oder erlauben unsinniges Verhalten aus dem Nichts, das in der Praxis nicht beobachtbar ist. Um die sequenzielle Komposition zu unterstützen und gleichzeitig moderne Hardware zu nutzen, erweitern wir den standardmäßigen ereignisbasierten Ansatz um Vorbedingungen und Familien von Prädikatstransformatoren. Bei der Berechnung der Bedeutung von (𝑆1; 𝑆2) wird der Prädikatstransformator, der auf die Vorbedingung eines Ereignisses 𝑒 aus 𝑆2 angewendet wird, auf der Grundlage der Menge der Ereignisse in 𝑆1 ausgewählt, von denen 𝑒 abhängt.

Teilnehmende

Anton Podkopaev