A Graph Transformation System formalism for correctness of Transactional Memory algorithms

• Diogo Cardoso UFPel
• Luciana Foss UFPel
• Andre Du Bois UFPel

Resumo

With the constant research and development of Transactional Memory (TM) systems, various algorithms have been proposed, and their correctness is always an important aspect to take into account. When analyzing TM algorithms, one of the most commonly used correctness criterion is opacity, which infers that the algorithm only generates executions that observe consistent states of the shared memory. In this work we present a formal definition to demonstrate that a given TM algorithm only generates opaque histories using a Graph Transformation System (GTS). We achieve that by introducing a methodology of translating an algorithm into production rules that manipulate the state of a graph. With a set initial state of transactions, the result of this method consists of a state space that includes every possible order of execution of transactional operations that are automatically checked for opacity, therefore all possible histories the algorithm can generate are checked for the safety property. As a case study we demonstrate our approach using the algorithm CaPR+.