Identifying concurrency control from a sequential proof

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.

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.