A Methodology for Opacity verification for Transactional Memory algorithms using Graph Transformation System - Cardoso, Diogo J.; Foss, Luciana; Du Bois, Andre R. (Anais do Workshop-Escola de Informática Teórica (WEIT), 2021)
Com a constante pesquisa e desenvolvimento de sistemas de Memória Transacional (TM), vários algoritmos têm sido propostos, e sua corretude é sempre um aspecto importante a se levar em consideração. Ao analisar algoritmos de TM, um dos critérios de corretude mais comumente usados é opacidade, que infere que execuções só observam estados consistentes da memória compartilhada. Este artigo propõe uma definição formal para demonstrar que um determinado algoritmo TM só gera histórias opacas usando um Sistema de Transformação de Grafos. Uma metodologia é introduzida para traduzir um algoritmo para regras de produção que manipulam o estado de um grafo. A abordagem proposta demonstrou a capacidade de lidar com algumas das complexidades de algoritmos TM e um caso de estudo mostra o funcionamento da prova de opacidade do algoritmo em questão.