Programming model to detect deadlocks in concurrent programs
First Claim
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 Assignments
0 Petitions
Accused Products
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.
-
Citations
37 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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16)
-
-
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. - View Dependent Claims (18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29)
-
-
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. - View Dependent Claims (31)
-
-
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. - View Dependent Claims (33, 34, 35, 36, 37)
-
Specification