Exploring Opacity Software Transactional Memory in Haskell through Graph Transformation

• Diogo J. Cardoso UFPel
• Luciana Foss UFPel
• Andre R. Du Bois UFPel

Resumo

Software Transactional Memory (STM) is considered an alternative abstraction for concurrent programming, it has shown to be more approachable when compared to it’s main counterpart, lock-based synchronization. Haskell included language support very early through the STM Haskell library, that allows concurrent lock-free programming using composable atomic actions that manipulate transactional variables. In this work, we explore the correctness criterion Opacity and CO-Opacity for the STM Haskell algorithm using a Graph Transformation System (GTS) approach. Even though Opacity can be demonstrated in Haskell using other STM algorithms, the original STM Haskell library does not satisfy it. Using a GTS to represent the execution of the original STM Haskell, we demonstrate it’s correctness, or lack thereof, using the graph characterization of the criterion. We also compare it to a GTS for the TL2 algorithm, to observe how the algorithms differ in decision making, and how it affects the correctness of the execution.

Palavras-chave: Concurrent Programming, Graph Grammar, Formal Semantics, Transactional Memory