Sciweavers

Share
CAV
2006
Springer

Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study

10 years 3 months ago
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study
Many multithreaded programs employ concurrent data types to safely share data among threads. However, highly-concurrent algorithms for even seemingly simple data types are difficult to implement correctly, especially when considering the relaxed memory ordering models commonly employed by today's multiprocessors. The formal verification of such implementations is challenging as well because the high degree of concurrency leads to a large number of possible executions. In this case study, we develop a SAT-based bounded verification method and apply it to a representative example, a well-known twolock concurrent queue algorithm. We first formulate a correctness criterion that specifically targets failures caused by concurrency; it demands that all concurrent executions be observationally equivalent to some serial execution. Next, we define a relaxed memory model that conservatively approximates several common shared-memory multiprocessors. Using commit point specifications, a suite ...
Sebastian Burckhardt, Rajeev Alur, Milo M. K. Mart
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CAV
Authors Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin
Comments (0)
books