Author(s): Garcia, Tiago Soares Cogumbreiro
Date: 2009
Persistent ID: http://hdl.handle.net/10451/14039
Origin: Repositório da Universidade de Lisboa
Subject(s): compilação certificada; compilação conservadora de tipos; multithreading; compilação orientada a tipos; monitores; cálculo pi
Restrições físicas e eléctricas limitam o aumento da velocidade do relógio dos processadores, pelo que não se espera que o poder computacional por unidade de processamento aumente muito num futuro próximo. Em vez disso, os fabricantes estão a aumentar o número de unidades de processamento (\texto {cores}) por processador para continuarem a criar produtos com aumentos de performance. A indústria fez grandes investimentos em projectos como o RAMP e BEE2 que permitem a emulação de arquitecturas multi-core, mostrando interesse em suportar as fundações para a investigação de \ texto {software} que se destina a essas arquitecturas. Para tirar vantagem de arquitecturas multi-core, tem de se dominar tanto a programação concorrente como a paralela. Com a grande disponibilidade de sistemas paralelos que vai desde sistemas embebidos até a super computadores, acreditamos que os programadores têm de fazer uma mudança de paradigma passando da programação sequencial para a programação paralela e produzir \texto{software} adaptado, de raiz, a plataformas multi-core. O \texto{multithreading} é uma escolha bem conhecida e usada pela indústria para desenvolver sistemas explicitamente paralelos. Os \ texto {locks} são um mecanismo utilizado para sincronizar programas texto {multithreaded} de uma forma altamente eficiente. Porém, é comum surgirem problemas relacionados com concorrência como deter um \ texto {lock} tempo demais, não compreender quando se usam \t texto {locks} leitores/escritores ou escolher um mecanismo de sincronização desadequado. Estes problemas podem ser mitigados com recurso a abstracções de concorrência. Os tipos e as regras de tipos são formas simples e eficazes de garantir segurança. Os tipos não são só usados por sistemas de tipos para garantir que programas não têm erros de execução, mas servem também como especificações (verificáveis de uma forma automática). A informação dada pelos tipos é expressiva o suficiente para representar propriedades operacionais importantes, como segurança de memória. Os compiladores que \emph{preservam tipos} perduram a informação dada pelos tipos por todos os passos de compilação, permitindo uma compilação mais segura e que preserva a semântica (representada pelos tipos). Propomos um compilador que endereça os problemas que levantámos até agora: * uma linguagem fonte com abstracções para concorrência e para o paralelismo; * um compilador que se destine a uma arquitectura multi-core; * uma tradução que preserve a informação dada pelos tipos. Em relação à linguagem fonte, os cálculos de processos evidenciam-se como um bom modelo de programação para a computação concorrente. O cálculo pi, em particular, tem uma semântica bem compreendida, consiste num conjunto pequeno de operadores em que a comunicação é o passo fundamental de computação. Os cálculos de processos oferecem esquemas de compilação natural que expõe o paralelismo ao nível dos \ texto {threads}. Por estas razões, escolhemos o cálculo pi simplesmente tipificado como linguagem fonte. Vasconcelos e Martins propõem o MIL como uma linguagem\ texto {assembly} tipificada para arquitecturas\ texto {multithreaded}, um modelo que assenta numa máquina abstracta multi-core com memória principal partilhada. Esta linguagem fortemente tipificada oferece as seguintes propriedades de segurança: de memória, de controlo de fluxo e de liberdade de\ texto {race conditions}. O MIL contradiz a ideia que considera a associação entre a memória e\textit{locks} uma convenção, ao torná-la explícita na linguagem. O sistema de tipos faz cumprir uma política de utilização de\ texto {lock} que inclui: proibir apanhar um \ texto {lock} em posse (fechado), proibir libertar um \ texto {lock} que não está em posse e faz com que os \ texto {threads} não se esqueçam de libertar todos os \ texto {locks} no final da sua execução. Propomos uma tradução que preserva os tipos do cálculo pi para o MIL. O cálculo pi é uma álgebra de processos para descrever \emph{mobilidade}: uma rede de processos interligados computa comunicando ligações (ou referências a outros processos). No cálculo pi, a comunicação reconfigura dinamicamente a rede, fazendo com que os processos passem a estar visíveis a diferentes nós quando o sistema evolui. Ao traduzirmos o cálculo pi em MIL, partimos de uma linguagem onde os processos comunicam através de passagem de mensagens e chegamos a uma linguagem onde \ texto {threads} comunicam por memória partilhada. O processo de compilação não é directo nem trivial: certas abstracções, como canais, não têm uma representação complementar no MIL. Para ajudar a tradução, desenvolvemos, na linguagem de destino, uma biblioteca de tampões não limitados e polimórficos que são usados como canais. Estes tampões não limitados são monitores de Hoare, daí introduzirem uma forma de sincronização aos \ texto {threads} que estejam a aceder o tampão, e que encapsulam a manipulação directa de \ texto {locks}. A disciplina de \ texto {locks} do MIL permite representar explicitamente a noção da transferência ininterrupta da região crítica dos monitores---vai do \ texto {thread} que assinala a condição, e que termina, para o \ texto {thread} que está à espera nessa mesma condição, e que é activado. Os tampões não limitados são uma boa forma de representar canais, o que por sua vez simplifica a tradução, já que enviar uma mensagem corresponde a colocar um elemento no tampão, e que receber uma mensagem equivale a retirar um elemento do tampão. Impomos uma ordem FIFO no tampão, para assegurarmos que as mensagens enviadas têm a oportunidade de serem alguma vez recebidas. A função de tradução que definimos é uma especificação formal do compilador. A tradução do cálculo pi para MIL comporta a tradução de tipos, de valores e de processos. Os compiladores que preservam os tipos dão garantias em termos de segurança (os programas gerados não vão correr mal) e também em termos de correcção parcial (as propriedades semânticas dadas pelos tipos perduram no programa gerado). O nosso resultado principal é, portanto, uma tradução que preserva os tipos: o compilador gera programas MIL correctos ao nível dos tipos para processos pi fechados e bem tipificados. Outra preocupação da nossa função de tradução é que o programa gerado tente manter o nível de concorrência do programa fonte, o que inclui a criação dinâmica de \ texto {threads} e a sincronização entre \texto{threads}. As contribuições deste trabalho são: * Um algoritmo de compilação que preserva os tipos, mostrando a flexibilidade do MIL num ambiente tipificado e \ texto {race-free}. * Exemplos de programação e estruturas de dados feitos em MIL. Mostramos a im\-ple\-men\-ta\-ção de tampões polimórficos não limitados sob a forma de monitores, de variáveis de condição genéricas (primitivas dos monitores) e de filas polimórficas. Também descrevemos como codificar monitores na linguagem MIL. * Ferramentas. Criámos um protótipo para o compilador de $\pi$ para MIL, o que consiste em: o analisador sintáctico, o analisador semântico (estático) e o gerador de código. Refinámos o protótipo do MIL: adicionámos suporte para tipos universais e existenciais, \ texto {locks} de leitores/escritores, locks lineares e tuplos locais. Criámos uma \ texto {applet} Java que mostra de uma forma rápida e intuitiva o nosso trabalho sem ser necessário qualquer instalação (desde que o navegador \ texto {web} suporte \ texto {applets} de Java): podemos gerar código MIL a partir de código $\pi$, alterar o código MIL gerado e executá-lo. Os nossos protótipos estão disponíveis \ texto {on-line}, em http://gloss.di.fc.ul.pt/mil/: a \ texto {applet} Java, o código fonte e exemplos $\pi$ e MIL.
