Relaxed Memory Concurrency and Compiler Correctness

Soham Chakraborty

In this talk, I will present my work on formally defining a good concurrency model for C/C++ and proving that it satisfies both requirements. Unlike the prior state-of-the-art models, our model is easy to adapt and we have extended it to cover the full range of C/C++ features. I will conclude with a summary of my ongoing work and future research plans.

---

Previous: Artem Khyzha | Speculative Taint Tracking (and a formal analysis of its protection for speculatively-accessed data)
Next: Tobias Kappé | Guarded Kleene Algebra with Tests