Patent Publication Number: US-2013239093-A1

Title: Parallelizing top-down interprocedural analysis

Description:
BACKGROUND 
     As computer programs have continued to increase in complexity, importance of program verification has likewise increased. For example, many programs have hundreds of thousands or even millions of lines of code, and prior to such a program being deployed, it is often desirable to verify that the program will operate as intended by its developers. It is to be understood that program verification differs from location of bugs in computer-executable code. For example, an error exists in the source code that would not allow the resulting program to be interpretable by a computer processor, typically a compiler will include bug checking functionality that identifies the errors in the source code. In many cases, however, the program that includes no bugs may still not operate as intended by its developers. This is especially true when multiple developers are modifying different parts of code at different geographic locations. 
     There generally exists two different types of program verification tools; the first type is a static analysis tool that performs program verification without actually executing the program. In contrast, dynamic program analysis is the analysis of computer-executable code when such code is executed. Thus, dynamic program analysis is performed by executing a program built from desirably tested code on a real or virtual processor. Generally, this involves ascertaining test inputs to provide to the executing program, such that the behavior of the program with the test inputs can be observed. 
     In conventional program verification that utilizes static analysis, two techniques are typically employed. The first technique can be referred to as a bottom-up analysis. A bottom-up analysis is performed by processing a call graph of a computer program upwards from the leaves of the call graph. Therefore, for example, in a bottom-up analysis, before a procedure P i  is analyzed, sub-procedures that are called by P i  are analyzed, and for each sub-procedure a summary is computed, typically without considering be calling context of the respective sub-procedure. During the analysis of P i , the summary of a called sub-procedure is utilized to calculate the effects of calling the sub-procedure (instead of the body of the sub-procedure). An inherent advantage of bottom-up analysis is its modularity, as there is decoupling between callers of a procedure and the analysis of the body of such procedure. 
     In contrast, a top-down analysis begins from the root of the call graph for a program, and proceeds downward such that each procedure in the program is analyzed in the context in which it is called. It can be ascertained that a program verification tool that utilizes top-down analysis is typically more precise than program verification tools that utilize bottom-up analysis. As each analysis of a program procedure is undertaken with respect to its calling context, the summary for such context is caused to be relatively precise. A trade-off to the increased precision of top-down analysis, however, has been the lack of modularity when performing such analysis. 
     SUMMARY 
     The following is a brief summary of subject matter that is described in greater detail herein. This summary is not intended to be limiting as to the scope of the claims. 
     Described herein are various technologies pertaining to parallelizing top-down interprocedural analysis of a computer program. Computer programs can be represented by a call graph, wherein nodes of the call graph represent procedures (methods), and a directed edge between a first node and a second node represents a call from the procedure represented by the first node to a procedure represented by the second node. It can therefore be ascertained that a root node in the call graph represents a main procedure in the computer program, while the remaining nodes represent sub-procedures in the computer program. Described herein are technologies which employ a map/reduce style parallelism to scale top-down analysis of the computer program. 
     In operation, a program that is desirably subjected to a top-down analysis can be retained in a data store, and a query that is desirably executed over such program can be received. For example, the query can be formulated to ascertain whether the program ever reaches a particular state, to ascertain whether it is possible for a certain procedure to be reached, or the like. An intraprocedural analysis algorithm can then process the query (referred to as a main query) over the main procedure of the computer program (the procedure represented by the root node in the call graph). The intraprocedural analysis algorithm can explore paths in the main procedure of the computer program (forward, backward, or some combination of forward and backward). When the analysis algorithm encounters a method call to a sub-procedure, such algorithm automatically formulates a sub-query for the sub-procedure, wherein a result of the sub-query is needed to answer the main query. A summary of the respective sub-procedure can be searched for in a database of summaries in connection with answering the sub-query. If a summary for such sub-procedure is located, the sub-query can be answered utilizing the summary and processing can continue. If there is no suitable summary for the sub-procedure, then the sub-query can be transitioned to a Ready state and added to a set of queries to be returned. Subsequently, other paths in the main procedure are explored, and the same strategy is repeated, thereby generating multiple sub-queries that are to be executed over respective sub-procedures. The processing of the main query over the main procedure halts when further analysis is unable to be performed without obtaining answers to the sub-queries. 
     After a plurality of sub-queries have been formulated and returned, such sub-queries can be scheduled for execution in parallel across multiple computing nodes. A computing node may be a processor core and accessible memory, a processor and accessible memory, an independent computing device (e.g., a personal computing device, a server), or the like. It can be ascertained that the multiple computing nodes can process the sub-queries in parallel. The process of formulating sub-queries and returning results (if possible) is repeated until there is sufficient information to answer the main query. 
     Other aspects will be appreciated upon reading and understanding the attached figures and description. 
    
    
     
       BRIEF DESCRIPTION OF THE DRAWINGS 
         FIG. 1  is a functional block diagram of an exemplary system that facilitates parallelizing interprocedural top-down analysis of a computer program. 
         FIG. 2  is a functional block diagram of an analysis component that can perform an intraprocedural analysis on a procedure of a computer program. 
         FIG. 3  is an exemplary computer program. 
         FIG. 4  is an exemplary state machine that illustrates possible states of a query that is to be executed over a procedure of a computer program. 
         FIG. 5  is an exemplary depiction of an interprocedural top-down analysis over the computer program shown in  FIG. 3 . 
         FIG. 6  is a flow diagram that illustrates an exemplary methodology for performing an interprocedural top-down analysis of a computer program. 
         FIG. 7  is an exemplary computing system. 
     
    
    
     DETAILED DESCRIPTION 
     Various technologies pertaining to parallelizing a top-down interprocedural analysis of a computer program will now be described with reference to the drawings, where like reference numerals represent like elements throughout. In addition, several functional block diagrams of exemplary systems are illustrated and described herein for purposes of explanation; however, it is to be understood that functionality that is described as being carried out by certain system components may be performed by multiple components. Similarly, for instance, a component may be configured to perform functionality that is described as being carried out by multiple components. Additionally, as used herein, the term “exemplary” is intended to mean serving as an illustration or example of something, and is not intended to indicate a preference. 
     As used herein, the terms “component” and “system” are intended to encompass computer-readable data storage that is configured with computer-executable instructions that cause certain functionality to be performed when executed by a processor. The computer-executable instructions may include a routine, a function, or the like. It is also to be understood that a component or system may be localized on a single device or distributed across several devices. 
     With reference now to  FIG. 1 , an exemplary system that facilitates parallelizing top-down interprocedural analysis of a computer program is illustrated. The system  100  comprises a data store  102 , which can be any suitable computer-readable data storage device, including but not limited to memory of a computing device, a hard drive, a removable disk, a flash drive etc. The data store  102  comprises an executable program  104  that is written in a suitable language. For example, the executable program  104  can be written in C, C+C++, C#, or the like. In an exemplary embodiment, the executable program can be a device driver. The executable program  104 , as will be understood by one skilled in the art, can be represented through utilization of a call graph, where nodes of the call graph represent procedures (methods), while directed edges represent calls between procedures. A root node in the call graph, therefore, represents a main procedure of the executable program  104  while other nodes in the call graph represent sub-procedures. 
     The system  100  further comprises an analysis framework  106  that receives the executable program  104  and a query that is desirably executed over the executable program  104 . The analysis framework  106  facilitates parallelizing top-down interprocedural analysis of the executable program  104  based at least in part upon the query. In an example, the query can be constructed to ascertain whether the executable program  104  can, during execution thereof, reach a particular intermediate state or output state (e.g. whether certain values of variables in the executable program  104  can be in a range specified in the query). In another example, the query can be a reachability query, wherein it is desirable to understand whether the executable program  104  ever reaches a certain function (e.g. an error function). 
     The system  100  further comprises a plurality of computing nodes  108 - 110  that are in communication with the analysis framework  106 . While shown as being separate therefrom, it is to be understood that all or portions of the analysis framework  106  may be included in one or more of the computing nodes  108 - 110 . In an exemplary embodiment, a computing node, as the term is used herein, can refer to a core of a processor and memory that is accessible by such core. In another example, a computing node can refer to a processor and memory that is accessible by the processor. In still yet another example, a computing node can refer to an entirety of a computing device (a server, a personal computing device, etc.). In still yet another example, a computing node may be a system on a chip (SoC) or a cluster on a chip (CoC). Still further, a computing node may be a virtual processor and corresponding virtual memory in a virtualized system. 
     Each of the computing nodes  108 - 110  has an analysis component  112   a - 112   b,  respectively (collectively referred to as analysis component  112 ). The analysis component  112  is and intraprocedural analysis algorithm which, as will be described below, can be configured to formulate queries as well as execute a query over a procedure in the executable program  104 . 
     The system  100  further comprises a data store  114  that retains procedure summaries  116 . While shown as being different from the data store  102 , it is to be understood that a data store or series of distributed data stores can retain the executable program  104  and the procedure summaries  116 . The data store  114  is accessible to each of the computing nodes  108 - 110  and is further accessible to the analysis framework  106 . As will be understood, a procedure summary can represent potential output states of a procedure with respect to a corresponding calling context of such procedure. In an exemplary embodiment, the analysis component  112  can be configured to generate a procedure summary responsive to receipt of an identity of a particular procedure and a query that is to be executed over such procedure. Furthermore, the analysis component  112  can output an answer to a query based at least in part upon a procedure summary in the procedure summaries  116  of the data store  114 . For example, the analysis component  112  can receive a particular procedure and a query that is to be executed over such procedure. Execution of the query, however, may require obtaining a summary of a sub-procedure that is called by such procedure. The analysis component  112  can access the data store  114  and retrieve the requisite summary and can output an answer to the query based at least in part upon the summary of the sub-procedure that is called by the procedure. Furthermore, in such a case, the analysis component  112  can generate a summary for the procedure (which is based upon the summary of the sub-procedure called by the aforementioned procedure), and can cause such summary to be retained in the data store  114  such that the summary can be accessed by other executing instantiations of the analysis component  112 . 
     The analysis framework  106  comprises a receiver component  118  that receives the executable program  104 , which, as described above, comprises a main procedure and a plurality of sub-procedures. The receiver component  118  additionally receives the query, which can be referred to herein as a main query, wherein the main query is desirably executed over the executable program  104 . The analysis framework  106  also comprises a scheduler component  120  that, responsive to receipt of the main query, assigns computing tasks across the plurality of computing nodes  108 - 110 , wherein the computing tasks are to be executed in parallel. Each of the computing nodes  108 - 110  is assigned a computing task for a different respective sub-procedure in the executable program  104 . The scheduler component  120  can schedule the computing tasks to execute on the computing nodes  108 - 110  in parallel, wherein execution of such computing tasks in parallel results in performance of a top-down interprocedural analysis of the executable program  104 . The analysis framework  106  may then output a result of such interprocedural analysis (a result of the main query executed over the executable program  104 ). 
     As will be described in greater detail below, the scheduler component  120  can comprise or be in communication with the analysis component  112 , and responsive to receipt of the query, can perform an intraprocedural analysis on the main procedure in the executable program  104 . The analysis component  112  can explore paths in the main procedure (forward, backward, or some combination of both). The analysis component  112  can employ and overapproximate analysis, an underapproximate analysis, or some combination thereof. When the analysis component  112  encounters a call to a sub-procedure in the main procedure, it automatically formulates a sub-query for the sub-procedure, wherein results of the sub-query are needed to answer the original query (the main query). The analysis component  112  first accesses the procedure summaries  116  to determine if a summary resides therein that can be employed to answer the sub-query. If the analysis component  112  locates such a summary, the analysis component  112  outputs a result for the sub-query using such summary. Otherwise, the analysis component  112  assigns a Ready state to the sub-query, and adds it to a set of queries that will be returned. The analysis component  112  then continues to explore paths in the main procedure, repeating the same strategy to handle any procedure calls it encounters on such paths. The analysis component  112  completes processing of the main query when such component  112  cannot perform any further analysis on the main procedures without obtaining answers to sub-queries formulated by the analysis component  112 . 
     The analysis component  112  than returns all sub-queries it has generated (which are in the Ready state) as well as the main query, which is set to a Blocked state. The scheduler component  120  receives the list of sub-queries and schedules processing of such sub-queries over their respective sub-procedures across the computing nodes  108 - 110 . The analysis component  112  (instantiated separately on the different computing nodes  108 - 110 ) processes the respective sub-queries in parallel, and can generate additional queries to other procedures called in such sub-procedures. Eventually, parent queries are answered, and the process continues until the main query returns an answer (output). 
     With reference now to  FIG. 2 , an exemplary depiction  200  of the analysis component  112  is shown. The analysis component  112  is in communication with the data store  102 , which is shown to comprise the executable program  104  and the procedure summaries  116 . The analysis component  112  comprises an identifier component  202  that receives a procedure in the executable program  104  and identifies calls to other procedures (sub-procedures) in such procedure. As described above, the identifier component  202  can explore paths in the identified procedure forward, backwards, or some combination thereof. The analysis component  112  further comprises a query formulator component  204  that can, responsive to the encountering a call to a sub-procedure in the procedure, formulate a query that, when executed over the sub-procedure, returns an output utilized to process the received query over the parent procedure. The query formulator component  204  can use any suitable technique in connection with formulating sub-queries. 
     The analysis component  112  further comprises a summary analyzer component  206  that, responsive to the query formulator component  204  formulating a sub-query, accesses the data store  102  to ascertain whether the sub-query can be answered utilizing a procedure summary in the procedure summaries  116 . If such a procedure summary exists in the data store  102 , the analysis component  112  can answer the sub-query utilizing the located summary and can continue processing the received query over the procedure. Otherwise, the analysis component  112  can add the sub-query generated by the query formulator component  204  to a list of sub-queries that are to be returned. 
     The analysis component  112  may also comprise a summary generator component  208  that, for example, can generate a summary for the procedure if the procedure is a leaf node in the call graph or if the summary can be computed based upon summaries that are retrievable from the data store  102 . If the summary generator component  208  generates a summary for the procedure, such summary can be added to the procedure summaries  116  in the data store  102 . 
     The analysis component  112  further comprises a return component  210  that returns the received query and sub-queries that need to be process to answer the received query to the scheduler component  120 . If the analysis component  112  is able to answer the received query over the procedure (using one or more summaries from the data store  102  and/or a summary generated by the summary generator component  208 ), such result can be returned to the scheduler component  120 . As discussed above, once the analysis framework  106  receives sufficient answers to sub-queries, the main query can be answered. 
     Now referring to  FIG. 3 , an exemplary computer program  300  that may be subject to parallelized top-down interprocedural analysis is shown. The program  300  comprises a main procedure main, and the procedure main invokes three other procedures: bar, foo, and baz (which only have their signatures shown). In this example, it is desirable to ascertain whether some input to main exists that violates the assertion “assert(y&gt;0)” at the end of main. Such check can be encoded as the following query over the procedure main: 
       Q main = true   main  y≦0   (1)
 
     This query is configured to ascertain whether there is an execution through the procedure main starting in any input state (denoted by the precondition true) and ending in a state satisfying the error condition y≦0. 
     With reference now to  FIG. 4 , an exemplary state diagram  400  illustrating possible states of a query Q i  is shown. The query Q i  is placed in a Ready state  402  when it is ready to be processed (e.g., when it is ready to be executed over a procedure P i  by the analysis component  112 ). As described above, the analysis component  112  formulates a query Q j  that is to be executed over a procedure P j  called by the procedure P i . If the analysis component  112  is unable to provide an output to the query Q i  (due to lack of a summary S P     j    of procedure P j  called by P i ), then the query Q i  is transitioned to a Blocked state  404 , and the query Q j  is added to a list of queries to be returned to the scheduler component  120 . The returned queries are then placed in the Ready state  402 . Alternatively, if the analysis component  112  has sufficient information pertaining to all sub-procedures called by procedure P i  to generate a summary S P     i    for procedure P i , then the analysis component  112  outputs an answer to the query Q i  (e.g., returns the answer to the scheduler component  120 ), stores the summary S P     i    in the procedure summaries  116 , and transitions Q i  to a Done state  406 . 
     With reference now to  FIG. 5 , an exemplary depiction  500  of a parallelized top-down interprocedural analysis of the program  300  is illustrated. The depiction  500  shows alternating between MAP and REDUCE stages for query formulating and processing. The analysis framework  106  can operate, in this example, by first applying the analysis component  112  to Q main    502  over the procedure main. The query Q main    502  is initialized in the Ready state  402  (e.g., ready to be processed). Processing of Q main    502  by the analysis component  112  results in new queries Q foo    504 , Q bar    506 , and Q baz    508 . Such initial processing of the query Q main    502  occurs in a first MAP stage  509 . The queries Q foo    504 , Q bar    506 , and Q baz    508  can be referred to as children of Q main    502 , and are all in the Ready state  402 . Examples of such queries are as follows: 
         Q   foo = true   foo  ret≦−5   (2)
 
         Q   bar = true   bar  ret≦−5   (3)
 
         Q   baz   =     p   baz ≦−10   baz  ret≦−5   (4)
 
     In this example, the intraprocedural analysis undertaken by the analysis component  112  over main using Q main    502  results in the ascertainment that the assertion “assert(y&gt;0)” in main holds if and only if each of the procedures foo, bar, and baz return a value greater than −5. It can be noted that Q baz    508  has the precondition to p baz ≦−10, since baz is only called with inputs less than or equal to −10. 
     Responsive to the queries Q foo    504 , Q bar    506 , and Q baz    508  being returned, query Q main    502  is placed in the Blocked state  404 , because results from execution of at least one of its child sub-queries is needed before the query Q main    502  can make progress over main. A first REDUCE stage  510  is then initiated, where the analysis component  112  analyzes if any interdependencies between the queries Q foo    504 , Q bar    506 , and Q baz    508  have been resolved. In this example, none are resolved, so each query remains in its respective state (the first reduce stage  510  is essentially a no-op). At this point, the scheduler component  120  can schedule execution of the queries, Q foo    504 , Q bar    506 , and Q baz    508  over respective procedures foo, bar, and baz across differing computing nodes. 
     In a second MAP stage  512 , the analysis component  112  is executed, in parallel, on different computing nodes, such that the analysis component  112  executes queries in the Ready state  402  over their respective procedures. Accordingly, in an example, the analysis component  112  on a first computing node can execute the query Q foo    504  over foo, the analysis component  112  on a second computing node can execute the query Q bar    506  over bar, and the analysis component  112  on a third computing node can execute the query Q baz    508  over baz. For sake of explanation, the queries Q foo    504  and Q bar    506  can be entirely processed during the second MAP stage  512  (perhaps due to foo and bar being leaf nodes in the call graph of the program  300 ), and accordingly such queries are transitioned to the Done state  406 . Results of queries transitioned to the Done state  406  can be retained as procedure summaries in the procedure summaries  116 . As will be understood by one skilled in the art, a procedure summary can be a must summary (representing an underapproximation of the procedure and containing a path to error states), or a not-may summary (representing an overapproximation of the procedure and excluding paths to error states). The procedure baz calls the procedure roo; when executing Q baz    508  over baz, the analysis component  112  can formulate a new query Q roo    514  that needs to be executed over roo before Q baz    508  can generate a result. During the MAP stage  512 , Q baz    508  is moved to the Blocked state  404 , and Q roo    514  is placed in the Ready state  402 . 
     During a second REDUCE stage  516 , since Q foo    504  and Q bar    506  have moved to the Done state  406 , Q main  is placed in the Ready state  402 , thereby enabling Q main  to be further processed by the analysis component  112  over main. Queries that have transitioned to the Done state  406  are also deleted (as well as all of their respective descendants); accordingly, in this example, the queries Q foo    504  and Q bar    506  are deleted during the second REDUCE stage  516 . 
     In subsequent stages (not shown in  FIG. 5 ), it is possible that Q main    502  can complete based upon answers received from the processing of Q foo    504  and Q bar    506 . If this occurred, then a subsequent reduce stage will garbage collect the remaining queries (Q baz    508  and Q roo ), since results of such queries are no longer required. In other words, it is possible that a parent query can be answered based upon results of a subset of its child queries. 
     Returning now to  FIG. 1 , a more detailed description of operation of the analysis framework  106  and the analysis component  112  is provided. The data store  102  comprises the executable program  104 , which will be referred to as program  . The program   is a set of procedures {P 0 , . . . , P n ), where P 0  is the main procedure (entry point) of  . A procedure P i  is a tuple (V i , N i , E i , n i   0 , η i   x , λ i ), where:
         V i  is the disjoint union of the set of local variables V i   L  of P i  and the set of global variables V G  of  .   N i  is the set of control nodes (locations).   E i : N i ×N i  is the set of edges between control nodes.   β i   0 , n i   x  ∈ N i  are the entry and exit locations, respectively.   λ i : E i →Stmt is a labeling function, where Stmt is the set of program statements over V i . Statements in Stmt can be either simple statements or call statements, wherein a simple statement in a procedure P i  is an assignment statement x=E or an assume statement assume(Q), where x is a variable in V i , E is an expression over the variables V i , and Q is a Boolean expression over the variables V i . A call statement to the procedure P j  is of the form call P j .       

     It can be assumed, without loss of generality, that communication between procedures is performed via the global variables V G , and for each procedure P i , there need not exist a node n ∈ N i  such that (n i   x , n) ∈ E i . 
     An exemplary program model will now be described. A configuration of a procedure P i  is a pair (n, σ), where n ∈ N i , and the state σ is a valuation of variables V i  of P i . The set of all states P i  is denoted by Σ P     i   . Every edge e ∈ E i  is a relation Γ e    ⊂  Σ P     i   ×Σ P     i    defined by the standard semantics of the statement λ i (e). 
     The initial configurations of a procedure P i  are {(n i   0 , σ)|σ ∈ Σ P     i   }. From a configuration (n, σ), P i  can execute a statement by traversing some edge e=(n, n′) ∈ E i  and reaching a configuration (n′, σ′), where (σ, σ′ ∈ Γ e ). A configuration of (n, σ) can reach another configuration (n′, σ′), where n, n′ ∈ N i , if and only if there exists a sequence of edges in (n, n 1 ), (n, n 2 ), . . . , (n m , n′) ∈ E i , which, if executed from state σ leads to state σ′. 
     Procedure summaries that can be generated by the analysis component  112  and retained in the procedure summaries  116  are now described. For any procedure P i , φ 1  and φ 2  can be formulae representing sets of states in 2 Σ     Pi   . Then, there can exist two types of summaries for P i : must summaries and not-may summaries, defined respectively as follows:
     Must Summary:  φ 1   P i φ 2    is a must summary for P i  if and only if every exit configuration (n i   x , σ′), where σ′ ∈ φ 2 , is reachable from some initial configuration (n i   0 , σ), where σ ∈ φ 1 .   Not-may Summary:  φ 1   P j φ 2    is a not-may summary for P i  if and only if every initial configuration (n i   0 , σ), where σ ∈ φ 1 , cannot reach any exit configuration (n i   x , σ′), where σ′ ∈ φ 2 .   

     Queries that can be executed over procedures are now described. A query Q i  over some procedure P j  is defined as a 4-tuple (q i , s i , p i ,    i ), where
         q i  is a reachability question of the form  φ 1   P j φ 2   , asking if a procedure P j  starting in a configuration in {(n j   0 , σ)|σ ∈ φ 1 } can reach a configuration in {(n j   x , σ)|σ ∈ φ 2 }.   s i  ∈ {Ready, Blocked, Done} is the query state.   p i  is the index of the parent query Q P     i    of Q i .       i  is a verification object that maintains the internal state of a query. The exact nature of such an object depends on a kind of analysis being performed by the analysis framework  106  (may-analysis, must-analysis, may-must-analysis).       

     A procedure summary S can be used to answer a reachability question
       φ 1   P j φ 2    in either of the following ways: 1) Answer=“yes”, if   S= {circumflex over (φ)} 1   P j {circumflex over (φ)} 2   , where {circumflex over (φ)} 1    ⊂  φ 1  and φ 2  ∩ {circumflex over (φ)} 2 ≠0; 2) Answer=“no”, if   S= {circumflex over (φ)} 1   P j {circumflex over (φ)} 2   , where φ 1    ⊂  {circumflex over (φ)} 1  and φ 2    ⊂ {circumflex over (φ)} 2 .   

     Intuitively, a must-summary S answers a reachability question  φ 1   P j φ 2    with a “yes, there is an execution from a state in φ 1  to a state in φ 2  through P j .” On the other hand, if S is a not-may summary, then it answers the reachability question with a “no, there are no executions through P j  from any state in φ 1  to any state in φ 2 .” 
     A verification question for a program   is a query Q 0 =(q 0 , s 0 , p 0 ,    0 ) over its main procedure P 0 , where q 0 = φ 1   P 0 φ 2   , φ 2  describes undesirable (error) states, and p 0  is undefined, since the initial query Q 0  does not have any parent queries. 
     The analysis component  112  will now be described in greater detail. The analysis component  112  comprises an intraprocedural analysis algorithm for manipulating queries, and such algorithm parameterizes the analysis framework  106 . The analysis component receives a query Q i  in the Ready state, and the goal is to either compute a summary that answers the reachability question of Q i  or produce new queries that are to utilized to answer Q i . The analysis component  112 , as discussed above, can store procedure summaries that it computes in the data store  114 . The analysis component  112  can also query the data store  114  for procedure summaries in order to avoid recomputing answers to queries. An exemplary formal specification of the analysis component  112  is set forth below: 
     Input: Q i =(q i , s i , p i ,    i ) 
     Output: Set of queries R. 
     Precondition: s i =Ready. 
     Postcondition: R={Q′ i  ∪ C), where Q′ i =(q i , s′ i , p i ,  ′) and:
         1. (s′ i =Done) (C=0); and   2. (s′ i  ∈ {Blocked, Ready)) ∀(q j , s j , p j ,    j ) ∈ C·p j =i s j =Ready.       

     The analysis component  112  receives a query Q i =(q i , s i , p i ,    i ) as input and returns a set of queries R. If the analysis component  112  successfully analyzes Q i , it returns a copy Q′ i  of Q i  in a Done state (formula 1 of the above postcondition), and adds a summary that answers q i  to the procedural summaries  116 . Otherwise, the analysis component  112  returns a copy Q′ i  of Q i  that is either in the Ready state or the Blocked state as well as a set of child sub-queries C of Q′ i  (formula 2 of the above postcondition). Each child sub-query Q j =(q j , s j , p j ,    j ) ∈ C is uniquely identified by its index j. If a query Q i  is in a Blocked state, the analysis component  112  can make no progress with Q i  and can only continue when one of its children returns a result (e.g., the child query is transitioned to a Done state and a corresponding summary is added to the procedural summaries  116 ). If Q i  is in the Ready state, the analysis component  112  can perform more processing on Q i . 
     The analysis framework  106  interacts with the analysis component  112  as follows: first, the analysis component  112  attempts to return an answer to a query Q i  on some procedure P j  by analyzing P j  using summaries of the procedures called by P j  that are stored in the procedure summaries  116 . If the analysis component  112  is unable to locate appropriate summaries for such procedures, it transitions Q i  to the Blocked state and produces a number of new sub-queries C. The query Q i  remains in the Blocked state until one of its sub-queries has transitioned to the Done state (and, therefore, has a summary in the procedural summaries  116 ). The scheduler component  120  can schedule execution of the new sub-queries C across the multiple computing nodes  108 - 110 , such that the query Q i  is processed in parallel. 
     For purposes of explanation, and without loss of granularity, an exemplary instantiation of the analysis framework  106  is set forth below. Other instantiations that facilitate parallelizing interprocecural top-down analysis are also contemplated and are intended to fall under the scope of the hereto-appended claims. 
     
       
         
           
               
             
               
                   
               
             
            
               
                 1: function FRAMEWORK(Program    , Query Q 0  = (q 0 , s 0 , p 0 , O 0 )) 
               
            
           
           
               
               
            
               
                 2: 
                 QSet = {Q 0 } 
               
               
                 3: 
                 while    ∃(q i , s i , p i , O i ) ε QSet · s i  = Done    q i  = q 0  do 
               
               
                   
                  MAP: 
               
               
                 4. 
                    QSet′ ←     {ANALYSIS(Q i )|Q i  ε QSet    s i  = Ready} 
               
               
                 5. 
                    QSet ← QSet′ ∪ {Q i |Q i  ε QSet    s i  ≠ Ready} 
               
               
                   
                  REDUCE: 
               
               
                 6. 
                    for all Q i  = (q i , s i , p i , O i ) ε QSet do 
               
               
                 7. 
                     if s i  = Done then 
               
               
                 8. 
                       if s P     i    = Blocked then set s P     i    to Ready 
               
               
                 9. 
                       (*remove subtree rooted at Q i  from QSet*) 
               
               
                 10. 
                       QSet ← QSet\Descendants(Q i ) 
               
               
                 11. 
                  if there exists a must summary for q 0  in Procedural Summaries, 
               
               
                   
                  then 
               
               
                 12. 
                    return “Error Reachable” 
               
               
                 13. 
                  else 
               
               
                 14. 
                    return “Program is Safe” 
               
               
                   
               
            
           
         
       
     
     The analysis framework  106  receives as input the executable program  104  (a program  ) and a verification question Q 0  over the main procedure P 0  of  . The algorithm set forth above begins with a set of queries QSet that is initialized to the verification question (line 2). Each iteration (lines 3-10) is divided into 2 stages:
         1) The MAP stage (lines 4-5): Applies the analysis component  112 , in parallel, to each query Q i  ∈ QSet that is in the Ready state. Application of the analysis component  112  is shown in the algorithm as “ANALYSIS”. QSet′ is then assigned the union of all of the results returned by all calls to the analysis component  112 . This is denoted by parallel union symbol  . The only resource shared by parallel instances of the analysis component  112  is the database that comprises the procedure summaries.   2) The REDUCE stage (lines 6-10): Removes redundant and Done queries from QSet. The function Descendants(Q i ) is used to denote the image of the transitive closure of the parent-child relation starting from Q i . For every Q i  s.t.s i =Done, all descendants of Q i  are garbage collected.       

     The above algorithm iterates, executing the MAP and REDUCE stages until q 0  is answered. For a query Q i , when s i =Done, the procedure summaries  116  either contain a must summary or a not-may summary that answers q i . Therefore, when the analysis framework  106  exits the loop at line 3, it can be ascertained that there exists a summary that answers the reachability question q 0 . If q 0  is answered by a must summary, then the analysis framework  106  outputs “Error Reachable”, as there is an execution to the error states defined in q 0 . Alternatively, if q 0  is answered by a not-may summary, then the analysis framework  106  returns “Program is Safe”, since the not-may summary precludes any execution to an error state in q 0 . 
     For purposes of explanation, an example corresponding to  FIGS. 3 and 5  is set forth herein. In the second MAP stage  512 , the analysis component  112  is applied to queries in the Ready state in QSet: Q foo    504 , Q bar    506 , and Q baz    508 . That is, in the second MAP stage  512 , QSet is assigned as follows: 
         Q Set′←ANALYSIS( Q   foo )∪ ANALYSIS( Q   bar )∪ ANALYSIS( Q   baz )={ Q′   foo   } ∪ {Q′   bar   } ∪ {Q   roo   , Q   baz }, and
 
       QSet←QSet′ ∪ Q main  
 
     It can be noted that ANALYSIS(Q foo ), ANALYSIS(Q bar ), and ANALYSIS(Q baz ) are computed in parallel. Subsequently, in the second REDUCE stage  516 , Q′ foo  and Q′ bar  are in the Done state and, therefore, Q main  is set to the Ready state and Q′ foo  and Q′ bar  are removed from QSet. 
     Description of how a must-analysis, may-analysis, and may-must-analysis can be suitably modified in connection with the above-described analysis component  112  is now set forth. In an example, the analysis component  112  can be given a query Q m =(q m , s m , p m ,    m ), where q m = φ 1   P i φ 2    and s m  =Ready. A must-map and a may-map over procedure P i  can be defined as follows:
     Must-map: a must-map Ω: N i →2 Σ     Pi    maps locations n ∈ N i  of P i  to sets of states, representing an underapproximation of the set of reachable states at that location from states in φ 1  at n i   0 . For each node n ∈ N i , Ω n  can be used to denote Ω(n). Initially, Ω n     i       o   =φ 1 , and for all   

     
       
         
           
             
               n 
               ∈ 
               
                 
                   N 
                   i 
                 
                 
                   { 
                   
                     n 
                     i 
                     0 
                   
                   } 
                 
               
             
             , 
             
               
                 Ω 
                 n 
               
               = 
               0. 
             
           
         
       
         
         May-map: A may-map Π: N i →2 2     ΣPi    maps locations n ∈ N i  of P i  to sets of states (partitions), which together represent an overapproximation of the set of states that can reach φ 2  at that location. For each node n ∈ N i , Π n  can be used to denote Π(n). Initially, Π n     i       x   ={φ 2 , Σ P     i   \φ 2 ), and for every n ∈ N i \{n i   x }, Π n ={Σ P     i   }. 
       
    
     For a node n ∈ N i , sets of states Ω n  and φ n  ∈ Π n  are treated as formulas, and the notations Ω n   G  and φ n   G  are utilized to denote, respectively, versions of Ω n  and φ n  where all local variables are existentially quantified. Below, how different analyses populate such maps to answer the reachability question q m  is described. 
     With respect to a must-analysis, such analysis explores a subset of the behaviors, or an underapproximation, of a given program, and is therefore useful for proving the presence of errors. In a must-analysis, the analysis component  112  can progressively propagate sets of reachable states along edges of the procedure P i . If at any point Ω n     i       x   ∩φ 2 ≠0, then the postcondition φ 2  of q m  is reachable from a state in φ 1 , and, therefore, a must-summary that answers q m  can be generated and stored in the procedure summaries  116 . The verification object    m  for a must-analysis is the must-map Ω. 
     A difference from a typical must-analysis is the way in which the analysis component  112  can propagate reachable states over call statements. Given an edge e=(n, n′) ∈ E i  such that λ i (e) is a call statement call P j , the analysis component  112  an encode reachability over this call as the reachability question  Ω n   G   P j Σ P     j     , and can first check whether a must-summary that answers this question is available in the procedure summaries  116 . If such a summary exists in the procedure summaries  116 , the analysis component  112  uses the summary to update the set of reachable states Ω n′  at n′, the destination location of the call-edge e. Alternatively, if a must-summary is unavailable, the analysis component  112  can create a child query Q k , where q k = Ω n   G   P j Σ P     j     , and adds it to R (the set of sub-queries that the analysis component  112  returns to the analysis framework  106 ), which includes an updated copy of Q m . In contrast, a regular must-analysis would analyze the procedure P j  and compute reachability information. 
     If the analysis component  112  successfully computes all reachable states, then the analysis component  112  terminates analysis of Q m . Since a must-analysis is not guaranteed to converge, however, the analysis component  112  can continue to analyze Q m  up to some time limit or an upper-bound on the number of explored paths before it stops analysis and returns a set of child sub-queries R of Q m . This is to ensure that the MAP stage always terminates. When the analysis component  112  ceases its analysis of Q m , the state of the analysis component, which is the must-map Ω, is saved in    m , so that the next time Q m  is processed by the analysis component  112 , it can continue exploration from the saved state    m . 
     With respect to a may-analysis, such an analysis explores an overapproximation of behaviors of a program, and is therefore used to prove absence of errors. An exemplary goal of a may-analysis is to prove that no execution can reach a state in φ 2  at n i   x  from a state φ 1  at n i   0 . For every edge e=(n, n′) ∈ E i , it can be assumed that there exists an abstract edge between every ψ n  ∈ Π n  and every ψ n′  ∈ Π n′  (denoted by ψ n → e ψ n′ ). The may-analysis proceeds by eliminating infeasible abstract edges in order to prove that φ 2  is unreachable. Eliminated abstract edges are stored in the set Ē, which is initially empty. 
     In an example, for edge e=(n, n′), λ i (e) is a simple statement, and that there exists an abstract edge ψ 1 → e ψ 2 . A may-analysis checks if ψ 1  can reach a state in ψ 2  by taking an edge e. In case it cannot, ψ 1  is split into two partitions: ψ 1   θ and ψ 1     θ, where pre(λ i (e),ψ 2 )  ⊂  θ and pre(λ i (e),ψ 2 ) is the preimage of the set of states ψ 2  with respect to the statement λ i (e). Since no state in ψ 1     θ an reach ψ 2 , Ē is updated with the edge (ψ 1     θ,ψ 2 ). Intuitively, the partition ψ 1  is refined into a partition that may reach ψ 2 , and another one may not. 
     If it is now assumed that λ i (e) is a call statement to some procedure P j , then the analysis component  112  encodes the reachability question  ψ 1   G   P j ψ 2   G   . If there exists a not-may summary  {circumflex over (ψ)}{circumflex over (ψ 1 )} P i {circumflex over (ψ)}{circumflex over (ψ 2 )}  that answers this reachability question, then it can be ascertained that there are no executions from ψ 1  to ψ 2 . Accordingly, the analysis component  112  splits ψ 1  into ψ 1   θ and ψ 1     θ, where θ  ⊂  {circumflex over (φ)}{circumflex over (φ 1 )}, and adds (ψ 1     ν,ψ 2 ) to the set Ē. Otherwise, if there does not exist such a summary, the analysis component  112  can add a child query Q k , where q k = ψ 1   G   P j ψ 2   , to the set R. 
     As discussed, a may-analysis maintains the map Π and the set of eliminated edges Ē. Therefore, when the analysis component  112  returns Q m  in a Ready or Blocked state,    m  is set to (Π, Ē). A may-analysis sets the query Q m  to Done when all partitions of n i   0  intersecting with φ 1  cannot reach a partition of n i   x  intersecting with φ 2 , where reachability is defined via abstract edges. As with a must-analysis, for fairness, the analysis component  112  can terminate analysis prematurely and store the state of the analysis in    m . 
     With respect to a may-must-analysis, such an analysis combines a must-analysis with a may-analysis in order to efficiently find errors as well as prove their absence. In an exemplary embodiment, the analysis component  112  can employ testing, symbolic execution and abstraction to check properties of programs using a may-must analysis. Further, the analysis component  112  can employ interpolation-based model checking algorithms in connection with performing a may-must analysis, where symbolic executions to error locations can be undertaken to locate bugs and, in case of infeasible executions, use interpolants derived from refutation proofs to create an abstraction that eliminates a large number of potential counterexamples. 
     For a query Q m , a may-must analysis maintains Π, Ω, and Ē. Thus, if the analysis component  112  returns Q m  in a Ready or Blocked state, it sets    m  to (Π, Ω, Ē). 
     A may-must analysis only analyzes an abstract transition ψ 1 → e  ψ 2 , where e=(n, n′) ∈ E i  and λ i (e) is a call to some procedure P j , if Ω n ∩ψ 1 ≠0 and Ω n′ ∩ψ 2 ≠0. That is, only abstract transitions which have been reached by the must analysis, but not taken, are analyzed. Such transitions are known to those skilled in the art as “frontiers”. 
     A may-must-analysis, as instantiated in the analysis component  112 , handles such transitions as follows:
         1. If there exists a must summary  {circumflex over (ψ)}{circumflex over (ψ 1 )} P 1 {circumflex over (ψ)}{circumflex over (ψ 2 )}  that answers the query  Ω n   G   P j ψ 2   G   , then it can be ascertained that there exists an execution from Ω n  to ψ 2  through P j , and, therefore, the analysis component  112  updates Ω n′  to be Ω n′  ∪ θ, where θ  ⊂  {circumflex over (ψ)}{circumflex over (ψ 2 )} and θ ∩ ψ 2 ≠0.   2. If there exists a not-may summary  {circumflex over (ψ)}{circumflex over (ψ 1 )} P i {circumflex over (ψ)}{circumflex over (ψ 2 )}  that answers the query  Ω n   G   P j ψ 2   G   , then it can be ascertained that there are no executions from Ω n  to ψ 2 , and, therefore, the analysis component  112  splits region ψ 1  into ψ 1     θ and ψ 1   θ, where θ  ⊂  {circumflex over (φ)}{circumflex over (φ 1 )} and  θ ∩ Ω n =0. Thus, the edge (ψ 1   θ,ψ 2 ) is added to Ē.   3. If neither kind of summaries exist, then a child query Q k , where q k = (Ω n   ψ 1 ) G   P i ψ 2   G   , is added to R.       

     When undertaking a may-must analysis, the analysis component  112  continues processing a query Q m  until a must summary is produced, a not-may summary is produced, or all abstract edges have been analyzed and child queries must be answered to continue processing. Similar to may- and must-analyses, the analysis component  112  can terminate analysis prematurely. 
     In summary, the analysis component  112  can be instantiated with various classes of analyses, which encompass a large number of existing algorithms. 
     With reference now to  FIG. 6 , an exemplary methodology is illustrated and described. While the methodology is described as being a series of acts that are performed in a sequence, it is to be understood that the methodology is not limited by the order of the sequence. For instance, some acts may occur in a different order than what is described herein. In addition, an act may occur concurrently with another act. Furthermore, in some instances, not all acts may be required to implement a methodology described herein. 
     Moreover, the acts described herein may be computer-executable instructions that can be implemented by one or more processors and/or stored on a computer-readable medium or media. The computer-executable instructions may include a routine, a sub-routine, programs, a thread of execution, and/or the like. Still further, results of acts of the methodologies may be stored in a computer-readable medium, displayed on a display device, and/or the like. The computer-readable medium may be any suitable computer-readable storage device, such as memory, hard drive, CD, DVD, flash drive, or the like. As used herein, the term “computer-readable medium” is not intended to encompass a propagating signal. 
       FIG. 6  illustrates an exemplary methodology  600  that facilitates paralyzing top-down interprocedural analysis of a computer program. The methodology  600  starts at  602 , and at  604  a first query that is to be executed over a computer program is received. The computer program comprises a main procedure that calls a plurality of sub-procedures. 
     At  606 , at least one path from amongst a plurality of possible paths in the main procedure is explored (forwards, backwards or some combination thereof) until a call to one of the sub-procedures is encountered. At  608 , a sub-query that is to be executed over the sub-procedure is formulated based upon the first query. Such formulation is undertaken responsive to the call to the sub-procedure being encountered in the main procedure. 
     At  610 , a determination is made regarding whether there are additional calls in the main procedure. If there are additional calls to sub-procedures in the main procedure, the methodology  600  returns to act  606 , where the main procedure is further explored. If no additional calls reside in the main procedure, then at  612  the plurality of sub-queries are distributed for execution over respective sub-procedures across multiple computing nodes. At  614  results from the multiple computing nodes for the plurality of sub-queries are received, wherein the computing nodes generate such results by way of executing the plurality of sub-queries over the respective plurality of sub-procedures. It is to be noted that the computing nodes compute the results to the sub-queries in parallel. At  616 , an output for the first query is generated based at least in part upon the results received from the multiple computing nodes. The methodology  600  completes at  618 . 
     Now referring to  FIG. 7 , a high-level illustration of an exemplary computing device  700  that can be used in accordance with the systems and methodologies disclosed herein is illustrated. For instance, the computing device  700  may be used in a system that supports parellizing top-down interprocdural analysis. In another example, at least a portion of the computing device  700  may be used in a system that supports intraprocedural analysis. The computing device  700  includes at least one processor  702  that executes instructions that are stored in a memory  704 . The memory  704  may be or include RAM, ROM, EEPROM, Flash memory, or other suitable memory. The instructions may be, for instance, instructions for implementing functionality described as being carried out by one or more components discussed above or instructions for implementing one or more of the methods described above. The processor  702  may access the memory  704  by way of a system bus  706 . In addition to storing executable instructions, the memory  704  may also store procedure summaries, queries, etc. 
     The computing device  700  additionally includes a data store  708  that is accessible by the processor  702  by way of the system bus  706 . The data store may be or include any suitable computer-readable storage, including a hard disk, memory, etc. The data store  708  may include executable instructions, procedure summaries, etc. The computing device  700  also includes an input interface  710  that allows external devices to communicate with the computing device  700 . For instance, the input interface  710  may be used to receive instructions from an external computer device, from a user, etc. The computing device  700  also includes an output interface  712  that interfaces the computing device  700  with one or more external devices. For example, the computing device  700  may display text, images, etc. by way of the output interface  712 . 
     Additionally, while illustrated as a single system, it is to be understood that the computing device  700  may be a distributed system. Thus, for instance, several devices may be in communication by way of a network connection and may collectively perform tasks described as being performed by the computing device  700 . 
     It is noted that several examples have been provided for purposes of explanation. These examples are not to be construed as limiting the hereto-appended claims. Additionally, it may be recognized that the examples provided herein may be permutated while still falling under the scope of the claims.