Research group

Programming Languages and Tools Lab

The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency

November 8

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: