Invited Talk by Dr. Saurabh Joshi- 'Property-Driven Fence Insertion using Reorder Bounded Model Checking'

Invited Talk by Dr. Saurabh Joshi: ‘Property-Driven Fence Insertion using Reorder Bounded Model Checking’

Title: Property-Driven Fence Insertion using Reorder Bounded Model Checking
Speaker: Dr. Saurabh Joshi (University of Oxford, UK)

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.

Bio of the speaker:

Saurabh is a post-doc researcher in the Systems Verification Group in the Department of Computer Science at the University of Oxford. He obtained his PhD from IIT Kanpur and his Masters degree from IIT Bombay. In between, he was also working at IBM India Research Lab. Saurabh has research interests in Formal Methods and recently he has also started working in the domain of constraint solving.

Where Room no. 123 (map) Video call [https://plus.google.com/hangouts//iith.ac.in/invited-talk-by](https://plus.google.com/hangouts//iith.ac.in/invited-talk-by)

Dates:
Wednesday, May 20, 2015 - 11:30 to 12:30