A Legalidade de Computações sobre Memória Compartilhada

Neste trabalho, investigamos a consistência de computações sobre memória compartilhada do ponto de vista do conceito de legalidade. A modelagem formal de tais sistemas é fundamental para o correto entendimento das propriedades de cada modelo de consistência. Como uma primeira contribuição, propomos um novo modelo de dois níveis (eventos e operações) que não apresenta características indesejáveis como dependência de arquitetura, uso de referência global de tempo e uso de conjuntos totalmente ordenados de eventos ou operações. Em ambos os níveis, uma execução é vista como um conjunto parcialmente ordenado. Definida desta forma, uma execução pode ser representada por um grafo E-OU e propriedades relativas a condições de consistência podem ser derivadas das estruturas que surgem na representação gráfica. Em particular, a existência de b-knots e estruturas semelhantes está fortemente ligada à legalidade da execução a este grafo associada. Como uma segunda contribuição, definimos novas estruturas em grafos E-OU, c-subgrafos e k-componentes e estabelecemos as relações entre estas estruturas e outras já conhecidas (knots, b-knots e ciclos).  Utilizando os resultados obtidos pela teoria de grafos, apresentamos uma nova definição de legalidade que, em contraste com a definição original sobre uma seqüência de operações, é estabelecida sobre uma ordem parcial de operações. Utilizamos esta nova definição na apresentação formal de vários modelos de consistência. Concluímos que o novo modelo formal para computações sobre memória compartilhada e a teoria de legalidade aqui introduzidos podem ser utilizados para a análise formal de virtualmente todos os modelos de consistência, bem como para a proposição de novos modelos, podendo levar a implementações mais eficientes, uma vez que restrições de ordem entre operações não são impostas além daquelas realmente necessárias a cada modelo.