Programming model for concurrent programs

• US 20030204641A1
• Filed: 04/30/2002
• Published: 10/30/2003
• 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
• Granted Patent: US 7,703,077 B2
• Time in Patent Office: Days
• US Class Current: 719/313
• CPC Class Codes: G06F 9/546 Message passing systems or structures, e.g. queues

Abstract

A system and method for developing a message-passing application program is disclosed. The message-passing application 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 that occur as a result of the asynchronous nature of these communications, 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 and, conversely, when an operation should wait for a message from 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 asynchronous function; and

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.

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

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

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

3. A 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; and

creating a report depicting whether there exists a possibility that deadlock will occur while the first program module communicates with the second program module during execution of the message-passing application program, wherein deadlock is considered a possibility if one of the plurality of asynchronous functions fails to conform to an associated behavioral type signature.

4. A method as defined in claim 3, wherein the report includes the evaluation for each of the plurality of asynchronous functions and whether each of the plurality of asynchronous functions is marked as conforming to or failing to conform to the associated behavioral type signature.

5. A 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. A method as defined in claim 1, wherein the analyzing operation comprises:

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

checking the implementation model against the behavioral type signature to determine whether the asynchronous function conforms to the behavioral type signature.

7. A method as defined in claim 6, 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.

8. A method as defined in claim 7, 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 asynchronous function 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.

9. A method as defined in claim 8, 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 asynchronous function 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.

10. A method as defined in claim 7, 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 asynchronous function 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.

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

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

14. A 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.

15. A method as defined in claim 14, 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.

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

17. A method as defined in claim 16, 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.

18. A method as defined in claim 1, wherein the analyzing operation further comprises:

determining whether the behavioral type signature specifies that the asynchronous function perform a first action and a second action in a substantially simultaneous manner;

extracting a first implementation model of the asynchronous function, the first implementation model reflecting performance of the first action by the asynchronous function;

extracting a second implementation model of the asynchronous function, the first implementation model reflecting performance of the second action by the asynchronous function; and

checking the first implementation model and the second implemenation model against the behavioral type signature to determine whether the asynchronous function conforms to the behavioral type signature.

19. A method as defined in claim 18, wherein the checking operation further comprises:

marking the evaluation to reflect that the asynchronous function fails to conform to the behavioral type signature if it is determined that conformance does not exist between the first implementation model and the behavioral type signature and between the second implementation model and the behavioral type signature.

11. A method as defined in claim 11, 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 asynchronous function 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.

20. A computer program product 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 asynchronous function;

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; and

checking the implementation model against the behavioral type signature to determine whether the asynchronous function conforms to the behavioral type signature.

21. The computer process in the computer program product of claim 20, wherein the checking operation comprises:

comparing the message-passing actions of the implementation model against the message-passing properties of the asynchronous function.

22. The computer process in the computer program product of claim 21, wherein the computer process further comprises:

rendering an evaluation on whether the asynchronous function conforms to the behavioral type signature.

23. The computer process in the computer program product of claim 22, wherein the rendering operation comprises:

marking the asynchronous function as conforming to the behavioral type signature if the message-passing actions of the asynchronous function conform to 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 the message-passing actions of the asynchronous function do not conform to the message-passing properties specified by an associated behavioral type signature.

24. The computer process in the computer program product of claim 23, 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; and

creating a report depicting whether there exists a possibility that deadlock will occur while the first program module communicates with the second program module during execution of the message-passing application program, wherein deadlock is considered a possibility if one of the plurality of asynchronous functions fails to conform to the associated behavioral type signature.

25. The computer process in the computer program product of claim 22, 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.

26. The computer process in the computer program product of claim 23, 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 asynchronous function 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.

27. The computer process in the computer program product of claim 26, 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 asynchronous function 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.

28. The computer process in the computer program product of claim 25, 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 asynchronous function 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.

29. The computer process in the computer program product of claim 28, 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 asynchronous function 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.

30. The computer process in the computer program product of claim 20, 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.

31. The computer process in the computer program product of claim 20, wherein the message-passing application program operates in a distributed computing environment.

32. The computer process in the computer program product of claim 31, 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.

33. A method for evaluating behavioral properties of a message-passing application program having a first program module with a 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;

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 to determine whether conformance exists between the implementation model and the behavioral type signature; and

rendering an evaluation on whether the asynchronous function conforms to the behavioral type signature based on whether conformance exists between the implementation model and the behavioral type signature.

34. A method as defined in claim 33, 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 does not conformance exist between the message-passing actions of the implementation model and the message-passing properties specified by the associated behavioral type signature.

35. A method as defined in claim 34, further comprising:

creating a report depicting whether there exists a possibility that deadlock will occur while the first program module communicates with the second program module during execution of the message-passing application program, wherein deadlock is considered a possibility if one the asynchronous functions fails to conform to the behavioral type signature.

36. 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 method comprising:

a define module defining a behavioral type signature for the asynchronous function, the behavioral type signature specifying message-passing properties for the asynchronous function; and

a type checker extracting 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 the asynchronous function conforms to the behavioral type signature.

37. A system as defined in claim 36, 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.

38. A system as defined in claim 36, 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.

39. A system as defined in claim 38, 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.

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

41. A system as defined in claim 40, 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.