Programming multicores safely : handling barrier deadlocks

Tese de doutoramento, Informática (Ciências da Computação), Universidade de Lisboa, Faculdade de Ciências, 2015Nowadays, most produced computing devices include multicore processors. Applications that run on these devices only scale if they can compute in parallel. To this end, mainstream programming languages, like Java and C♯, adopted various parallel programming techniqffes. his thesis focffses on a parallel technique, called barrier, used for synchronisation. A barrier coordinates the execution order of parallel activities, by letting them wait for each other. Tasks using barriers are susceptible to the problem of deadlocks, where at least two activities are (indirectly) in a stalemate because of a conflicting ordering of some barriers. Deadlocks are a class of concurrency failures with a big impact in parallel programs. To help make parallel programming more productive, we propose two complementary techniques that handle deadlocks caused by barriers: a runtime verification tool, and a deadlock-free programming model. We present Armus, a runtime verification tool specialised in barrier deadlocks that is distributed, fault-tolerant, and verifies X10 and Java programs. Our technique verifies more barrier synchronisation patterns than existing state-of-the-art techniques. We improve deadlock verification based on graph analysis: our technique selects from two alternative graph representations of concurrency dependencies to hasten deadlock checking. Armus is evaluated with three benchmark suites in local and distributed scenarios. To handle barrier deadlocks at design time we propose a language called SBrenner that extends and formalises a programming model that originates from the Habanero-Java and the X10 languages. The outcome is a deadlock-free programming model that leverages pipeline parallelism. We present an operational semantics and a type system for SBrenner. Offr type system enjoys the properties of progress and subject reduction.Actualmente, a generalidade dos dispositivos de computação inclui um processador multicore. As aplicações que correm em processadores muIticore só aumentam o seu desempenho se computarem em paralelo, aproveitando assim o poder computacional dos núcleos disponíveis. Para este efeito, as linguagens de programação mais populares, tal como Java e C♯, adoptaram, nos últimos anos, várias técnicas de programação paralela. Esta tese lida com uma classe de falhas que origina da utilização de uma técnica de programação paralela, chamada barreira, cuja funcionalidade é a de sincronizar grupos de tarefas. Uma barreira coordena a ordem de execução de um grupo de tarefas, disponibilizando um ponto de execução em que as várias tarefas dum grupo podem esperar umas pelas outras. As tarefas que usam barreiras são vulneráveis ao problema de impasse, em que pelo menos duas tarefas estão (indirectamente) à espera uma da outra em barreiras diferentes sem que qualquer uma das tarefas possa avançar. Os impasses constituem uma classe de falhas, da área de concorrência, com grande impacto em programas paralelos. O nosso objectivo é aumentar a produtividade da programação paralela tratando do problema de impasses em barreiras. Nesta tese propomos duas técnicas complementares para lidar com o problema de impasses: uma ferramenta de verificação especializada em impasses sobre barreiras que é distribuída, tolerante a falhas e verifica aplicações X10 e Java; um modelo de programação isento de impasses