Estamos desenvolvendo um modelo intermediário de memória fraca (IMM), como uma maneira de modularizar provas de correção da compilação, desde linguagens de programação simultânea com semântica de consistência de memória fraca até arquiteturas multicore comuns, como Power e Arm. Usamos o IMM para provar a correção da compilação, desde vários novos modelos de memória de linguagens de programação (principalmente aqueles que têm o objetivo de corrigir o problema Out-of-Thin-Air) até modelos de memória em hardware, como Power, Armv7, Armv8, RISC-V e x86-TSO. Nossos resultados são mecanizados no Coq e, até onde sabemos, estes são os primeiros resultados de correção da compilação verificados por máquina para modelos mais fracos que o x86-TSO.

• Repositório de projetos