# US 2010/0169618 A1 · Identifying concurrency control from a sequential proof > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 2010/0169618 A1 - Document ID: US20100169618A1 - Status: Published application - Kind: A1 - Application number: 12/345,857 - Filed: 2008-12-30 - Published: 2010-07-01 - Earliest claimed: 2008-12-30 - Assignees: Microsoft Corporation - Inventors: Ganesan Ramalingam; Sriram Rajamani; Venkatesh-Prasad Ranganath; Kapil Vaswani; Jyotirmoy Vinay Deshmukh - Web page: https://patentgrep.com/patent/US20100169618A1 ## CPC - G06F 8/456: {Parallelism detection} - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract The claimed subject matter provides a system and/or a method that facilitates ensuring non-interference between multiple threads that access a shared resource. An interface can receive a portion of sequential code, wherein the portion of sequential code includes a property that is maintained and relied upon when invoked and executed by a sequential client. A synthesizer component can leverage a sequential proof related to the portion of sequential code in order to derive a concurrency control mechanism for a portion of concurrency code that maintains the property when invoked by a concurrent client, wherein the sequential proof identifies a concurrent interference at an execution point that is tolerable for the concurrent client. ## Claims ### Claim 1 A system that facilitates ensuring non-interference between concurrent clients that share some resource, comprising: an interface that receives a portion of sequential code, the portion of sequential code includes a property that is maintained and relied upon when invoked and executed by a sequential client; the interface receives a proof that the portion of sequential code satisfies the property during a sequential execution; a synthesizer component that identifies, for two or more program points in the portion of sequential code, a set of predicates that are relevant at such program points; the synthesizer component determines a type of concurrency control, the type of concurrency control is a lock and is associated with each predicate within the set of predicates identified; the synthesizer component inserts instructions in the portion of sequential code to manage the concurrency control, the management is at least one of an acquiring of a lock or a releasing of a lock; and the synthesizer component ensures that the lock is held on a predicate at the two or more program points, the locks correspond to the predicates relevant at the two or more program points. ### Claim 2 (depends on 1) The system of claim 1, further comprising at least one of the following: the synthesizer component identifies a first instruction in the portion of sequential code whose execution invalidates a relevant predicate; the synthesizer component inserts before the first instruction a second instruction for acquiring the lock corresponding to the relevant predicate unless the lock corresponds to a predicate relevant at the respective program point before the first instruction; or the synthesizer component inserts after the first instruction a third instruction for releasing the lock corresponding to the relevant predicate unless the lock corresponds to a predicate relevant at the respective program point after the first instruction. ### Claim 3 (depends on 1) The system of claim 1, further comprising at least one of the following: a second portion of sequential code that access a portion of shared data related to the portion of sequential code; the synthesizer component identifies a first instruction in the second portion of sequential code whose execution invalidates a relevant predicate; the synthesizer component inserts before the first instruction a second instruction for acquiring the lock corresponding to the relevant predicate; or the synthesizer component inserts after the first instruction a third instruction for releasing the lock corresponding to the relevant predicate. ### Claim 4 (depends on 1) The system of claim 1, the synthesizer component analyzes the portion of sequential code and a specification of one or more desired properties in order to employ a verification technique to generate the proof that the portion of sequential code satisfies the specification in a sequential execution, the synthesizer component utilizes the portion of the code and the proof to insert instructions to provide concurrency control. ### Claim 5 (depends on 1) The system of claim 1, further comprising a protection component that identifies a type of concurrency control mechanism to employ specific to a target concurrent client. ### Claim 6 (depends on 5) The system of claim 5, the protection component employs the type of concurrency control mechanism on a region corresponding to the execution point of the property for the portion the sequential code to create the portion of concurrency control code that executes in the concurrent client without an interference with the shared resource. ### Claim 7 (depends on 6) The system of claim 6, the sequential proof corresponds to a thread, the protection component implements the concurrency control mechanism to the execution point in order to create the concurrent control code. ### Claim 8 (depends on 1) The system of claim 1, further comprising a debug component that utilizes the derived concurrency control mechanism to check for consistent incorporation of concurrency control mechanisms at an execution point within a second portion of concurrency control code. ### Claim 9 (depends on 8) The system of claim 8, the debug component generates a notification based upon an inconsistency in regards to the comparison between the derived concurrent control mechanism and a concurrent control mechanism implemented by the second portion of concurrency code. ### Claim 10 (depends on 8) The system of claim 8, the debug component generates a notification related to an identified inconsistency in regards to the comparison between the execution point identified by the synthesizer component and an execution point for the concurrent control mechanism related to the second point of concurrency code. ### Claim 11 (depends on 8) The system of claim 8, the debug component automatically incorporated the derived concurrency control mechanism over the concurrency control mechanism in light of a detected inconsistency. ### Claim 12 (depends on 1) The system of claim 1, further comprising a verification tool that automatically identifies or generates the sequential proof based upon an analysis of the portion of sequential proof. ### Claim 13 (depends on 12) The system of claim 12, the verification tool receives the sequential proof from an entity and automatically communicates the sequential proof to the interface. ### Claim 14 (depends on 13) The system of claim 13, the entity is at least one of a user, a machine, a server, a website, a link, a network, a data store, or an enterprise. ### Claim 15 (depends on 1) The system of claim 1, further comprising a data store that includes a plurality of the portion of sequential code. ### Claim 16 (depends on 15) The system of claim 15, the synthesizer component adapts the data store and the plurality of the portion of sequential code in order to be utilized in a concurrent environment without an interference with a shared resource. ### Claim 17 A computer-implemented method that facilitates automatically creating concurrency control code, comprising: receiving a sequential proof; analyzing the sequential proof; identifying an assertion that is satisfied at a point of sequential execution from the sequential proof; incorporating concurrency control at the point to create concurrent control code; and utilizing the concurrent control code including the concurrent control with a concurrent client. ### Claim 18 (depends on 17) The method of claim 17, further comprising: utilizing the sequential proof corresponding to the sequential code to derive a type of lock and a location for the sequential code; utilizing at least one of the type of lock or the location to verify a portion of concurrency control code; and generate a notification of an inconsistency based upon the verification. ### Claim 19 (depends on 17) The method of claim 17, the concurrency control is at least one of an atomic region, a lock, a semaphore, an optimistic technique, a pessimistic technique, or a two-phase locking. ### Claim 20 A computer-implemented system that facilitates ensuring non-interference between concurrent clients that share a resource, comprising: means for receiving a portion of sequential code, the portion of sequential code includes a property that is maintained and relied upon when invoked and executed by a sequential client; means for leveraging a sequential proof related to the portion of sequential code in order to derive concurrency control for a portion of concurrency control code that maintains the property when invoked by a concurrent client; means for utilizing the sequential proof to identify a concurrent interference at an execution point that is tolerable for the concurrent client; means for enforcing the concurrency control systematically and automatically derived from the sequential proof enabling the concurrent client to utilize the portion of concurrency control code without an interference involving a shared resource; and means for utilizing the derived concurrency control to debug a disparate portion of concurrency control code.