# Atomicity Violation in Multithreaded Applications and Its Detection in Static Code Analysis Process
## 5 Multithreaded Application Source Code Model  
Locating an atomicity violation is possible using the source code model of a multithreaded application [2]; however, this model should be extended with a set that will describe the relationship between the two operations. This model looks as follows:  
\[C_{P}=(T_{P},U_{P},R_{P},O_{P},Q_{P},F_{P},B_{P}) \tag{1}\]  
where:  
1. \(P\) is the application index;
2. \(T_{P}=\{t_{i}|i=0...\alpha\}\), \((\alpha\in\mathbb{N})\) is a a set of threads \(t_{i}\) 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 a sequence of \(u_{b}\), sets which are subsets of \(T_{P}\) containing threads working in the same period of time in the application \(C_{P}\), whereas \(|U_{P}|>2\), \(u_{1}=\{t_{0}\}\) and \(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 collection of shared application resources \(C_{P}\), and the subsequent elements are sets of variable names relating to a single resource;
5. \(O_{P}=\{o_{i,j}|i=1...\delta,j=1...e\}\), \((\delta,e,\in\mathbb{N}^{+})\) is a set of all \(C_{P}\) application operations which are atomic at a certain level of abstraction--i.e., dividing them into smaller operations is impossible (it 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...\kappa\},q_{s}=(w_{s},x_{s}),(\kappa,\in\mathbb{N}^{+})\)--a set of all locks available in the program, defined as a pair of variables, type of lock, where the type is understood as one of the set values (PMN, PME, PMR, PMD);
7. \(F_{P}=\{f_{n}|n=1...l\}\) and \(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})\), (\(\iota\in\mathbb{N}^{+}\))--a set of edges including: 1. Transition edges--specifying the order in which the operation is performed. These edges are pairs \(f_{n}=(o_{i,j},o_{i,k})\), where the elements describe two successive operations \(o_{i,j}\in O_{P}\); 2. Usage edges--indicating resources that change during the operation. These edges are pairs \(f_{n}=(o_{i,j},r_{c})\), in which one element is operation \(o_{i,j}\in O_{P}\), and the other is resource \(r_{c}\in R_{P}\);* Dependency edges--indicating operations depending on the current value of one of the resources. These edges are pairs \(f_{n}=(r_{c},o_{i,j})\), in which one element is the resource \(r_{c}\in R_{P}\), and the other is the operation \(o_{i,j}\in O_{P}\);
* Locking edges--indicating the operation applying the selected lock. These edges are pair \(f_{n}=(q_{s},o_{i,j})\), in which one element is the lock, and the other is the locking operation;
* Unlocking edge--indicating the operation releasing the selected lock. These edges are pairs \(f_{n}=(o_{i,j},q_{s})\), in which one element is the unlocking operation, and the other is the released lock;
* \(B_{P}=(B_{P}^{\text{FWD}},B_{P}^{\text{BWD}},B_{P}^{\text{SYM}})\)--sequence of sets:
* \(B_{P}^{\text{FWD}}\) a set of pairs of forward relationship operations: \(B_{P}^{\text{FWD}}=\{(o_{i,j},o_{a,b});o_{i,j},o_{a,b}\in O_{P}\}\);
* \(B_{P}^{\text{BWD}}\) a set of pairs of backward relationship operations: \(B_{P}^{\text{BWD}}=\{(o_{i,j},o_{a,b});o_{i,j},o_{a,b}\in O_{P}\}\);
* \(B_{P}^{\text{SYM}}\) family of pairs of operations related by a symmetrical relation: \(B_{P}^{\text{SYM}}=\{\{o_{i,j},o_{a,b}\};o_{i,j},o_{a,b}\in O_{P}\}\). Introduced into the model set \(B_{P}\) in the graphical representation is as shown in Figure 2. If a pair of operations is in a **forward** relationship with each other, then the edge connecting the two operations has a filled ring at the operation after which the second operation is required.