Write a Blog >>
Wed 22 Jan 2020 16:18 - 16:40 at Ile de France III (IDF III) - Concurrency / Memory Chair(s): Susmit Sarkar

The Rust programming language supports safe systems programming by means of a strong ownership-tracking type system. In their prior work on RustBelt, Jung et al. began the task of setting Rust’s safety claims on a more rigorous formal foundation. Specifically, they used Iris, a Coq-based separation logic framework, to build a machine-checked proof of semantic soundness for a λ-calculus model of Rust, as well as for a number of widely-used Rust libraries that internally employ unsafe language features. However, they also made the significant simplifying assumption that the language is sequentially consistent. In this paper, we adapt RustBelt to account for the relaxed-memory operations that concurrent Rust libraries actually use, in the process uncovering a data race in the Arc library. We focus on the most interesting technical problem: how to reason about resource reclamation under relaxed memory, using a logical construction we call synchronized ghost state.

Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change

15:35 - 16:40: Concurrency / MemoryResearch Papers at Ile de France III (IDF III)
Chair(s): Susmit SarkarUniversity of St. Andrews
15:35 - 15:56
Talk
Persistency Semantics of the Intel-x86 Architecture
Research Papers
Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, Germany
Link to publication DOI Media Attached
15:56 - 16:18
Talk
Reductions for Safety Proofs
Research Papers
Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto
Link to publication DOI Media Attached
16:18 - 16:40
Talk
RustBelt Meets Relaxed Memory
Research Papers
Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-SWS
Link to publication DOI Media Attached