# Deadlocks Detection in Multithreaded Applications Based on Source Code Analysis
## 3 Multithreaded Application Source Code Model  
The work [14] presents the author's multithreaded application source code model. Based on that model a theorem was developed, the fulfilment of which means that, in the application, the phenomenon of race condition occurs. For this article, this model was extended and is as follows:  
\[C_{P}=(T_{P},U_{P},R_{P},O_{P},Q_{P},F_{P}) \tag{1}\]  
where:1. \(P\) is the application index,
2. \(T_{P}=\{t_{i}|i=0...\alpha\}\), (\(\alpha\in\mathbb{N}\)) is a set of \(t_{i}\) threads of \(C_{P}\) application, where \(t_{0}\) is the main thread, \(|T_{P}|>1\),
3. \(U_{P}=(u_{b}|b=1...\beta)\), (\(\beta\in\mathbb{N}^{+}\)) is \(u_{b}\) sequence of sets that are subsets of \(T_{P}\) set containing threads working in the same time interval in \(C_{P}\) application, with \(|U_{P}|>2\), \(u_{1}=\{t_{0}\}\) i \(u_{\beta}=\{t_{0}\}\),
4. \(R_{P}=\{r_{c}|c=1...\gamma\},r_{c}=\{v_{1},v_{2},...,v_{\eta}\},(\gamma,\eta \in\mathbb{N}^{+})\) is a set of shared resources of \(C_{P}\) application, and the next elements are sets of names of variables related to a single resource,
5. \(O_{P}=\{o_{ij,j}|i=1...\delta,j=1...e\}\), (\(\delta,\epsilon,\in\mathbb{N}^{+}\)) is a set of all \(C_{P}\)application operations which are atomic operations at a certain level of abstraction, i.e., dividing them into smaller operations is impossible. An operation should be understood as an instruction or function defined in a programming language. Index \(i\) indicates the number of the thread in which the operation is performed, and index \(j\) is the ordinal number of operations working within the same thread,
6. \(Q_{P}=\{q_{s}|s=1...k\},q_{s}=(w_{s},x_{s})\), (\(\kappa,\in\mathbb{N}^{+}\)) - a set of locks available in the program, defined as a pair (mutex variable name \((w_{s})\), a type of lock \((x_{s})\)), where type is understood as one from the set value (PMN, PME, PMR, PMD),
7. \(F_{P}=\{f_{n}|n=1...\}\) i F \(\subseteq(O_{P}\times O_{P})\cup(O_{P}\times R_{P})\cup(R_{P}\times O_{P})\cup( O_{P}\times Q_{P})\cup(Q_{P}\times O_{P})\), (\(i\in\mathbb{N}^{+}\)) - set of edges including: 1. transition edges - specifying the order in which the operation is performed. These edges are pairs \(  
Another significant change is the definition of the elements of the \(R\) resource set. C language has a mechanism of indicators with which one can access the selected memory area in which the resource is located. Therefore, it is reasonable to store in the model all possible variable names referring to the same resource.  
Two new edge types were also introduced to the model: the locking edge and the unlocking edge. The first type leads from the lock to the operation, and the second type leads from the operation to the lock to be released. This solution is a more faithful representation of what is happening in the application code than the solution presented in previous works on the source code model of a multithreaded application.  
In the graphic representation, the frames surrounding the operations will no longer be seen. In further works, the locking and unlocking operations will consist of operation symbols, edges, and a lock symbol. A separate symbol is assigned to each of the three types of locks, i.e., PMN is a triangle symbol, PME is a diamond symbol, PMR is a trapezoid symbol. In the implementation of the pthreads library for Linux, the PMD type is an alias of the PMN type; therefore, in this paper, the PMD type will be synonymous with PMN. If another implementation is used, it should be clearly stated how PMD is represented.