	US 7,555,418 B1
	Procedure summaries for multithreaded software
Shaz Qadeer, Seattle, Wash. (US); Niels Jakob Rehof, Redmond, Wash. (US); and Sriram K. Rajamani, Bellevue, Wash. (US)
Assigned to Microsoft Corporation, Redmond, Wash. (US)
Filed on Dec. 19, 2003, as Appl. No. 10/742,695.
Int. Cl. G06F 9/45 (2006.01)

U.S. Cl. 703—22

19 Claims

1. A computer program product embodied on a first computer-readable medium and comprising code that, when executed, causes a computer to perform a method of generating a partial procedure summary of a procedure of multithreaded software, wherein the procedure performs a plurality of actions when executed, the method comprising:

during a reachability analysis of at least a portion of the multithreaded software, reaching the procedure at a first point in the reachability analysis;

when the procedure is reached at the first point in the reachability analysis,

1) identifying at least one plurality of the actions within the procedure as atomically modelable with respect to multithreaded execution of the procedure as atomically modelable actions, wherein the atomically modelable actions are not subject to interruption by other threads, and

2) generating, by the computer, the at least one partial procedure summary of the procedure from the identified atomically modelable actions, wherein the at least one partial procedure summary comprises at least one state pair, wherein the at least one state pair models an initial state and a resulting state of the identified atomically modelable actions;

storing the at least one partial procedure summary of the procedure of multithreaded software on a second computer readable medium;

during continuation of the reachability analysis, at a second point in the reachability analysis, reaching the procedure a second time; and

wherein if an initial state of the procedure reached the second time is the same as the initial state of the at least one partial procedure summary, then the resulting state of the at least one partial procedure summary is used as a state of the procedure in the reachability analysis.