# Deadlocks Detection in Multithreaded Applications Based on Source Code Analysis
## 5 Deadlock
### DL0 Application Model  
According to the model in Section 3, the source code of DL0 application is as follows:  
\[ \begin{array}{l}\text{T}_{DL0}=(\text{t}_{0},\text{t}_{1},\text{t}_{2}),\\ \text{U}_{DL0}=(\{\text{t}_{0}\},\{\text{t}_{1},\text{t}_{2}\},\{\text{t}_{0}\}), \\ \text{R}_{DL0}=\{\{\text{counter}\}\}\,\\ \text{O}_{DL0}=\{\{\text{0}_{0,1},\text{0}_{2},\text{0}_{0,3},\text{0}_{0,4}, \text{0}_{1,1},\text{0}_{1,2},\\ \text{o}_{1,3},\text{o}_{1,4},\text{o}_{1,5},\text{o}_{1,6},\text{o}_{2,1}, \text{o}_{2,2},\text{o}_{2,3},\text{o}_{2,4},\\ \text{o}_{2,5},\text{o}_{2,6}\}\,\\ \text{Q}_{DL0}=\{\text{(m,\,PMD),\,\text{(n,\,PMD)}\},\\ \text{F}_{DL0}=\{\{\text{(o}_{0,1},\,\text{o}_{0,2}),\,\text{(r}_{1},\,\text{o}_{ 0,2}),\\ \end{array} \]  
The phenomenon of deadlock in the DL0 application is caused by the work of a pair of threads using a pair of locks to exclude each other. In large multithreaded applications, this happens very often because in order to achieve maximum performance, while maintaining the correctness of the application code, one shared resource usually has one lock. According to the above, there is a very high probability that there will be threads working with a group of shared resources, and thus also with a group of locks. As a result, in all of these threads, the order of establishing lock groups must be identical because a different order leads to the deadlock phenomenon. It is possible, however, that the programmer, through the use of C language structures or intentionally through the use of specialised tools, will obfuscate the code, and the resource conflict causing this phenomenon will be hidden from him. The resource conflict in the case of the S1 scenario is a different order of establishing lock pairs in two threads. Code obfuscation should be understood as the lack of using standard rules for writing the application code, e.g., MISRA C, Netrino, or GNU coding standard. A graph of the DL0 application source code operation is shown in Figure 3. This representation locates the resource conflict that causes deadlock. This conflict in the graph manifests itself by the crossing of the edges leading from the lock to the operation in thread \(t_{2}\), while the edges leading from the locks to the operation in \(t_{1}\) thread do not cross. The crossing of the edges is the effect of a different order of locking. Based on the scenario presented in the form of the DL0 application source code and operation graph, it can be concluded that:  
**Definition 1**. : _Let \(\lambda^{P,i}\), \(i\) be the set of all paths that can be created from \(t_{i}\) thread operation beginning with operation \(o_{i,j}\). Formally, the \(i\)th path of \(\lambda^{P,i}\), \(i\) set is defined as the sequence:_  
\[\lambda^{P,i}_{a}=(\lambda^{P,i}_{a,1},\lambda^{P,i}_{a,2},..., \lambda^{P,i}_{a,q}),\text{ where }\lambda^{P,i}_{a,1}=o_{i,1},\lambda^{P,i}_{a,1}\in O _{P},\] \[(\lambda^{P,i}_{a,k^{\prime}},\lambda^{P,i}_{a,k+1})\in E_{P}, \lambda^{P,i}_{a,k}\
eq\lambda^{P,i}_{a,l}\text{ for }k\
eq l,\,l,k=1...q\]  
**Definition 2**. : _Let in \(\lambda^{P,i}_{l}\) path be two such operations \(o_{i,a}\) and \(o_{i,b}\) where locks \(q_{c}\) and \(q_{d}\) (that is, in. \(w\)\(G_{P}\) there are edges \((o_{i,a},q_{c})\) and \((o_{i,b},q_{d})\))._  
_Lock \(q_{c}\) is said to precede lock \(q_{d}\) in path \(\lambda^{P,i}_{l}\), if \(a\prec b\). This relation is denoted \(q_{c}\prec_{i}^{l}q_{d}\)._  
**Lemma 1**. : _Two threads \(t_{i}\) and \(t_{j}\) are given in the source code of \(P\) application, and path sets \(\lambda^{P,i}\) are known. In both threads, there are operations putting locks \(q_{c}\) and \(q_{d}\)._  
_If there is such a pair of paths: \(\lambda^{P,i}_{l},\lambda^{P,i}_{k}\) for which the following condition is met: \((q_{c}\prec_{i}^{l}q_{d})\bigwedge(q_{d}\prec_{j}^{k}q_{c})\) or \((q_{c}\prec_{j}^{l}q_{d})\bigwedge(q_{d}\prec_{j}^{l}q_{c})\) then in \(P\) application source code there is a resource conflict that will cause a deadlock phenomenon with \(t_{i}\)\(t_{j}\) threads._  
Proof.