Date(s) - 07/03/2016
2:00 pm - 3:00 pm
Speaker: Prof. Daniel Kroening, Oxford University.
Date: Monday, March 7, 2016
Location: Taub 601CS building
Analysis of Programs with Weak Memory Semantics
I will give a brief tutorial of weak memory consistency and formal models for these. I will then give an overview of analysis techniques we have developed for programs with weak consistency semantics. We begin with a simple but powerful result that non-relational analyses are sound for any sensible memory model (APLAS 2011). We then show a technique for transforming a program with TSO/PSO/ARM/Power semantics into one with sequential consistency by inserting buffers. I then show a direct encoding of weak memory semantics into a set of constraints over partial orders. Finally, I advertise two techniques for inserting fences into programs to remove undesired weakenings.