Verification and Fence Insertion under the TSO Memory Model
Speaker
Date and Time
Thursday, October 25th, 2012 at 10:30
Location
Polacksbacken, room 1145
Abstract
Hardware optimizations on most shared memory parallel architectures cause memory accesses to take effect in an order different from that written in the program. This may cause bugs that are very difficult to find by testing. Reasoning about the reordering behavior is made difficult by the use of hardware buffers whose length is not a priori known. We investigate two approaches to automatic verification of programs running under the TSO memory model. We will also see how these approaches can be used to automatically infer the correct placement of memory fences in such programs.