Department of Information Technology

Verification and Fence Insertion under the TSO Memory Model

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.

Back to the seminar page

Updated  2012-10-22 17:12:50 by Frédéric Haziza.