Loading...
Please wait, while we are loading the content...
Similar Documents
Runtime Model Checking of Multithreaded C Programs using Automated Instrumentation Dynamic Partial Order Reduction and Distributed Checking ⋆
| Content Provider | Semantic Scholar |
|---|---|
| Author | Yang, G. G. |
| Copyright Year | 2007 |
| Abstract | Conventional testing methods are inadequate for debugging multithreaded C programs because many “unexpected” thread interactions can only be manifested through very low probability event sequences that are easily missed during test creation. As a result, bugs can escape into the field, and often manifest years after code deployment [1]. While the approach of building formal models in modeling languages such as Promela [2] followed by model checking using tools such as SPIN [2] has been shown to be effective for verification, the burden of model extraction makes this approach inapplicable in general software development. Runtime model checking – first implemented in the Verisoft [3] tool – can help solve this problem by running the actual code under the control of a scheduling mechanism, and detecting violations of assertions (typically deadlocks and other safety properties). It is well recognized that when interleaving thread actions, one must prevent the interleaving of independent actions to avoid state explosion. Static partial order reduction methods achieve this objective by a priori (through static criteria) determining persistent sets (which are a subset of actions enabled at any given state) and only interleaving actions within persistent sets. This method is ineffective in the face of information that is difficult to compute statically. For instance, given the actions of two threads a[e1] and a[e2] that are simultaneously enabled, unless one can determine whether e1==e2, it is not possible to tell whether the actions commute. The dynamic partial order reduction (DPOR) approach of Flanagan and Godefroid [4] avoids this difficulty by taking advantage of the known values of expressions and pointer references (in the above example checking whether e1==e2 at runtime) to dramatically cut down the number of interleavings examined. It has been shown to be very effective in detecting safety violations and deadlocks by systematically exploring all relevant interleavings of the multithreaded programs under specific inputs (meaning, specific external input drivers). |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.fm2008.abo.fi/tutorials/Tutorial_ModelCheck.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
