Laboratório de Linguagens e Ferramentas de Programação

Projeto "Mechanization of Non-Interleaving Concurrency Models in the Coq Proof Assistant"

Uma teoria mecanizada de vários modelos não entrelaçados de computação concorrente no Coq Proof Assistant.

Uma possível abordagem objetiva do raciocínio a respeito de programas concorrentes é definir o comportamento destes como um conjunto de todos os possíveis entrelaçamentos das ações atômicas de threads individuais. Porém, raciocinar em termos de entrelaçamentos demonstra ser difícil demais, tanto para humanos quanto para computadores, porque o número de entrelaçamentos possíveis aumenta rapidamente.

Modelos não entrelaçados de concorrência, tais como linguagens pomset e estruturas de eventos, tentam atacar este problema propondo representações mais compactas do conjunto de comportamentos do programa. Nos últimos anos, tem havido um interesse renovado em modelos não entrelaçados de concorrência — por exemplo, no contexto de modelos relaxados de memória, verificação de modelos de programas concorrentes e testes de mutações baseadas em modelos.

O objetivo deste projeto é desenvolver uma teoria mecanizada de modelos não entrelaçados de concorrência no Coq Proof Assistant. Essa biblioteca deve ajudar os pesquisadores interessados a provarem formalmente as propriedades desses modelos e desenvolverem novas aplicações dessa teoria.

Participantes

Evgenii Moiseenko