As propriedades de "liveness" (como o encerramento) até dos programas simultâneos mais simples que usam memória compartilhada sob consistência sequencial tipicamente exigem algumas premissas de "fairness" quanto ao agendador. Sob modelos de memória fraca, as noções usuais de "thread fairness" são insuficientes e é necessária uma propriedade adicional de "fairness", memory fairness. Neste projeto, propomos definições de "memory fairness" nos ambientes de modelos operacionais e declarativos de memória, tais como SC, x86-TSO, RA e StrongCOH, e investigamos o seu uso na verificação de modelos e do encerramento de programas simultâneos com sincronização de baixo nível.

• Repositório de projetos