Loading...
Please wait, while we are loading the content...
Similar Documents
Runtime model checking of multithreaded c/c++ programs abstract.
| Content Provider | CiteSeerX |
|---|---|
| Author | Kir, Robert M. Chen, Xiaofang Gopalakrishnan, Ganesh Yang, Yu |
| Abstract | We present inspect, a tool for model checking safety properties of multithreaded C/C++ programs where threads interact through shared variables and synchronization primitives. The given program is mechanically transformed into an instrumented version that yields control to a centralized scheduler around each such interaction. The scheduler first enables an arbitrary execution. It then explores alternative interleavings of the program. It avoids redundancy exploration through dynamic partial order reduction(DPOR) [1]. Our initial experience shows that inspect is effective in testing and debugging multithreaded C/C++ programs. We are not aware of DPOR having been implemented in such a setting. With inspect, we have been able to find many bugs in real applications. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Safety Property Instrumented Version Redundancy Exploration Centralized Scheduler Dynamic Partial Order Reduction Real Application Alternative Interleavings Initial Experience Show Synchronization Primitive Many Bug Runtime Model Checking Yield Control Arbitrary Execution Multithreaded Program Abstract Multithreaded Program |
| Content Type | Text |
