Dissertação

{en_GB=Resource-Centered Concurrency Control - Mechanization of a Type Safety proof} {} EVALUATED

{pt=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., en=Concurrency control aims at coordinating access to resources that are shared by concurrent computations, ensuring that they are accessed atomically in order to prevent data races. Resource-Centered Concurrency Control proposes that the atomicity nature of resources, i.e, whether they must be accessed atomically, is automatically inferred and enforced from annotations that the programmer introduces by associating the "atomic" keyword to the type of program resources. The mechanism involves several stages, including inference (if possible) of the unspecified atomicity natures of types in the program, generation of code that resolves overloading from different method calls, and enforcement of atomic accesses to atomic resources. In this Thesis we present a machine checked proof of type safety (type preservation and progress) for a formalization of the RC3 type system over the OOlong language. The formalization and proofs have been implemented using the Coq proof assistant, as a modification of the corresponding ones for OOlong. While the formalization of the complete mechanism is still underway, this work provides rigorous assurance about the correctness of the initial and central type system, over which the remaining stages are based.}
{pt=Controlo de concurrência, RC3, Type Safety, Coq, OOlong, Atomicidade., en=Concurrency Control, RC3, Type Safety, Coq, OOlong, Atomic.}

Junho 18, 2019, 14:30

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