| Title | : | Property-Driven Fence Insertion using Reorder Bounded Model Checking |
| Speaker | : | Saurabh Joshi (University of Oxford, UK) |
| Details | : | Mon, 11 May, 2015 11:00 AM @ BSB 361 |
| Abstract: | : | Modern processor architectures employ optimizations such as store buffers. Such an optimization, however, may result in program executions that violate Sequential Consistency. In other words, program statements may appear to have been reordered violating the program order. Some of these executions may result in safety property (assertion) violation. Architectures provide fence instructions (memory barriers) that can be inserted to avoid any unwanted reordering. Too many fences may degrade performance drastically whereas too few fences may result in a buggy behaviour. Due to non-determinism in scheduling and reordering, it may be very difficult for even an expert programmer to insert fences in an optimal manner.
Automated techniques have been proposed for property-driven fence insertion that repairs a concurrent program through fence insertion by suggesting optimal fence placement for a given architecture. In this talk, I will introduce a technique we call 'Reorder Bounded Model-Checking' (ROBMC). ROBMC introduces a new parameter in the world of bounded model checking. We show that ROBMC based approach outperforms traditional property-driven fence insertion techniques. This work has been accepted for publication at FM 2015. Toward the end of the talk, I will also briefly discuss other research works that I have been involved in. |
