Verificação prática de anomalias em programas de memória transaccional

Abstract

A Memória Transaccional (MT) é uma nova abordagem ao controlo de concorrência, baseada no conceito de transacção dos sistemas de gestão de base de dados. Ao contrário dos modelos baseados em locks, em MT podem existir diversos processos a aceder optimística e simultaneamente à mesma região crítica. Assim, uma transacção executa como se fosse única no sistema sendo que, no final, os resultados tornam-se permanentes ou são descartados (rolled-back) consoante a existência ou não de conflitos. Apesar de potenciar um melhor desempenho e utilidade, a MT é ainda uma tecnologia prematura, carecendo de ferramentas e trabalho que comprovem o seu potencial. A programação concorrente é difícil e propensa a erros. Muitos destes erros são decorrentes de anomalias relacionadas com o acesso concorrente a dados partilhados. Apesar de alguns autores defenderem que os programas em MT são menos propensos a erros, estes também podem exibir anomalias concorrentes, tais como high-level dataraces, i.e., delimitações incorrectas do escopo das transacções, ou stale-value errors, que correspondem a transposições erróneas de variáveis de um bloco atómico para outro. Programas com este tipo de anomalias podem exibir comportamentos imprevisíveis ou erróneos, não cumprindo os objectivos para os quais foram concebidos. Este trabalho visa o desenvolvimento de algoritmos, baseados em análise estática, para a detecção de anomalias de programas escritos no paradigma transaccional. Estes algoritmos estão consolidados numa infraestrutura —MoTH — que agrega um conjunto de plugins que detectam anomalias específicas de programas Java ByteCode. Com este trabalho pretendemos provar que a utilização de análise estática na detecção de high-level dataraces e de stale-value errors é uma solução viável que permite obter resultados com um nível de precisão razoável.