The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Program logics and semantics tell a pleasant story about sequential composition: when executing (S_1; S_2), we first execute S_1 then S_2. To improve performance, however, processors execute instructions out of order, and compilers reorder programs even more dramatically.
In this talk, I will present PwT - a new result to appear at POPL'22. PwT is a compositional model that formalizes the real-world multiple-threaded systems using a logical approach. It enriches the standard event-based approach with preconditions and families of predicate transformers to calculate dependencies between instructions.
First, I will introduce the main challenges of concurrent semantics. Then I will show how concurrent program behaviors are determined by dependencies. Finally, I will demonstrate the basic idea of the logical approach to dependency calculation and support it with several examples.
Speaker: Ilya Kaysin
Google Meet: https://meet.google.com/myu-dhmz-gvu