Seminários de Pesquisa do PPGC – Prof. Rodrigo Geraldo Ribeiro

Resumo: Software Transactional Memory (STM) provides programmers with a simple high-level model of transactions that allows the writing of concurrent programs without worrying with locks, since all transaction concurrency management is done by the STM runtime. Such programming model grealy simplifies development of concurrent applications, but it has a cost: implementing an efficient and correct
STM algorithm is an art. Several criteria have been proposed to certify STM algorithms, some based on model checkers and proof assistants. In this work, we are interested in a more lightweight approach: specify STM algorithm as small-step operational semantics of a idealized language with STM support and check for safety properties using QuickCheck, a property-based testing library for Haskell.