O Ponto-e-Vírgula com Vazamento
Author
Venue
Anais da ACM sobre Linguagens de Programação 2021
Abstract
A lógica e a semântica dos programas contam uma história agradável sobre a composição sequencial: ao executar (S1; S2), executamos primeiro S1 e depois S2. Para melhorar o desempenho, no entanto, os processadores executam instruções fora de ordem, e os compiladores reordenam os programas de forma ainda mais drástica. Por padrão, os sistemas de thread único não conseguem observar essas reordenações; no entanto, os sistemas de múltiplos threads conseguem, tornando a história consideravelmente menos agradável. Uma tentativa formal de compreender a confusão resultante é conhecida como “modelo de memória relaxado”. Modelos anteriores ou não abordam a composição sequencial diretamente, ou restringem excessivamente processadores e compiladores, ou permitem comportamentos absurdos e irreais que são inobserváveis na prática. Para dar suporte à composição sequencial ao mesmo tempo em que visamos hardware moderno, enriquecemos a abordagem padrão baseada em eventos com pré-condições e famílias de transformadores de predicados. Ao calcular o significado de (S1;S2), o transformador de predicados aplicado à pré-condição de um evento e de S2 é escolhido com base no conjunto de eventos em S1 dos quais e depende. Aplicamos essa abordagem a dois modelos de memória existentes.
