Invention Grant
US08200474B2 Dynamic model checking with property driven pruning to detect race conditions
有权
动态模型检查与属性驱动修剪检测竞争条件
- Patent Title: Dynamic model checking with property driven pruning to detect race conditions
- Patent Title (中): 动态模型检查与属性驱动修剪检测竞争条件
-
Application No.: US12397696Application Date: 2009-03-04
-
Publication No.: US08200474B2Publication Date: 2012-06-12
- Inventor: Chao Wang , Aarti Gupta
- Applicant: Chao Wang , Aarti Gupta
- Applicant Address: US NJ Princeton
- Assignee: NEC Laboratories America, Inc.
- Current Assignee: NEC Laboratories America, Inc.
- Current Assignee Address: US NJ Princeton
- Agent James Bitetta; Bao Tran; Joseph Kolodka
- Main IPC: G06F9/45
- IPC: G06F9/45
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.
Public/Granted literature
- US20090282288A1 DYNAMIC MODEL CHECKING WITH PROPERTY DRIVEN PRUNING TO DETECT RACE CONDITIONS Public/Granted day:2009-11-12
Information query
