YoVDO

Putting Weak Memory in Order via a Promising Intermediate Representation

Offered By: ACM SIGPLAN via YouTube

Tags

Concurrency Courses Formal Verification Courses Coq Courses

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
Explore an innovative approach to developing an 'in-order' shared-memory concurrency model for languages like C and C++ in this conference talk from PLDI 2023. Delve into the challenges of creating a model that executes instructions following program order while supporting non-atomic accesses and validating compiler optimizations. Learn how the researchers utilize the distinction between a source model and an intermediate representation (IR) model to achieve this goal. Examine the implications for relaxed atomic accesses and the proposed pragmatic approach to address load-store reordering. Gain insights into the mechanized Coq proofs for the correctness of mappings from source to IR and from IR to Armv8. Discover how this work relates an in-order source model to an out-of-order IR model, aiming to create an in-order source semantics without performance overhead for non-atomics.

Syllabus

[PLDI'23] Putting Weak Memory in Order via a Promising Intermediate Representation


Taught by

ACM SIGPLAN

Related Courses

Verifying the LLVM
Strange Loop Conference via YouTube
Beweisbar sichere Software
media.ccc.de via YouTube
RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube
Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube
Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube