Contracts and futures in an asynchronous programming language
AssigneeMicrosoft Corporation
InventorsJames R. Larus, Sriram K. Rajamani, Jakob Rehof
Life of this patent
Estimating the term…
Abstract
An asynchronous programming language that facilitates concurrent programming by utilizing futures, asynchronous calls, and joins on futures. For each of a client interface and a service interface of an asynchronous interface, respective models are automatically extracted. A behavioral contract is defined on the asynchronous interface. The client and service models are then passed to modular checking algorithm that checks to ensure that both the client and the service conform to the behavioral contract. The checking algorithm combines region-based type systems with model checking techniques to handle pointer aliasing in a sound manner.
Claims63
A system that facilitates asynchronous programming, comprising:
- a contract component that facilitates stating a behavioral contract on an asynchronous service interface between a client interface and a service interface;
- and
- a conformance checking component that checks that at least one of the client interface and the service interface conform to the contract defined therebetween.
A system that facilitates asynchronous programming, comprising:
- a client interface and a service interface;
- an extraction component that automatically extracts a client model from the client interface and a service model from the service interface;
- a relator component that creates a behavioral relationship between the client model and the service model;
- and
- a conformance checking component that checks that the client interface obeys the behavioral relationship, and the service interface properly implements the behavioral relationship.
A method of asynchronous programming, comprising:
- receiving a client interface and a service interface;
- creating a behavioral relationship between the client interface and the service interface;
- and
- checking to ensure that the client interface obeys the behavioral relationship and the service interface properly implements the behavioral relationship.
A method of asynchronous programming, comprising:
- receiving a client interface and a service interface;
- automatically extracting a client model from the client interface and a service model from the service interface;
- creating a behavioral relationship between the client model and the service model;
- and
- enforcing the behavioral relationship between the client interface and the service interface.
A computer software product that embodies program instructions for execution by a processing unit, the processing unit retrieving the instructions from a computer-readable memory to facilitate concurrent execution of the instructions, the product comprising:
- a contract component that creates a contract state between a client state and a service state;
- an extraction component that automatically extracts a client model from the client state, a service model from the service state, and an interface model from the contract state;
- and
- a conformance checking component that checks that the client model obeys the interface model, and the service model properly implements the contract model.
A system of asynchronous programming, comprising:
- means for receiving a client interface and a service interface;
- means for automatically extracting a client model from the client interface and a service model from the service interface;
- means for creating a behavioral relationship between the client model and the service model;
- and
- means for checking to ensure that the client interface obeys the behavioral relationship and the service interface properly implements the behavioral relationship.
Dependencies are inferred from the claim text.