Constraint verification for distributed applications

• US 9,448,820 B1
• Filed: 01/03/2013
• Issued: 09/20/2016
• Est. Priority Date: 01/03/2013
• Status: Active Grant

• Current Assignee: Amazon Technologies, Inc. (Amazon.com, Inc.)
• Original Assignee: Amazon Technologies, Inc. (Amazon.com, Inc.)
• Inventors: Allen, Nicholas Alexander
• Primary Examiner(s): Puente, Emerson
• Assistant Examiner(s): Labud, Jonathan R
• Application Number:
  US13/733,780
• Time in Patent Office: 1,356 Days
• Field of Search: None
• US Class Current: 1/1
• CPC Class Codes: G06F 11/3082 the data filtering being achieved by aggregating or compressing the monitored data
• CPC Class Codes: G06F 11/3612 by runtime analysis performance monitoring G06F11/3466
• CPC Class Codes: G06F 2009/45591 Monitoring or debugging support
• CPC Class Codes: G06F 9/455 Emulation; Interpretation; Software simulation, e.g. virtualisation or emulation of application or operating system execution engines
• CPC Class Codes: G06F 9/45558 Hypervisor-specific management and integration aspects
• CPC Class Codes: G06F 9/4843 by program, e.g. task dispatcher, supervisor, operating system
• CPC Class Codes: G06F 9/5066 Algorithms for mapping a plurality of inter-dependent sub-tasks onto a plurality of physical CPUs mappping at compile time, see G06F8/451

Abstract

Systems and methods are described for analyzing and verifying distributed applications. In one embodiment, an application program is executed as independently executable components. During execution, redundant portions of application program data are aggregated. A property of the application program is verified using the aggregated application program data to represent code execution paths.

Claims

1. A computing system comprising one or more computing nodes and one or more data stores in communication with the one or more computing nodes, the one or more data stores having stored thereon:

a constraint data store storing thereon one or more constraints indicative of predetermined application program conditions; and

computer instructions that, upon execution by the one or more computing nodes, at least cause the computing system to;

receive an application program for execution in a distributed computing environment;

divide the application program into a plurality of components that are executable as independent processes in accordance with the one or more constraints;

instantiate a plurality of virtual machines and execute the plurality of independently executable components in the plurality of virtual machines;

generate condition variables based on execution of the components;

in response to a determination that application program data is to be communicated between at least two of the components;

generate data path information for the application program data;

aggregate application program data from multiple communication events and combine respective condition variable and data path information;

generate a single data packet that encapsulates the aggregated application program data along with associated condition variables and the data path information; and

send the single data packet to a destination virtual machine for the data packet; and

verify a runtime property of the application program by using the aggregated application program data to represent code execution paths of the application program.

2. The computing system according to claim 1, further comprising computer instructions that, upon execution by the at least one computing node, at least cause the system to analyze the application program until a multivariate condition is reached and create the condition variable at a branch point.

3. The computing system according to claim 1, wherein at least some of the independently executable components are executed in at least a portion of the plurality of virtual machines in parallel.

4. The computing system according to claim 1, wherein the constraints include invariant conditions at identified program locations.

5. The computing system according to claim 1, wherein the aggregated application program data includes logical expressions representing program variables.

6. A computer-implemented method for verifying a property of a distributed application program, the method comprising:

dividing an application program operable to execute in a distributed computing environment into a plurality of executable components that can be executed as separate and distinct processes in a computing device;

executing the components in a plurality of constraint verification modules comprising at least one application module executing in a virtual environment;

collapsing application data communicated between the constraint verification modules by aggregating multiple input messages into a lesser number of input messages and responding to the aggregated input messages, wherein the collapsed application data includes associated condition variable and data path information; and

verifying a runtime property of the application program by using the collapsed application data.

7. The method of claim 6 wherein the application program is divided based on one or more constraints indicative of predetermined application program conditions.

8. The method of claim 6 wherein said collapsing comprises aggregating similar application data into a single data packet and combining respective condition variables and data path information.

9. The method of claim 6, wherein said application module comprises source code, binary executables, scripts, or data operable to exercise one of the executable components.

10. The method of claim 6 wherein the constraint verification modules are configured to perform symbolic analysis or logical analysis of application modules executing in the virtual environment.

11. The method of claim 6 further comprising:

maintaining an analysis state for the application program; and

analyzing the application program until a branch condition is reached and recording the branch condition in the analysis state.

12. The method of claim 11 wherein the branch condition is recorded by adding a condition variable to the analysis state at the branch condition.

13. The method of claim 6 wherein at least a portion of said verifying is performed in parallel.

14. The method of claim 6 wherein said runtime property comprises one or more of the following:

an absence of a specified fault condition, execution of an identified line of code, a security property, or a range of values for a variable.

15. One or more non-transitory computer-readable storage media having collectively stored thereon executable instructions that, when executed by one or more processors of a computer system, cause the computer system to:

analyze an application program operable to execute in a distributed computing environment;

divide the application program into a plurality of executable components in accordance with one or more rules;

independently execute the executable components in one or more constraint verification modules;

maintain state information for the application program during execution of the executable components; and

aggregate application data communicated between the constraint verification modules to reduce inter-module communications and use the aggregated application data to verify a property of the application program, wherein the aggregated application data includes associated condition variable and data path information.

16. The computer-readable storage media of claim 15 wherein the state information includes branch conditions.

17. The computer-readable storage media of claim 15 wherein the application data is aggregated by reducing logical expressions representing program variables and condition variables.

18. The computer-readable storage media of claim 15 wherein the application data is aggregated by aggregating multiple code paths.

19. A computing system comprising one or more computing nodes and one or more data stores in communication with the one or more computing nodes, the one or more data stores having stored thereon computer instructions that, upon execution by the one or more computing nodes, at least cause the computing system to:

divide an application program operable to execute in a distributed computing environment into a plurality of executable components that can be executed as separate and distinct processes in a computing device;

execute the components in a plurality of constraint verification modules comprising at least one application module executing in a virtual environment;

collapse application data communicated between the constraint verification modules by aggregating multiple input messages into a lesser number of input messages and responding to the aggregated input messages, wherein the collapsed application data includes associated condition variable and data path information; and

verify a runtime property of the application program by using the collapsed application data.