# Data Synchronization: A Complete Theoretical Solution for Filesystems
## 6 Synchronization by Conflict Resolution
### Theoretical Foundation
: The meanings of the symbols are as in Definition 7. Suppose by contradiction that both are in \(M\). As they are on comparable nodes, there is an \(\ll\)-chain in \(M\) between \(\sigma\) and \(\tau\). Consequently there are two consecutive commands in this chain so that one is in \(A\) and the other is in \(B\), say \(\sigma^{\prime}\ll\tau^{\prime}\), \(\sigma^{\prime}\in A\) and \(\tau^{\prime}\in B\). However, Proposition 8 says that in this case \(\sigma^{\prime}\in B\), contradicting that \(A\) and \(B\) are disjoint. **Proposition 14**. : _Suppose \((\sigma,\tau)\) is a conflict, \(\sigma^{\prime}\in A\) and \(\sigma\ll\sigma^{\prime}\). Then \((\sigma^{\prime},\tau)\) is also a conflict._  
Proof. : Let \(\sigma,\sigma^{\prime}\) be on nodes \(n\) and \(n^{\prime}\), respectively. If \(n^{\prime}\) is the parent of \(n\), then the node of \(\tau\) is comparable to \(n^{\prime}\), thus we are done. Therefore \(n\) is the parent of \(n^{\prime}\), \(\sigma\) and \(\sigma^{\prime}\) are constructors, and \(\sigma\) matches \(\langle n,\mathbb{OF},\mathbb{D}\rangle\). If the node of \(\tau\) is not below \(n\), then we are done. If it is, then the input type of \(\tau\) is \(\mathbb{O}\) (as in the original filesystem \(\Phi\), \(\Phi(n)\) is not a directory, therefore every node below it is empty). For the same reason the command set \(B\) must contain a command on node \(n\) (otherwise when executing \(\tau\), \(\Phi\) still has the original content at \(n\), and then \(\tau\) breaks \(\Phi\)). This command has the same input type as \(\sigma\), must create a directory, thus it is equal to \(\sigma\), contradicting that \(A\) and \(B\) are disjoint. By symmetry, the same claim holds when \(A\) and \(B\) are swapped. Fix \(\sigma\in A\), and split \(B\) into \(B_{\sigma}^{\mathsf{ok}}\) and \(B_{\sigma}^{\mathsf{conf}}\) as follows:  
\[B_{\sigma}^{\mathsf{ok}} =\{\tau\in B:\ (\sigma,\tau)\text{ is not a conflict}\}=\{\tau\in B: \sigma\,\|\,\tau\},\] \[B_{\sigma}^{\mathsf{conf}} =\{\tau\in B:\ (\sigma,\tau)\text{ is a conflict}\}=\{\tau\in B: \sigma\,\|\,\tau\}.\]  
We know \(B_{\sigma}^{\mathsf{ok}}\in B\) by Propositions 5 and 14, which means that if \(\Phi\) is a filesystem \(B\) does not break, then neither does \(B_{\sigma}^{\mathsf{ok}}\). Moreover, if \(\sigma\ll\sigma^{\prime}\), then \(B_{\sigma}^{\mathsf{conf}}\subseteq B_{\sigma^{\prime}}^{\mathsf{conf}}\). In particular, if \(B_{\sigma}^{\mathsf{conf}}\) is empty, then so is \(B_{\sigma}^{\mathsf{conf}}\). Next we show that if there are no conflicts, then the synchronization is done; however, we need a stronger statement which will be used to justify the correctness of the synchronization process. **Proposition 15**. : _Suppose \(B_{\sigma}^{\mathsf{conf}}\) is empty, that is, no \(\tau\in B\) is in conflict with \(\sigma\in A\). Then \(\sigma\in M\)._  
Proof. : It is enough to show that \(M\cup\{\sigma\}\) is canonical. Since \(\sigma\,\|\,B\), it has at most one command on every node. It can only be non-canonical if there is a \(\tau\in M\) on a related node that cannot be connected to \(\sigma\) using an \(\ll\)-chain from the commands in \(M\). This \(\tau\) must be in \(A\), which has a chain between \(\sigma\) and \(\tau\). If this chain goes in the direction \(\sigma\ll\cdots\ll\tau\), then \(\sigma\in M\) by Proposition 9. Otherwise we know \(\tau\ll\cdots\ll\sigma\), and based on the remark above, \(B_{\omega}^{\mathsf{conf}}\) is empty for all members of this chain and so are independent of \(B\). This means the chain can be added to \(M\), which is a contradiction. **Corollary 1** (Termination). : _If there are no conflicts, then the merger \(M\) is \(A\cup B\)._  
Figure 5: (**a**) The conflict graph of the synchronization problem of Figure 3. The conflict \((\sigma_{2},\tau_{7})\) is resolved with the winner \(\tau_{7}\). (**b**) The conflict graph after resolving \((\sigma_{2},\tau_{7})\); commands \(\sigma_{1}\) and \(\sigma_{2}\) are deleted. The next conflict we resolve is \((\sigma_{A},\tau_{5})\).