Fast and accurate static data-race detection for concurrent programs
AssigneeNEC Laboratories America, Inc.
InventorsVineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
A system and method for race warning generation for computer program verification includes determining shared variables and determining context-sensitive points-to sets for lock pointers by focusing on pointers that may affect aliases of lock pointers, and by leveraging function summarization. Locksets are determined at locations where shared variables are accessed using the points-to sets for lock pointers. Warnings are based on disjointness of locksets.
Claims25
A method for race warning generation for computer program verification, comprising:
- determining shared variables;
- determining context-sensitive points-to sets for lock pointers by focusing on pointers that may affect aliases of lock pointers, and by leveraging function summarization;
- determining locksets at locations where shared variables are accessed using the points-to sets for lock pointers;
- and
- generating warnings based on disjointness of locksets.
A computer readable medium for race warning generation for computer program verification comprising a computer readable program, wherein the computer readable program when executed on a computer causes the computer to perform the steps of:
- determining shared variables;
- determining context-sensitive points-to sets for lock pointers by focusing on pointers that may affect aliases of lock pointers, and by leveraging function summarization;
- determining locksets at locations where shared variables are accessed using the points-to sets for lock pointers;
- and
- generating warnings based on disjointness of locksets.
A method for race warning generation for computer program verification, comprising:
- automatically determining shared variables by performing a dataflow analysis by performing the dataflow analysis to determine only genuine variable updates by determining which variables are written to in the program;
- determining context-sensitive points-to sets for lock pointers efficiently by focusing on pointers that may affect aliases of lock pointers, and by leveraging function summarization;
- determining locksets at locations where shared variables are accessed;
- and
- generating race warnings based on the locksets and lock acquisition patterns.
Dependencies are inferred from the claim text.