Nieszczelny średnik
Author
Venue
Materiały konferencyjne ACM dotyczące języków programowania 2021
Abstract
Logika i semantyka programów przedstawiają przyjemny obraz kompozycji sekwencyjnej: podczas wykonywania (S1; S2) najpierw wykonujemy S1, a następnie S2. Jednak w celu poprawy wydajności procesory wykonują instrukcje w nieuporządkowanej kolejności, a kompilatory zmieniają kolejność programów w jeszcze bardziej radykalny sposób. Z założenia systemy jednowątkowe nie są w stanie zaobserwować tych zmian kolejności; jednak systemy wielowątkowe są w stanie to zrobić, co sprawia, że obraz ten staje się znacznie mniej przyjemny. Formalną próbą zrozumienia wynikającego z tego chaosu jest tzw. „złagodzony model pamięci”. Wcześniejsze modele albo nie zajmowały się bezpośrednio kompozycją sekwencyjną, albo nadmiernie ograniczały procesory i kompilatory, albo pozwalały na bezsensowne zachowania „z powietrza”, których w praktyce nie da się zaobserwować. Aby wspierać kompozycję sekwencyjną przy jednoczesnym ukierunkowaniu na nowoczesny sprzęt, wzbogacamy standardowe podejście oparte na zdarzeniach o warunki wstępne i rodziny transformatorów predykatów. Podczas obliczania znaczenia (S1;S2) transformator predykatów zastosowany do warunku wstępnego zdarzenia e z S2 jest wybierany na podstawie zbioru zdarzeń w S1, od których zależy e. Stosujemy to podejście do dwóch istniejących modeli pamięci.
