IPC분류정보
국가/구분 |
United States(US) Patent
등록
|
국제특허분류(IPC7판) |
|
출원번호 |
UP-0403414
(2006-04-12)
|
등록번호 |
US-7752605
(2010-07-26)
|
발명자
/ 주소 |
- Qadeer, Shaz
- Elmas, Tayfun
|
출원인 / 주소 |
|
대리인 / 주소 |
|
인용정보 |
피인용 횟수 :
20 인용 특허 :
0 |
초록
▼
A data race detection system is described which precisely identifies data races in concurrent programs. The system and techniques described utilize locksets to maintain information while searching through executions of a concurrent program. The locksets are updated according to program statements in
A data race detection system is described which precisely identifies data races in concurrent programs. The system and techniques described utilize locksets to maintain information while searching through executions of a concurrent program. The locksets are updated according to program statements in the concurrent program. The dynamic updating of the locksets, combined with a less conservative approach then used in existing lockset data race detection techniques, allows the technique to be precise; that is, the technique does not report false positives when searching a program.
대표청구항
▼
We claim: 1. A method for detecting one or more data races in a concurrent program, the method comprising performing by a computer the acts of: generating locksets for an execution of the program; wherein locksets comprise: one or more thread locksets, each thread lockset representing locks owned b
We claim: 1. A method for detecting one or more data races in a concurrent program, the method comprising performing by a computer the acts of: generating locksets for an execution of the program; wherein locksets comprise: one or more thread locksets, each thread lockset representing locks owned by a thread in the execution; and one or more variable locksets, each variable lockset representing locks which may provide protection for a variable in the execution; and wherein generating locksets for the execution comprises: creating locksets for the execution; and modifying content of the locksets according to program statements in the execution, wherein modifying the content of the locksets according to program statements comprises, for at least some program statements in a current thread which do not involve accesses to a variable, adding locks from a lockset of the current thread to the variable lockset; and analyzing the generated locksets for the execution to determine a set of data race variables in the program, wherein, for each variable in the set of data race variables, the execution of the program involves a data race on the variable. 2. The method of claim 1, wherein, for every variable involved in a data race in the execution of the program, the set of data race variables comprises the variable. 3. The method of claim 1, wherein in a case that the program statement in a current thread which does not involve accesses to a variable is a statement to acquire a lock, then said modifying the content of the locksets according to program statements comprises: adding the lock to a thread lockset for the current thread; and for each variable in the execution, when there is at least one lock in common between the variable lockset for the variable and the lockset for the current thread, adding every lock in the thread lockset for the current thread to the variable lockset. 4. The method of claim 1, wherein in a case that the program statement in a current thread which does not involve accesses to a variable is a statement to release a lock, then said modifying variable locksets based on the program statement comprises removing the lock from a thread lockset for the current thread. 5. The method of claim 1, wherein in a case that the program statement in a current thread which does not involve accesses to a variable is a statement to fork a new thread, then said modifying the content of the locksets according to program statements comprises: creating a new thread lockset for the new thread; and for each variable in the execution, when there is at least one lock in common between the variable lockset for the variable and the lockset for the current thread, adding the new thread as a lock in the variable lockset. 6. The method of claim 1, wherein in a case that the program statement in a current thread which does not involve accesses to a variable is a statement to join a thread to the current thread, then said modifying the content of the locksets according to program statements comprises, for each variable in the execution, when there is at least one lock in common between the variable lockset for the variable and the lockset for the thread which is to be joined, adding every lock in the thread lockset for the thread to be joined to the variable lockset. 7. The method of claim 1, wherein analyzing the generated locksets for the execution comprises, when a program statement in the execution is a data access on an accessed variable: determining if there is a lock in common between a thread lockset for the current thread and a variable lockset for the accessed variable; when there is no lock in common, determining that there is a data race on the variable for the execution; and when there is at least one lock in common, modifying the variable lockset to contain the locks which were contained in the thread lockset at the time of the data access. 8. The method of claim 7, wherein: the one or more variable locksets comprise, for each variable in the execution: a read variable lockset representing locks which may provide read access protection for a variable in the execution; and a write variable lockset representing locks which may provide write access protection for a variable in the execution; and wherein analyzing the generated locksets for the execution comprises, when a program statement in the execution is a write access on an accessed variable: determining if there is a lock in common between a thread lockset for the current thread and a write variable lockset for the accessed variable; and when there is no lock in common, determining that there is a data race on the variable for the execution. 9. The method of claim 8, wherein analyzing the generated locksets for the execution comprises, when a program statement in the execution is a read accesses on an accessed variable, ignoring whether there may be a data race on the variable. 10. The method of claim 1, further comprising: searching through one or more executions of the program; repeating generating locksets and analyzing the generated locksets for each searched execution to determine data race variables for the searched execution; and including the one or more determined data race variables for the searched execution in the set of data race variables. 11. The method of claim 2, wherein the method operates without assumptions about any particular synchronization mechanism used in the execution. 12. A computer system for checking a model of a program, the program utilizing multiple threads, the computer system comprising: a memory storing a data race detection module; and a processing unit for running the data race detection module, wherein said data race detection module is configured to: perform a search of executions of the program; and for each execution searched: generate locksets for threads and references in the execution by adding locks to locksets for references based on non-access operations in the program, the locksets configured to comprise information which precisely demonstrates data races, wherein locksets comprise one or more thread locksets, each thread lockset representing locks owned by a thread in the execution and one or more variable locksets, each variable lockset representing locks which may provide protection for a variable in the execution, and wherein generating locksets for threads and references in the execution comprises creating locksets for the execution and modifying content of the locksets according to program statements in the execution, wherein modifying the content of the locksets according to program statements comprises, for at least some program statements in a current thread which do not involve accesses to a variable, adding locks from a lockset of the current thread to the one or more variable locksets; analyze the locksets generated for the execution to determine if a data race must exist on a reference in the execution; when a data race exists for a reference, record that a data race exists for the reference. 13. The system of claim 12, wherein: the data race detection module is configured to analyze the locksets by: determining, for each reference access, which, if any, references contained in the lockset for a thread containing the reference access are contained in the lockset for the reference; and when no member of the lockset for the reference is contained in the lockset for a thread containing the reference access, determining that there is a data race on the reference. 14. The system of claim 13, wherein: locksets for references in the execution comprise locksets for reference writes and locksets for reference reads; and determining, for each reference access, which, if any, references contained in the lockset for a thread containing the reference access are contained in the lockset for the reference comprises determining, for each reference write, which, if any, references contained in the lockset for the thread containing the reference access are contained in the lockset for reference writes for the reference. 15. One or more computer-readable storage media containing instructions which, when executed by a computer, cause the computer to perform a method for identifying data races on an execution of a concurrent program, the method comprising: maintaining a set of locksets for threads and variables used in the execution, the locksets comprising information sufficient to allow a precise data race analysis on the execution, wherein said maintaining a set of locksets for threads and variables used in the execution comprises adding locks from locksets for threads to locksets for variables based on semantics of program statements in the execution; wherein locksets comprise: one or more thread locksets, each thread lockset representing locks owned by a thread in the execution; and one or more variable locksets, each variable lockset representing locks which may provide protection for a variable in the execution; and wherein maintaining the set of locksets for threads and variables used in the execution comprises: creating locksets for the execution; and modifying content of the locksets according to program statements in the execution, wherein modifying the content of the locksets according to program statements comprises, for at least some program statements in a current thread which do not involve accesses to a variable, adding locks from a lockset of the current thread to the one or more variable locksets; and analyzing the set of locksets to determine which variables see a data race during the execution. 16. The computer-readable media of claim 15, wherein: analyzing the set of locksets comprises: at program statement in a thread, the program statement indicating a write to a variable, determining if any locks held in a lockset maintained for the thread in the execution are held in common with a lockset maintained for the variable in the execution; and if no locks are held in common, determining that the variable being written to in the program statement sees a data race. 17. The computer-readable media of claim 15, wherein the method further comprises: nondeterministically searching through executions of the program; and repeating maintaining a set of locksets and analyzing the set of locksets for each searched execution.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.