Aarhus University Seal / Aarhus Universitets segl

Special talk by Jean Pichon-Pharabod on Making sense of relaxed shared-memory concurrency

16.02.2021 | Søs Küster Markussen

Date Wed 24 Feb
Time 09:00 10:00
Location Online - Microsoft teams meeting

Special talk by Jean Pichon-Pharabod on Making sense of relaxed shared-memory concurrency

Abstract: About 60 years of clever design tricks have made computers really fast and power-efficient. However, the combined effect of these accumulated tricks, in particular on shared memory concurrency is at best confusing, if not completely unclear. The resulting complexity pervades many interfaces that programmers rely on: hardware architectures like ARM, and programming languages, both low-level like C, C++, or Rust, and higher-level, like Java, JavaScript, or WebAssembly. A particular challenge that programming languages pose is the out-of-thin-air problem, which, despite being a topic of active research, had been open since about 2005. In this talk, I will describe my work: (1) on mathematically capturing this unclear behaviour, so programmers have a definite reference, called a memory model, for a variety of programming languages which have different requirements; (2) on making these memory models more accessible, via oracle test tools and more programmer-friendly versions; (3) on model-checking tools and separation logics to verify programs that rely on these memory models. I will also discuss how I saw the same challenge resurface in educational programming, and my ideas to address it.

CS frontpage, Featured, Public/media