Verification and Fence Insertion under the TSO Memory Model
Date and Time
Thursday, October 25th, 2012 at 10:30
Polacksbacken, room 1145
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.