Geheugenmodellen van programmeertalen: problemen, oplossingen en richtingen Programming Language Memory Models: Problems, Solutions, and Directions

Door optimalisaties in compilers en hardware bieden moderne programmeertalen geen sequentieel consistente geheugenmodellen. In plaats daarvan hebben ze zwakke geheugenmodellen die meer gedrag toestaan. Zulke geheugenmodellen moeten een balans vinden tussen prestaties en de garanties die ze softwareontwikkelaars bieden, of anders gezegd: de balans ligt eigenlijk tussen prestaties en gezond verstand. In deze talk introduceren we concurrency met zwak geheugen, bekijken we de eisen die aan geheugenmodellen van programmeertalen worden gesteld, onderzoeken we de modellen die in de industrie worden gebruikt (C11 en Java), inclusief hun nadelen, en bespreken we daarna oplossingen die de academische wereld heeft voorgesteld. We sluiten af met een bespreking van hoe je het beste geheugenmodel kiest voor jouw taal of VM, afhankelijk van je eisen. Spreker: Anton Podkopaev Hij is hoofd van het Programming Languages and Tools Lab bij JetBrains Research. Na zijn promotie aan de Staatsuniversiteit van Sint-Petersburg was hij postdoc bij MPI-SWS. Anton werkt aan rigoureuze wiskundige specificaties en bewijzen voor realistische concurrente systemen, waaronder CPU-architecturen zoals x86, ARM en Power, en talen als C/C++, Java en JavaScript. Zijn professionele interesses zijn onder meer het bewijzen van de correctheid van compilers, het verifiëren van concurrente algoritmen in zwakke geheugenmodellen, het mechaniseren van bewijzen in interactieve theorem provers, en functioneel programmeren. Agenda: 00:00 - Introductie 03:52 - Sequentiële consistentie 06:43 - Peterson's lock 11:11 - Laten we het voorbeeld vereenvoudigen 11:54 - Dekker's lock 23:51 - Tussentijdse conclusie 24:38 - Load buffering 30:30 - Eisen aan geheugenmodellen 34:00 - Correctheid van compileroptimalisaties 35:28 - Efficiënte compilatie naar hardware 36:32 - Eenvoudige modus voor niet-experts 46:01 - Bestaande geheugenmodellen van programmeertalen 48:14 - SC-behoudende optimalisaties in LLM [Marino et al., 2011] 51:45 - End-to-end SC via Volatile JVM [Liu et al., 2017, Liu et al., 2019] 58:26 - Declaratieve (axiomatische) geheugenmodellen 01:09:48 - Out-of-thin-air in het C/C++-geheugenmodel 01:17:23 - po U rf-cycli verbieden 01:20:37 - Undefined behavior en geheugenmodellen 01:27:34 - Afhankelijkheden behouden in LLVM [Ou and Demsky, 2018] Presentatie: https://drive.google.com/file/d/1AXl70iZ5KewQ9ZNlpePN7tIvVBAxROg3/view?usp=sharing #ProgrammingLanguage #MemoryModels

Due to compiler and hardware optimizations, modern programming languages do not provide sequential consistent memory models. Instead, they have weak memory models that allow for more behaviors. Such memory models have to find the balance between performance and the guarantees provided to software developers, or, put another way, the balance needed is actually between performance and sanity. In this talk, we’ll introduce weak memory concurrency, consider requirements imposed on programming language memory models, examine those used by industry (C11 and Java), including their drawbacks, and then discuss solutions proposed by the academic community. We’ll conclude with a discussion on how to choose the best memory model for your language or VM, depending on your requirements. Speaker: Anton Podkopaev He is the head of the Programming Languages and Tools Lab at JetBrains Research. He was a postdoc at MPI-SWS after getting his PhD at St. Petersburg State University. Anton works on rigorous mathematical specifications and proofs for realistic concurrency systems, including CPU architectures, such as x86, ARM, and Power, and languages like C/C++, Java, and JavaScript. His professional interests include proving compiler correctness, verifying concurrent algorithms in weak memory models, mechanizing proofs in interactive theorem provers, and functional programming. Agenda: 00:00 - Introduction 03:52 - Sequential Consistency 06:43 - Peterson’s lock 11:11 - Let’s simplify example 11:54 - Dekker’s lock 23:51 - Intermediate conclusion 24:38 - Load buffering 30:30 - Requirements to Memory Models 34:00 - Correctness of Compiler optimizations 35:28 - Efficient compilation to hardware 36:32 - Easy, non-expert mode 46:01 - Existing PL Memory Models 48:14 - SC-preserving optimizations in LLM [Marino et al., 2011] 51:45 - End-to-end SC via Volatile JVM [Liu et al., 2017, Liu et al., 2019] 58:26 - Declarative (Axiomatic) Memory Models 01:09:48 - Out-of-Thin-Air in C/C++ MM 01:17:23 - Forbidding po U rf cycles 01:20:37 - Undefined Behavior and Memory Models 01:27:34 - Preserving dependencies in LLVM [Ou and Demsky, 2018] Presentation: https://drive.google.com/file/d/1AXl70iZ5KewQ9ZNlpePN7tIvVBAxROg3/view?usp=sharing #ProgrammingLanguage #MemoryModels