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.
Controlo de concurrência, RC3, Type Safety, Coq, OOlong, Atomicidade.

Junho 18, 2019, 14:30

Documentos da dissertação ainda não disponíveis publicamente

Orientação

ORIENTADOR

Ana Gualdina Almeida Matos

Departamento de Engenharia Informática (DEI)

Professor Auxiliar

ORIENTADOR

Jan Gunnar Cederquist

Departamento de Engenharia Informática (DEI)

Professor Auxiliar