Programming model to detect deadlocks in concurrent programs

• US 7,703,077 B2
• Filed: 04/30/2002
• Issued: 04/20/2010
• Est. Priority Date: 04/30/2002
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Rajamani, Sriram K., Larus, James R., Rehof, Jakob
• Primary Examiner(s): Zhen; Wei Y
• Assistant Examiner(s): Chen; Qing
• Application Number:
  US10/136,596
• Publication Number:
  US 20030204641A1
• Time in Patent Office: 2,912 Days
• Field of Search: 717104-105, 717124-135, 719313-317, 714/37, 714/38
• US Class Current: 717/127
• CPC Class Codes: G06F 9/546 Message passing systems or structures, e.g. queues

Abstract

Described are embodiments for developing a message-passing application program. The program is constructed using stages having a plurality of asynchronous functions, or operations. The operations communicate with other operations of other message-passing programs in a distributed computing environment. The operations also communicate with other operations on other stages of the message-passing application. In order to reduce deadlock errors, a behavioral type signature is appended to the declaration of each operation of the message-passing application program. The behavioral type signature specifies behavioral properties for each operation, such as when an operation should send a message to another operation. A type checker utilizes typing rules and the behavioral type signature to extract an implementation model of each function. The type checker then compares the implementation model to the behavioral type signature to determine whether the asynchronous function conforms to the behavioral type signature.

Claims

1. A method for developing a message-passing application program having a first program module with a plurality of asynchronous functions that communicate with operations of a second program module, the method comprising:

defining a behavioral type signature for one of the plurality of asynchronous functions, the behavioral type signature specifying message-passing properties for the one of the plurality of asynchronous functions, and the behavioral type signature dictating timing of input and output actions by the one of the plurality of asynchronous functions, and wherein the defining a behavioral type signature comprises determining whether a condition is to be placed in the behavioral type signature;

analyzing the one of the plurality of asynchronous functions against the behavioral type signature to render an evaluation on whether message-passing actions of the one of the plurality of asynchronous functions during execution of the message-passing application program will conform to the message-passing properties specified by the behavioral type signature, wherein the analyzing comprises;

extracting an implementation model of the one of the plurality of asynchronous functions, wherein the implementation model reflects the message-passing actions of the one of the plurality of asynchronous functions during compilation of the message-passing application program; and

checking the implementation model against the behavioral type signature by comparing actions of the implementation model to actions specified in the behavioral type signature to determine whether message-passing related errors are contained in executable code of the one of the plurality of asynchronous functions, wherein the checking comprises;

receiving the behavioral type signature specifying the message-passing properties for the one of the plurality of asynchronous functions, receiving the extracted implementation model, and assuming the behavioral type signature does not have parallel composition;

generating a report indicating whether any message-passing related errors exist, wherein the report includes the evaluation for the one of the plurality of asynchronous functions; and

storing the evaluation in memory.

2. The method as defined in claim 1, further comprising:

marking the one of the plurality of asynchronous functions as conforming to the behavioral type signature if the message-passing actions of the one of the plurality of asynchronous conform to the message-passing properties specified by the behavioral type signature; and

marking the one of the plurality of asynchronous functions as failing to conform to the behavioral type signature if the message-passing actions of the one of the plurality of asynchronous functions do not conform to the message-passing properties specified by the behavioral type signature.

3. The method as defined in claim 2, further comprising:

repeating the defining operation, the analyzing operation and one of the marking operations for each of the plurality of asynchronous functions on the first program module.

4. The method as defined in claim 1, wherein the report includes an indication as to whether the one of the plurality of asynchronous functions is marked as conforming to or failing to conform to the associated behavioral type signature.

5. The method as defined in claim 4, further comprising:

providing the report to a program developer developing the message-passing application program such that the program developer may complete development of the message-passing application program while taking into account the evaluation.

6. The method as defined in claim 1, wherein the checking operation comprises:

determining whether the behavioral type signature specifies an internal choice for performing an action or an external choice for performing an action.

7. The method as defined in claim 6, wherein the checking operation further comprises:

determining whether the implementation model performs at least one output action specified by the behavioral type signature if it is determined that the behavioral type signature specifies an internal choice; and

marking the evaluation to reflect that the one of the plurality of asynchronous functions fails to conform to the behavioral type signature if it is determined that the implementation model does not perform at least one output action specified by the behavioral type signature.

8. The method as defined in claim 7, wherein the checking operation further comprises:

determining whether all actions of the implementation model are actions allowed by the behavioral type signature; and

marking the evaluation to reflect that the one of the plurality of asynchronous functions conforms to the behavioral type signature if it is determined that the implementation model performs at least one output action specified by the behavioral type signature and that all actions of the implementation model are allowed by the behavioral type signature.

9. The method as defined in claim 6, wherein the checking operation further comprises:

determining whether the implementation model performs all input actions specified by the behavioral type signature if it is determined that the behavioral type signature specifies an external choice; and

marking the evaluation to reflect that the one of the plurality of asynchronous functions fails to conform to the behavioral type signature if it is determined that the implementation model does not perform all input actions specified by the behavioral type signature.

