De lekkende puntkomma
Author
Venue
Proceedings of the ACM on Programming Languages 2021
Abstract
Programmalogica en semantiek vertellen een mooi verhaal over sequentiële compositie: bij het uitvoeren van (S1; S2) voeren we eerst S1 uit en daarna S2. Om de prestaties te verbeteren, voeren processors instructies echter in willekeurige volgorde uit, en compilers herschikken programma's nog ingrijpender. Door hun ontwerp kunnen single-threaded systemen deze herschikkingen niet waarnemen; multi-threaded systemen kunnen dat echter wel, wat het verhaal aanzienlijk minder aantrekkelijk maakt. Een formele poging om de resulterende chaos te begrijpen staat bekend als een 'relaxed memory model'. Eerdere modellen slagen er niet in om sequentiële compositie direct aan te pakken, leggen processors en compilers te veel beperkingen op, of staan onzinnig gedrag toe dat in de praktijk niet waarneembaar is. Om sequentiële compositie te ondersteunen en tegelijkertijd moderne hardware te ondersteunen, verrijken we de standaard event-based benadering met precondities en families van predikaattransformatoren. Bij het berekenen van de betekenis van (S1;S2) wordt de predikaattransformator die wordt toegepast op de voorwaarde van een gebeurtenis e uit S2 gekozen op basis van de verzameling gebeurtenissen in S1 waarvan e afhankelijk is. We passen deze benadering toe op twee bestaande geheugenmodellen.
