RSS Meetup

Automatic Detection and Resolution of Deadlocks in Go Programs

Sala 6.3.27, Ciências ULisboa

Por António Ravara (FCT/UNL).

The Go programming language is gaining momentum as a tool for developing concurrent software, privileging message-passing as the favoured abstraction for concurrency interaction. Message-passing is not immune to the usual concurrency errors: programs may deadlock since the language run-time offers only basic support for deadlock detection with no safety guarantees at compile-time (apart from the usual data type-safety). There is a need for more general deadlock resolution strategies in a Go message-passing setting that go beyond prevention and avoidance: existing solutions detect numerous deadlocks but limit their resolution to a small set of specific deadlock patterns. In this paper, we develop an algorithm that takes an abstraction of the communication behaviour of a Go program containing all the channel communication necessary for progress, detects possible deadlocks, and then suggests replacement code to the erroneous code snippet causing the deadlock. Building on previous work, we deal with real world situations that go beyond the state-of-the-art, offering solutions for deadlock detection and fixing that other approaches do not deal with.
(join work with Jorge Coelho, Adrian Francalanza and João Lourenço)

Bio: António Ravara is an Associate Professor at the Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon, Portugal (since October 2018). He has a PhD in Mathematics at IST, of the Technical University of Lisbon, Portugal (December 2000). MSc in Applied Mathematics at IST of the Technical University of Lisbon, Portugal (May 1996). BSc in Geographical Engineering at the Faculty of Sciences of the University of Lisbon, Portugal (September 1991).
His main research problem is how to ensure that inherently concurrent, highly distributed, software systems behave correctly. The focus is on the development of techniques, program constructions, and tools that help creating safe and well-behaved systems, provably providing correctness guarantees. The toolbox used includes static analysis of source code, capturing defects before deployment, with decidable, low complexity, property-driven, proof systems, using behavioural descriptions of programs.

17h00
LASIGE Computer Science and Engineering Research Centre
Logótipo do Verão na ULisboa, sobre um fundo amarelo

Uma oportunidade única de conheceres e experimentares o ritmo e o espírito da vida académica!

Título/data do evento, logótipos das entidades organizadoras e fotografia de Lisboa (Castelo de S. Jorge e respetiva colina)

Inscrição (taxa reduzida) até 20 de abril.

Título/data/local do evento, logótipos das entidades organizadoras e várias fotografias da orla costeira e de pessoas

Escola de verão com um programa muito diversificado, com especialistas em vários tópicos, que vão falar sobre formas de olhar para o nosso planeta de uma forma integrada, juntando conhecimentos de várias disciplinas.

Vem investigar connosco!

Logótipo do evento, sobre um fundo branco

Um evento de reunião da comunidade nacional nas diversas vertentes da informática, com a ambição de ser o fórum de eleição para a divulgação, discussão e reconhecimento de trabalhos científicos.

Páginas