Effective Stateless Model Checking for C/C++ Concurrency

Add to your list(s) Download to your calendar using vCal

• Viktor Vafeiadis, MPI-SWS
• Tuesday 05 December 2017, 10:30-11:30
• FW26.

If you have a question about this talk, please contact Victor Gomes.

I will present a stateless model checking algorithm for verifying concurrent programs running under RC11 , a repaired version of the C/C++11 memory model without dependency cycles. Unlike previous approaches, which enumerate thread interleavings up to some partial order reduction improvements, our approach works directly on execution graphs and (in the absence of RMW instructions and SC atomics) avoids redundant exploration by construction. We have implemented a model checker, called RCMC , based on this approach and applied it to a number of concurrent programs. Our experiments confirm that RCMC is significantly faster, scales better than other model checking tools for sequential consistency, and is also more resilient to small changes in the benchmarks.

(This is joint work with Michalis Kokologiannakis, Ori Lahav, and Konstantinos Sagonas, and will appear at POPL ’18.)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.