Il punto e virgola mancante
Author
Venue
Atti dell'ACM sui linguaggi di programmazione 2021
Abstract
La logica e la semantica dei programmi raccontano una storia piacevole sulla composizione sequenziale: quando si esegue (S1; S2), si esegue prima S1 e poi S2. Per migliorare le prestazioni, tuttavia, i processori eseguono le istruzioni in ordine casuale e i compilatori riordinano i programmi in modo ancora più drastico. Per come sono progettati, i sistemi a thread singolo non possono osservare questi riordini; tuttavia, i sistemi a thread multipli possono farlo, rendendo la storia notevolmente meno piacevole. Un tentativo formale di comprendere la confusione che ne deriva è noto come "modello di memoria rilassato". I modelli precedenti non riescono ad affrontare direttamente la composizione sequenziale, oppure limitano eccessivamente i processori e i compilatori, oppure consentono comportamenti assurdi e irreali che sono inosservabili nella pratica. Per supportare la composizione sequenziale puntando all'hardware moderno, arricchiamo l'approccio standard basato sugli eventi con precondizioni e famiglie di trasformatori di predicati. Nel calcolare il significato di (S1;S2), il trasformatore di predicati applicato alla precondizione di un evento e proveniente da S2 viene scelto in base all'insieme di eventi in S1 da cui e dipende. Applichiamo questo approccio a due modelli di memoria esistenti.
