Correct refactoring of concurrent software
Automated refactorings as implemented in modern IDEs for Java usually make no special provisions for concurrent code. Thus, refactored programs may exhibit unexpected new concurrent behaviors. We analyze the types of such behavioral changes caused by current refactoring engines and develop techniques to make them behavior-preserving, ranging from simple techniques to deal with concurrency-related language constructs to a framework that computes and tracks synchronization dependencies. By basing our development directly on the Java Memory Model we can state and prove precise correctness results about refactoring concurrent programs. We show that a broad range of refactorings are not influenced by concurrency at all, whereas other important refactorings can be made behavior-preserving for correctly synchronized programs by using our framework. Experience with a prototype implementation shows that our techniques are easy to implement and require only minimal changes to existing refactoring engines.
1. A computer-implemented method for behavior-preserving transformation of a concurrent program, the method comprising:
receiving source code with a proposed refactoring operation to be performed;
transforming the source code by applying the proposed refactoring operation to create a transformed source code;
creating an intermediate representation of the source code including synchronization dependence edges between two specific elements of the source code;
creating an intermediate representation of the transformed source code including synchronization dependence edges;
comparing the intermediate representation for the source code and the intermediate representation for the transformed source code, and determining that synchronization dependence edges are equivalent to ensure concurrent behavior-preservation; and
in response to the synchronization dependence edges and synchronization dependences being equivalent, saving the transformed source code.
2. The method of claim 1 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation includes that checking synchronization dependence edges that were present in the intermediate representation for the source code are preserved in the transformed source code.
3. The method of claim 1 , wherein the source code includes synchronized blocks.
4. The method of claim 1 , wherein the comparing the synchronization dependence edges are equivalent to ensure behavior-preservation further comprises identifying in the source code at least one of:
an acquire dependence from statement A to statement B in some method M, meaning that A corresponds to an acquire action and B executes after A in at least one execution of M;
a release dependence from statement A to statement B in some method M, meaning that statement B corresponds to a release action and B executes after A in at least one execution of M; and
a thread management dependence from statement A to statement B in some method M, meaning that statement B corresponds to a thread management action and B executes after A in at least one execution of M.
5. The method of claim 1 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises ensuring that:
a normal access never loses acquire dependencies,
a normal access never loses release dependencies, and
a node corresponding to a synchronization action never gains any one of acquire dependence and release dependence.
6. The method of claim 4 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises ensuring that:
a normal access never loses acquire dependencies,
a normal access never loses release dependencies,
a node corresponding to a synchronization action never gains any one of acquire dependence and release dependence; and
a node corresponding to an action never gains and/or loses a thread management dependence.
7. The method of claim 4 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises ensuring that:
a normal access never loses acquire dependencies,
a normal access never loses release dependencies, and
a node corresponding to a synchronization action never gains any one of acquire dependence and release dependence.
8. The method of claim 1 , wherein the comparing the synchronization dependence edges are further defined by
computing an initial control flow graph (CFG) of the source code; and
wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises
computing synchronization dependencies on the initial CFG;
performing a refactoring as when applied to a sequential program to form an updated CFG; and
re-computing synchronization dependencies on the updated CFG.
9. The method of claim 4 , wherein the comparing the synchronization dependence edges are further defined by
computing an initial control flow graph (CFG) of the source code; and
wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises
computing synchronization dependencies on the initial CFG;
performing a refactoring as when applied to a sequential program to form an updated CFG; and
re-computing synchronization dependencies on the updated CFG.
10. The method of claim 5 wherein the comparing the synchronization dependence edges are further defined by
computing an initial control flow graph (CFG) of the source code; and
wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises
computing synchronization dependencies on the initial CFG;
performing a refactoring as when applied to a sequential program to form an updated CFG; and
re-computing synchronization dependencies on the updated CFG.
11. The method of claim 1 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation ensures that a Java Memory Model permits a similar execution of the source code and the transformed source code.
12. The method of claim 1 , further comprising:
wherein in response to any of the synchronization dependence edges and synchronization dependences being not being equivalent an error message is produced.
13. A computer program product for behavior-preserving transformation of a concurrent program, the computer program product comprising:
a non-transitory computer readable storage medium having computer readable program code embodied therewith, the computer readable program code comprising:
computer readable program code configured to perform:
receiving source code with a proposed refactoring operation to be performed;
transforming the source code by applying the proposed refactoring operation to create a transformed source code between two specific elements of the source code;
creating an intermediate representation of the source code including synchronization dependence edges;
creating an intermediate representation of the transformed source code including synchronization dependence edges;
comparing the intermediate representation for the source code and the intermediate representation for the transformed source code, and determining that synchronization dependence edges are equivalent to ensure concurrent behavior-preservation; and
in response to the synchronization dependence edges and synchronization dependences being equivalent, saving the transformed source code.
14. The computer program product of claim 13 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation includes that checking synchronization dependence edges that were present in the intermediate representation for the source code are preserved in the transformed source.
15. The computer program product of claim 13 , wherein the source code includes synchronized blocks.
16. The computer program product of claim 13 , wherein the comparing the synchronization dependence edges are equivalent to ensure behavior-preservation further comprises identifying in the source code at least one of:
an acquire dependence from statement A to statement B in some method M, meaning that A corresponds to an acquire action and B executes after A in at least one execution of M;
a release dependence from statement A to statement B in some method M, meaning that statement B corresponds to a release action and B executes after A in at least one execution of M; and
a thread management dependence from statement A to statement B in some method M, meaning that statement B corresponds to a thread management action and B executes after A in at least one execution of M.
17. The computer program product of claim 13 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises ensuring that:
a normal access never loses acquire dependencies,
a normal access never loses release dependencies, and
a node corresponding to a synchronization action never gains any one of acquire dependence and release dependence.
18. The computer program product of claim 16 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises ensuring that:
a normal access never loses acquire dependencies,
a normal access never loses release dependencies,
a node corresponding to a synchronization action never gains any one of acquire dependence and release dependence; and
a node corresponding to an action never gains and/or loses a thread management dependence.
19. The computer program product of claim 16 , wherein the comparing that synchronization dependence edges are equivalent to ensure behavior-preservation further comprises ensuring that:
a normal access never loses acquire dependencies,
a normal access never loses release dependencies, and
a node corresponding to a synchronization action never gains any one of acquire dependence and release dependence.
20. An information processing system for behavior-preserving transformation of a concurrent program managing variable operand length instructions, the information processing system comprising:
a processor communicatively coupled with a memory, to perform a method comprising:
receiving source code with a proposed refactoring operation to be performed;
transforming the source code by applying the proposed refactoring operation to create a transformed source code between two specific elements of the source code;
creating an intermediate representation of the source code including synchronization dependence edges;
creating an intermediate representation of the transformed source code including synchronization dependence edges;
comparing the intermediate representation for the source code and the intermediate representation for the transformed source code, and determining that synchronization dependence edges are equivalent to ensure concurrent behavior-preservation; and
in response to the synchronization dependence edges and synchronization dependences being equivalent, saving the transformed source code.