Analysis of Programs with Weak Memory Semantics

  • Map Unavailable

    Date(s) - 07/03/2016
    2:00 pm - 3:00 pm

    Categories No Categories

    Speaker:  Prof. Daniel Kroening, Oxford University.
    Date: Monday, March 7, 2016
    Time: 14:00-15:00 
    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.