Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Tue 25 Aug 2020 15:00 - 15:15 at ICFP NY 4 - New York 4 Chair(s): Stephanie Weirich
Wed 26 Aug 2020 03:00 - 03:15 at ICFP Asia 4 - Asia 4 Chair(s): Stephanie Weirich

Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code? To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing nonatomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model. We illustrate this claim via a number of case studies: we verify several implementations of locks with respect to a classic, memory-model-independent specification. Thus, a coarse-grained application that uses locks as the sole means of synchronization can be verified in the Concurrent-Separation-Logic fragment of Cosmo, without any knowledge of the weak memory model.

Tue 25 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

14:30 - 16:30: New York 4ICFP Program at ICFP NY 4
Chair(s): Stephanie WeirichUniversity of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

14:30 - 14:45
Talk
ICFP Program
DOI Pre-print Media Attached
14:45 - 15:00
Talk
ICFP Program
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI
15:00 - 15:15
Talk
ICFP Program
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI
15:15 - 15:30
Talk
ICFP Program
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI
15:30 - 15:45
Talk
ICFP Program
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print
15:45 - 16:00
Talk
ICFP Program
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI
16:00 - 16:15
Talk
ICFP Program
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI
16:15 - 16:30
Talk
ICFP Program
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto University, Japan
DOI

Wed 26 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

02:30 - 04:30: Asia 4ICFP Program at ICFP Asia 4
Chair(s): Stephanie WeirichUniversity of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

02:30 - 02:45
Talk
ICFP Program
DOI Pre-print Media Attached
02:45 - 03:00
Talk
ICFP Program
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI
03:00 - 03:15
Talk
ICFP Program
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI
03:15 - 03:30
Talk
ICFP Program
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI
03:30 - 03:45
Talk
ICFP Program
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print
03:45 - 04:00
Talk
ICFP Program
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI
04:00 - 04:15
Talk
ICFP Program
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI
04:15 - 04:30
Talk
ICFP Program
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto University, Japan
DOI