Dissertação
Resource-Centered Concurrency Control - Mechanization of a Type Safety proof EVALUATED
O controlo de concurrência tem como objectivo o acesso coordenado a recursos que são partilhados por computações concurrentes, garantindo que estes sejam acedidos atomicamente de forma a prevenir data races. O Controlo de Concurrência Centrado nos Recursos propõe que a natureza atómica dos recursos, ou seja, se eles devem ou não ser acedidos atomicamente, seja automaticamente inferida e garantida através das anotações que o programador introduz associando a palavra-chave "atomic" ao tipo dos recursos. O mecanismo envolve várias etapas, incluindo a inferência (se possível) das naturezas atómicas de tipos, que não estão especificadas no programa, criação de código que resolve a sobrecarga de diferentes chamadas de métodos, e a garantia de acessos atómicos a recursos atómicos. Nesta Tese apresentamos a mecanização da prova de type safety (preservação e progresso) para a formalização do sistema de tipos do RC3, que tem como base a linguagem OOolong. A formalização e as provas foram implementadas usando o assistente de provas Coq, modificando as já existentes para o OOlong. Apesar da formalização do mecanismo ainda não estar completa, este trabalho já garante um nível de certeza de que o sistema de tipos inicial e central, sobre o qual as outras fases são baseadas, está correcto.
junho 18, 2019, 14:30
Publicação
Obra sujeita a Direitos de Autor
Orientação
ORIENTADOR
Departamento de Engenharia Informática (DEI)
Professor Auxiliar
