Um Formalismo de Gramática de Grafos para Corretude de Memória Transacional de Software
Fecha
2023-04-06Metadatos
Mostrar el registro completo del ítemResumen
Com a crescente demanda de sistemas multi-core, programação concorrente tem visto um aumento em uso. Porém, desenvolver programas concorrentes que sejam corretos e eficientes é algo notoriamente desafiador. Um sistema de Memória Transacional de Software (MTS) provém uma interface de programação conveniente para o programador acessar a memória compartilhada sem se preocupar com problemas de concorrência. Um MTS permite desenvolver programas e raciocinar sobre sua corretude como se cada transação fosse executada atomicamente e sem intercalação. Para verificar a corretude de qualquer sistema MTS, uma descrição formal das garantias de implementação é necessária. Existem diversas condições de corretude para memória transacional, muitas delas envolvem a noção de história de operações sobre a memória compartilhada, além disso, algumas usam grafos como ferramentas para ajudar a formalizar o processo de correção. O uso de grafos no formalismo MTS geralmente envolve uma representação de dependências e relações entre transações e suas operações. Uma condição de corretude em particular, chamada Opacidade, usa um grafo para representar conflitos entre transações em uma história, e um método que extrapola se a execução da história é considerada correta ou não. Grafos e transformações de grafos desempenham um papel central na modelagem de sistemas de software. Esses modelos são especificados usando um formalismo que utiliza abstrações de alto nível independente da plataforma, de modo que o foco pode estar nos conceitos e não na implementação do sistema que está sendo forma lizado. Nas Gramáticas de Grafos (GGs), a modificação de grafos é especificada por meio de regras de transformação de grafos, que definem esquematicamente como um estado do sistema pode ser transformado em um novo estado. Ao formalizar sistemas complexos, os GGs podem levar em consideração orientação a objetos, concorrência,
mobilidade, distribuição etc. Esta tese apresenta uma metodologia para formalizar algoritmos de memória transacional utilizando gramática de grafos e demonstrar a corretude de suas execuções. O objetivo não é apenas descrever os procedimentos do algoritmo usando regras de produção, mas também incluir os passos necessários para aplicar a caracterização do grafo de certos critérios de corretude. A metodologia inclui três passos principais: uma tradução do algoritmo para uma gramática de grafo, o método para gerar histórias e o teste de corretude. Alguns estudos de caso são apresentados, como o algoritmo CaPR+, que trata de rollbacks parciais. Outro estudo de caso é o algoritmo STM Haskell, que é mais conhecido e é usado para comparar o comportamento entre diferentes aplicações de critérios de corretude. Por fim, uma alternativa à ferramenta GROOVE, utilizada para verificação de correção, é apresentada na forma de um modelo Event-B que inclui o mesmo formalismo gráfico do MTS, mas difere ao lidar com o espaço de estados e prova de corretude. Diferente de outros trabalhos que focam em formalização de algoritmos de MT, a metodologia proposta lida com grafos em todos os passos e não só durante o passao de verificação de corretude. Isso resulta em uma metodologia que pode tirar vantagem de ferramentas e características que focam em transformação de grafo e podem possivelmente fazer parte de um processo mais automatizado para para formalizações de MT futuras.