Disputation: Daniel S. Fava

Doctoral candidate Daniel S. Fava at the Department of informatics, Faculty of Mathematics and Natural Sciences, is defending the thesis Relaxed Memory Models and Data-Race Detection tailored for Shared-Memory Message-Passing Systems for the degree of Philosophiae Doctor.

Picture of the candidate

Photo: Private

The University of Oslo is closed. The PhD defence and trial lecture will therefore be fully digital and streamed directly using Zoom. The host of the session will moderate the technicalities while the chair of the defence will moderate the disputation.

Ex auditorio questions: the chair of the defence will invite the audience to ask ex auditorio questions either written or oral. This can be requested by clicking 'Participants -> Raise hand'. 

Trial lecture

Title: "Reasoning about program correctness using program logics for concurrent software."

 

Main research findings

  • Go is an open-source programming language developed at Google that has become the underpinning of large amounts of virtual infrastructure, especially in the area of cloud computing. Inspired by Go, this thesis analyzes a programming environment where threads synchronize with each other via the exchange of messages over channels. Go specifies this interaction on a document called the memory model, written in English. We present a mathematical interpretation of the Go memory model document. Our mathematization brings benefits. For example, it allows us to more easily relate the language's design to the language's implementation. As evidence, we were able to find and fix a non-trivial bug in the Go data-race detector. Rooted in theory, our improvements to the Go data-race detector were incorporated into release 1.16 of the language. In this thesis, we share our experience applying formal methods to a large, real-world software project.

Adjudication committee:

 

  • Professor Tarmo Uustalu, Dept. of Computer Science, Reykjavik University, Iceland
  • Professor Marieke Huisman, University of Twente, The Netherlands
  • Researcher Silvia Lizeth Tapia Tarifa, Department of Informatics, University of Oslo, Norway

Supervisors

  • Professor Martin Steffen, Department of Informatics, University of Oslo  Norway
  • Professor Olaf Owe, Department of Informatics, University of Oslo  Norway

Chair of defence

  • Professor Ole Hanseth, Department of Informatics, UiO

Contact information to Department: Mozhdeh Sheibani Harat

Publisert 27. mai 2021 14:31 - Sist endret 8. nov. 2021 11:55