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.
