Dynamic model checking with property driven pruning to detect race conditions
US8200474B2 · kind B2 · utility
2Cited by
0References
24Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Mar 4, 2009 |
| Grant date | Jun 12, 2012 |
| Priority date | — |
| Expiry date | Oct 13, 2030 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3612
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A system and method for dynamic data race detection for concurrent systems includes computing lockset information using a processor for different components of a concurrent system. A controlled execution of the system is performed where the controlled execution explores different interleavings of the concurrent components. The lockset information is used during the controlled execution to check whether a search subspace associated with a state in the execution is free of data races. A race-free search subspace is dynamically pruned to reduce resource usage.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.