[pt] REVISITANDO MONITORES, NOVAMENTE

[en] REVISITING MONITORS, AGAIN

[pt] RENAN ALMEIDA DE MIRANDA SANTOS

[pt] MONITOR

[pt] PROVA FORMAL

[pt] SEMANTICA OPERACIONAL

[pt] CONDICAO DE CORRIDA

[en] MONITOR

[en] FORMAL PROOF

[en] OPERATIONAL SEMANTICS

[en] DATA RACING

[pt] Ao longo dos anos, muitas linguagens de programação foram propostas com o objetivo de prevenir condições de corrida para acessos à memória. O conceito de monitores, em particular, foi concebido justamente para evitar condições de corrida com acessos à memória. Nesta tese, nós descrevemos uma linguagem de programação inspirada por monitores e livre desse tipo de condição de corrida. Nossa linguagem possui threads, memória compartilhada com ponteiros, laços não limitados, e uma construção nova que emula as capacidades de monitores. Essa nova construção é interessante porque é mais simples e, ao mesmo tempo, mais flexível do que monitores. Nós prevenimos condições de corrida na linguagem por meio de um sistema de tipos que permite apenas o compartilhamento entre threads de dados imutáveis ou protegidos. Nós definimos a semântica operacional em passo pequeno da nossa linguagem por meio de três operações distintas e hierarquicamente organizadas: grosseiramente, a primeira camada representa núcleos individuais, a segunda camada gerencia a memória compartilhada e a terceira camada gerencia o conjunto de threads. Sobre essas relações, nós definimos uma relação de múltiplos passos que produz um traço da execução do programa. Nós usamos esse traço para provar a ausência de condições de corrida. Todos esses resultados foram formalmente definidos e provados em Coq.

[en] Over the years, many programming languages were proposed with the goal of being free from data races. The concept of monitors, in particular, was envisioned precisely to prevent data races. In this thesis, we describe a data-race-free programming language inspired by monitors. Our languages features threads, shared memory with referential semantics, unbounded loops, and a novel construct that emulates monitor capabilities. This new construct is interesting because it is simpler and at the same time more flexible than monitors. We prevent data races in the language by using a type system that allows only immutable or protected data to be shared among threads. We defined the small-step operational semantics of this language through three distinct and hierarchically layered single-step operations: roughly, the first layer represents individual cores, the second layer manages the shared memory, and the third layer manages the thread pool. Over these relations, we defined a multistep relation that produces a trace of program execution. We use this trace to prove the absence of data races. All these results were formally defined and proved in Coq.

ROBERTO IERUSALIMSCHY

ROBERTO IERUSALIMSCHY

NOEMI DE LA ROCQUE RODRIGUEZ

ANAMARIA MARTINS MOREIRA

FRANCISCO FIGUEIREDO GOYTACAZ SANT ANNA

HUGO MUSSO GUALANDI

2025-08-26

2025-04-25

[pt] TEXTO

application/pdf

INGLÊS

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=72693@1

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=72693@2

https://doi.org/10.17771/PUCRio.acad.72693