Apresentamos uma abordagem de verificação de modelo para modelos axiomatizados de consistência de memória escritos na linguagem CAT. Ela pode provar propriedades de modelos de memória únicos, como a monotonicidade das barreiras, e também comparar modelos como TSO e ARM. Para alcançar essa expressividade, nossa abordagem suporta o fragmento racional completo do CAT. Nós não apenas suportamos a operação de estrela de Kleene, composição e união para definir relações em um modelo de memória, mas também, pela primeira vez, interseção, inverso e a construção de relações a partir de conjuntos. Nossa abordagem de verificação de modelos para modelos de consistência de memória é lógica por natureza: formulamos o problema como satisfabilidade em uma teoria lógica de relações. Nossa contribuição técnica é, então, um novo solucionador de teoria que é sólido, completo e ótimo do ponto de vista da complexidade. No coração do nosso solucionador está um sistema de prova cíclico que pode detectar invariantes em tempo real. Isso nos permite terminar precocemente não apenas no caso de um modelo ter sido encontrado, mas também no caso de insatisfatibilidade. Nosso solucionador é fácil de implementar e fácil de combinar com heurísticas. Implementamos uma combinação com refinamento de abstração guiado por contraexemplo e exercitamos o protótipo em vários benchmarks - com resultados promissores.
Grünke et al. (Sex,) estudaram essa questão.