10. The method as defined in claim 9, wherein the checking operation further comprises:

determining whether all actions of the implementation model are actions allowed by the behavioral type signature; and

marking the evaluation to reflect that the one of the plurality of asynchronous functions conforms to the behavioral type signature if it is determined that the implementation model performs all input actions specified by the behavioral type signature and that all actions of the implementation model are allowed by the behavioral type signature.

11. The method as defined in claim 1, wherein the analyzing operation is performed as the message-passing application program is being compiled.

12. The method as defined in claim 1, wherein each of the plurality of asynchronous functions is written as executable source code in a first programming language and the behavioral type signature is written in a second programming language.

13. The method as defined in claim 1, wherein the message-passing application program operates in a local computing environment as an event-driven application program wherein messages are passed between the first program module and the second program module within the local computing environment.

14. The method as defined in claim 13, wherein the first program module is a first stage of the message-passing application program containing a first collection of two or more of the plurality of asynchronous functions and the second program module is a second stage of the message-passing application program containing a second collection of two or more of the plurality of asynchronous functions.

15. The method as defined in claim 1, wherein the message-passing application program operates in .a distributed computing environment.

16. The method as defined in claim 15, wherein the first program module is a stage of the message-passing application program containing a collection of two or more of the plurality of asynchronous functions and the second program module is a stage of a second message-passing application program within the distributed computing environment.

17. A computer storage medium readable by a computing system and encoding a computer program of instructions for executing a computer process for controlling operations of the computing system and for developing a message-passing application program having a first program module with a plurality of asynchronous functions that communicate with operations of a second program module, the computer process comprising:

defining a behavioral type signature for one of the plurality of asynchronous functions, the behavioral type signature specifying message-passing properties for the one of the plurality of asynchronous functions, and the behavioral type signature dictating timing of input and output actions by the one of the plurality of asynchronous functions, and wherein the defining a behavioral type signature comprises determining whether a condition is to be placed in the behavioral type signature;

analyzing the one of the plurality of asynchronous functions against the behavioral type signature to render an evaluation on whether message-passing actions of the one of the plurality of asynchronous functions during execution of the message-passing application program will conform to the message-passing properties specified by the behavioral type signature, wherein the analyzing comprises;

extracting an implementation model of the one of the plurality of asynchronous functions, the implementation model reflecting message-passing actions of the one of the plurality of asynchronous functions during compilation of the message-passing application program; and

checking the implementation model against the behavioral type signature by comparing actions of the implementation model to actions specified in the behavioral type signature to determine whether message-passing related errors are contained in executable code of the one of the plurality of asynchronous functions, wherein the checking comprises;

receiving the behavioral type signature specifying the message-passing properties for the one of the plurality of asynchronous functions, receiving the extracted implementation model, and assuming the behavioral type signature does not have parallel composition;

generating a report indicating whether any message-passing related errors exist; and

storing in memory an indication of whether the one of the plurality of asynchronous functions conforms to the behavioral type signature.

18. The computer process in the computer storage medium of claim 17, wherein the checking operation comprises:

comparing the message-passing actions of the implementation model against the message-passing properties of the one of the plurality of asynchronous functions.

19. The computer process in the computer storage medium of claim 18, wherein the computer process further comprises:

rendering an evaluation on whether the one of the plurality of asynchronous functions conforms to the behavioral type signature.

20. The computer process in the computer storage medium of claim 19, wherein the rendering operation comprises:

marking the one of the plurality of asynchronous functions as conforming to the behavioral type signature if the message-passing actions of the one of the plurality of asynchronous functions conform to the message-passing properties specified by the associated behavioral type signature; and

marking the one of the plurality of asynchronous functions as failing to conform to the behavioral type signature if the message-passing actions of the one of the plurality of asynchronous functions do not conform to the message-passing properties specified by an associated behavioral type signature.

21. The computer process in the computer storage medium of claim 20, wherein the computer process further comprises:

repeating the defining operation, the extracting operation, the checking operation and one of the two marking operations for each of the plurality of asynchronous functions on the first program module.

22. The computer process in the computer storage medium of claim 19, wherein the checking operation comprises:

determining whether the behavioral type signature specifies an internal choice for performing an action or an external choice for performing an action.

23. The computer process in the computer storage medium of claim 20, wherein the checking operation further comprises:

determining whether the implementation model performs at least one output action specified by the behavioral type signature if it is determined that the behavioral type signature specifies an internal choice; and

marking the evaluation to reflect that the one of the plurality of the asynchronous functions fails to conform to the behavioral type signature if it is determined that the implementation model does not perform at least one output action specified by the behavioral type signature.

24. The computer process in the computer storage medium of claim 23, wherein the checking operation further comprises:

determining whether all actions of the implementation model are actions allowed by the behavioral type signature; and

marking the evaluation to reflect that the one of the plurality of asynchronous functions conforms to the behavioral type signature if it is determined that the implementation model performs at least one output action specified by the behavioral type signature and that all actions of the implementation model are allowed by the behavioral type signature.

25. The computer process in the computer storage medium of claim 22, wherein the checking operation further comprises:

