Sciweavers

Share
VMCAI
2016
Springer

Hybrid Analysis for Partial Order Reduction of Programs with Arrays

3 years 14 days ago
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
An important component of efficient approaches to software model checking and systematic concurrency testing is partial order reduction, which eliminates redundant non-deterministic thread scheduling choices during the state space traversal. Thread choices have to be created only at the execution of actions that access the global state visible by multiple threads, so the key challenge is to precisely determine the set of such globally-relevant actions. This includes accesses to object fields and array elements, and thread synchronization. However, some tools completely disable thread choices at actions that access individual array elements in order to avoid state explosion. We show that they can miss concurrency errors in such a case. Then, as the main contribution, we present a new hybrid analysis that identifies globally-relevant actions that access arrays. Our hybrid analysis combines static analysis with dynamic analysis, usage of information from dynamic program states, and sym...
Pavel Parizek
Added 11 Apr 2016
Updated 11 Apr 2016
Type Journal
Year 2016
Where VMCAI
Authors Pavel Parizek
Comments (0)
books