Detecting data race and atomicity violation via typestate-guided static analysis

A method of analyzing computer instructions, the computer instructions specifying actions by a computer and the computer instructions implementing a program, the method comprising:

• stepping through the computer instructions to simulate at least one control flow of the program;
• and
• while stepping through the computer instructions, for each variable in at least one variable-lock association, each variable-lock association being comprised of a variable and a lock associated with the variable that is intended to guard the variable from concurrent access:
• when the lock associated with the variable is referenced in an operation in the computer instructions that instructs the computer to leave a critical section, then changing a locking state associated with the variable to an unlocked state;
• when the locking state associated with the variable is the unlocked state and when the variable is referenced in a type state-dependent operation in the computer instructions, then indicating a warning, the variable being further associated with a type state, wherein executing a type state-dependent operation referencing the variable instructs the computer to enter into a particular error condition when the variable is associated with the type state in a first set of type states and executing a type state-dependent operation referencing the variable does not instruct the computer to enter into the particular error condition when the variable is associated with the type state in a second set of type states;
• when the lock associated with the variable is referenced in an operation in the computer instructions that instructs the computer to enter the critical section, then changing the locking state associated with the variable to a locked state, and changing the type state associated with the variable to an uninitialized state;
• and
• when the locking state associated with the variable is the locked state, when the type state associated with the variable is the uninitialized state, and when the variable is referenced in another type state-dependent operation in the computer instructions, then indicating the warning.