determining whether the implementation model performs all input actions specified by the behavioral type signature if it is determined that the behavioral type signature specifies an external choice; and

marking the evaluation to reflect that the one of the plurality of asynchronous functions fails to conform to the behavioral type signature if it is determined that the implementation model does not perform all input actions specified by the behavioral type signature.

26. The computer process in the computer storage medium of claim 25, wherein the checking operation further comprises:

determining whether all actions of the implementation model are actions allowed by the behavioral type signature; and

marking the evaluation to reflect that the one of the plurality of asynchronous functions conforms to the behavioral type signature if it is determined that the implementation model performs all input actions specified by the behavioral type signature and that all actions of the implementation model are allowed by the behavioral type signature.

27. The computer process in the computer storage medium of claim 17, wherein the message-passing application program operates in a local computing environment as an event-driven application program wherein messages are passed between the first program module and the second program module within the local computing environment.

28. The computer process in the computer storage medium of claim 17, wherein the message-passing application program operates in a distributed computing environment.

29. The computer process in the computer storage medium of claim 28, wherein the first program module is a stage of the message-passing application program containing a collection of two or more of the plurality of asynchronous functions and the second program module is a stage of a second message-passing application program within the distributed computing environment.

30. A method for evaluating behavioral properties of a message-passing application program having a first program module with an asynchronous function that communicates with operations of a second program module, the method comprising:

defining a behavioral type signature for the asynchronous function, the behavioral type signature specifying message-passing properties for the asynchronous function and the behavioral type signature dictating timing of input and output actions by the asynchronous function, and wherein the defining a behavioral type signature comprises determining whether a condition is to be placed in the behavioral type signature;

extracting an implementation model of the asynchronous function, the implementation model reflecting message-passing actions of the asynchronous function during compilation of the message-passing application program;

checking the implementation model against the behavioral type signature by comparing actions of the implementation model to actions specified in the behavioral type signature to determine whether message-passing related errors are contained in executable code of the asynchronous function, wherein the checking comprises;

receiving the behavioral type signature specifying the message-passing properties for the asynchronous function, receiving the extracted implementation model, and assuming the behavioral type signature does not have parallel composition;

rendering an evaluation on whether the asynchronous function conforms to the behavioral type signature based on whether the executable code of the asynchronous function contains message-passing related errors;

generating a report indicating whether any message-passing related errors exist, wherein the report includes the evaluation on whether the asynchronous function conforms to the behavioral type signature; and

storing the evaluation in memory.

31. The method as defined in claim 30, wherein the rendering operation comprises:

marking the asynchronous function as conforming to the behavioral type signature if conformance exists between the message-passing actions of the implementation model and the message-passing properties specified by the associated behavioral type signature; and

marking the asynchronous function as failing to conform to the behavioral type signature if conformance does not exist between the message-passing actions of the implementation model and the message-passing properties specified by the associated behavioral type signature.

32. A system for evaluating behavioral properties of a message-passing application program having a first program module with an asynchronous function that communicates with operations of a second program module, the system comprising:

a memory storing;

a define module;

a type checker; and

computer executable instructions that when executed perform the steps of;

defining, with the define module, a behavioral type signature for the asynchronous function, the behavioral type signature specifying message-passing properties for the asynchronous function, and the behavioral type signature dictating timing of input and output actions by the asynchronous function, and wherein the defining a behavioral type signature comprises determining whether a condition is to be placed in the behavioral type signature;

analyzing the asynchronous function against the behavioral type signature to render an evaluation on whether message-passing actions of the asynchronous function during execution of the message-passing application program will conform to the message-passing properties specified by the behavioral type signature, wherein the analyzing comprises;

extracting, with the type checker, an implementation model of the asynchronous function reflecting message-passing actions of the asynchronous function during compilation of the message-passing application program and checking the message-passing actions of the implementation model against the message-passing properties of the behavioral type signature to determine whether message-passing related errors are contained in executable code of the asynchronous function, wherein the checking comprises;

receiving the behavioral type signature specifying the message-passing properties for the asynchronous function, receiving the extracted implementation model, and assuming the behavioral type signature does not have parallel composition; and

generating a report indicating whether any message-passing related errors exist, wherein the report includes the evaluation for the asynchronous function; and

a processor for executing the computer executable instructions.

33. The system as defined in claim 32, wherein the asynchronous function is written as executable source code in a first programming language and the behavioral type signature is written in a second programming language.

34. The system as defined in claim 32, wherein the message-passing application program operates in a local computing environment as an event-driven application program, wherein messages are passed between the first program module and the second program module within the local computing environment.

35. The system as defined in claim 34, wherein the first program module is a first stage of the message-passing application program containing a first collection of two or more of a plurality of asynchronous functions and the second program module is a second stage of the message-passing application program containing a second collection of two or more of a plurality of asynchronous functions.

36. The system as defined in claim 32, wherein the message-passing application program operates in a distributed computing environment.

37. The system as defined in claim 36, wherein the first program module is a stage of the message-passing application program containing the asynchronous function and the second program module is a stage of a second message-passing application program within the distributed computing environment.