ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Mon 16 Nov 2020 05:00 - 05:20 at SPLASH-I - S-6 Chair(s): Jeremy Gibbons, Olivier Flückiger
Sun 15 Nov 2020 17:00 - 17:20 at SPLASH-I - S-6 Chair(s): Shigeru Chiba, Tiark Rompf

Go is a popular concurrent programming language thanks to its ability to efficiently combine concurrency and systems programming. In Go programs, a number of concurrency bugs can be caused by a mixture of data races and communication problems. In this paper, we develop a theory based on behavioural types to statically detect data races and deadlocks in Go programs. We first specify lock safety/liveness and data race properties over a Go program model, using the happens-before relation defined in the Go memory model. We represent these properties of programs in a µ-calculus model of types, and validate them using type-level model-checking. We then extend the framework to account for Go’s channels, and implement a static verification tool which can detect concurrency errors. This is, to the best of our knowledge, the first static verification framework of this kind for the Go language, uniformly analysing concurrency errors caused by a mix of shared memory accesses and asynchronous message-passing communications.

Sun 15 Nov
Times are displayed in time zone: Central Time (US & Canada) change

17:00 - 18:20: S-6Research Papers at SPLASH-I +12h
Chair(s): Shigeru ChibaThe University of Tokyo, Tiark RompfPurdue University
17:00 - 17:20
Talk
Research Papers
Julia GabetImperial College London, Nobuko YoshidaImperial College London
Link to publication DOI Media Attached
17:20 - 17:40
Talk
Research Papers
Vlastimil DortCharles University, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Media Attached
17:40 - 18:00
Talk
Research Papers
Keigo ImaiGifu University, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London, Shoji YuenNagoya University
Link to publication DOI Media Attached
18:00 - 18:20
Talk
Research Papers
Abel NietoAarhus University, Yaoyu ZhaoUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Angela ChangUniversity of Waterloo, Justin PuUniversity of Waterloo
Link to publication DOI Pre-print Media Attached

Mon 16 Nov
Times are displayed in time zone: Central Time (US & Canada) change

05:00 - 06:20: S-6Research Papers at SPLASH-I
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford, Olivier FlückigerNortheastern University
05:00 - 05:20
Talk
Research Papers
Julia GabetImperial College London, Nobuko YoshidaImperial College London
Link to publication DOI Media Attached
05:20 - 05:40
Talk
Research Papers
Vlastimil DortCharles University, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Media Attached
05:40 - 06:00
Talk
Research Papers
Keigo ImaiGifu University, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London, Shoji YuenNagoya University
Link to publication DOI Media Attached
06:00 - 06:20
Talk
Research Papers
Abel NietoAarhus University, Yaoyu ZhaoUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Angela ChangUniversity of Waterloo, Justin PuUniversity of Waterloo
Link to publication DOI Pre-print Media Attached