# Refactoring for Java-Structured Concurrency
## 5 Consistency Check  
The consistency check is used to check the consistency of the program before and after refactoring. _FlexSync_[26] is a tool that can perform refactoring and conversion among different synchronization mechanisms by applying different markers. It defines a set of consistency check rules to verify the correctness of concurrent programs before and after refactoring. Similarly to _FlexSync_, we design the consistency check rules for _ReStruct_. Before presenting these rules, we will first make the relevant definitions.  
Definition 4: (Task dependency). The dependency relationship for \(t_{i}\)\((1<=i<=n)\) in \(m_{i}\) is defined as the set \(D=\{d_{1},d_{2},\ldots,d_{k}\}\). For \(\forall d_{j}\in D(1<=j<=k)\), we have \(d_{j}\subset t_{i}\), indicating that the execution of task \(j\) may depend on multiple tasks.  
**Definition 5**.: _(Resources). For each os in \(m_{i}\), the definitions of the various variables, objects, and other resources contained in the set are represented as \(R=\{r_{1},r_{2},...,r_{z}\}\)._  
**Definition 6**.: _(Resource access). For each \(m_{i}\in M(1<=i<=n)\), the subsequent read and write operations contained after the statements (gs) are denoted as \(\{op_{i1},op_{i2},...,op_{iq}\}\). In \(m_{i}\), if there exists an operation (\(op_{ij}\)) \(\in m_{i}(1<=j<=q)\) that accesses a certain resource (\(r\)), it is represented as \(op_{ij}\).access\((r)\)._  
**Definition 7**.: _(Task cancellation mechanism). For \(\forall m_{i}\), when tasks fail, the set of tasks that are canceled at this time is defined as the set \(c_{i}\). Among them, \(c_{i}\subset t_{i}\) indicates that when these tasks fail, there will be multiple tasks to be canceled. However, the number of tasks canceled must be less than the total number of tasks minus one in \(m_{i}\)._  
Based on the definitions provided above, the following consistency check rules for refactoring are presented:  
**Rule 1:** Before refactoring, \(\forall t_{i}\in T(1<=i<=n)\), with \(t_{i}=\{t_{11},t_{2},\ldots,t_{ik}\}\), it follows that \(t_{before}=k\). After refactoring, for the same \(t_{i}\), it remains that \(t_{after}=k\).  
This rule indicates that the number of tasks will not change after refactoring, thus ensuring the integrity of the tasks.  
**Rule 2:** Before refactoring, for \(t_{i}\) (\(1<=i<=n\)) in \(m_{i}\), for all \(d_{j}\in D(1<=j<=k)\), we have \(d_{j}=\emptyset\). After refactoring, in this \(t_{i}\), for \(\forall d_{j}\in D\), we still have \(d_{j}=\emptyset\).  
This rule indicates that if there is no dependency relationship among the tasks before refactoring then there will still be no dependency relationship among the tasks after refactoring.  
**Rule 3:** Before refactoring \(\forall t_{i}\in T\) (\(1<=i<=n\)), it is the case that \(c_{i}=\emptyset\) (\(1<=i<=q\)). After refactoring, for the same \(t_{i}\), we have \(c_{i}=\{c_{i1},c_{i2},\ldots,c_{ir}\}\) (\(0<=r<=k-1\)), where \(r\) is the number of tasks that have not yet been completed at that time.  
Rule 3 ensures that the code that cancels specific tasks will not be refactored to structured concurrency. The reason is that the _shutdownOnFailure_ strategy does not allow the selective cancellation of individual tasks. In essence, this rule safeguards the integrity of the task cancellation mechanism during the refactoring process.  
**Rule 4:** Before refactoring, for \(\forall m_{i}\), \(\exists r_{t}\in R\) (\(1<=t<=z\)), \(\exists op_{ij}\in t_{i}\) (\(1<=j<=q\)), such that \(op_{ij}\).access\((r_{t})\). After refactoring, for \(m_{i}\), \(op_{ij}\) still contains \(op_{ij}\).access\((r_{t})\).  
Rule 4 ensures that before refactoring, the resources in \(\infty\) are accessible by a specific read/write operation (\(op\)) and remain accessible by the same operation after refactoring.