Comparative modelling and verification of Pthreads and Dthreads

Fei, Yuan, Zhu, Huibiao, Wu, Xi, Fang, Huixing and Qin, Shengchao (2018). Comparative modelling and verification of Pthreads and Dthreads. In: HASE 2016: 17 International Symposium on High Assurance Systems Engineering, City of Singapore, Singapore, (1-33). Sep 12, 2016. doi:10.1002/smr.1919


Author Fei, Yuan
Zhu, Huibiao
Wu, Xi
Fang, Huixing
Qin, Shengchao
Title of paper Comparative modelling and verification of Pthreads and Dthreads
Conference name HASE 2016: 17 International Symposium on High Assurance Systems Engineering
Conference location City of Singapore, Singapore
Conference dates Sep 12, 2016
Journal name Journal of Software: Evolution and Process   Check publisher's open access policy
Place of Publication Oxford, United Kingdom
Publisher John Wiley and Sons
Publication Year 2018
Sub-type Fully published paper
DOI 10.1002/smr.1919
Open Access Status Not yet assessed
ISSN 2047-7481
2047-7473
Volume 30
Issue 3
Start page 1
End page 33
Total pages 33
Language eng
Abstract/Summary The POSIX threads (Pthreads) library is a thread API for C/C++ to control parallel threads and spawn concurrent process flows. Programming in Pthreads usually suffers from undesirable deadlock, data race, and race condition problems due to the potential nondeterministic execution behaviors between parallel threads. Dthreads, as another multithreading model that re-implements Pthreads, was proposed by Liu et al for efficient deterministic multithreading. They found out that, under specific test cases, Dthreads can effectively prevent data races. However, no comparison test has been made with Pthreads. To perform a formal comparison between Pthreads and Dthreads over deadlocks, data races, and race conditions, in this paper, we adopt CSP (communicating sequential processes) as a formal model for specifying part of API functions in Pthreads and Dthreads and illustrate the model construction using 4 classical example programs. By feeding the models into the model checker PAT (process analysis toolkit), we have verified that deadlocks and data races exist in Pthreads, but do not exist in Dthreads, for the considered programs. We have also found that neither of them can prevent race conditions. Our comparative modelling and verification of Pthreads and Dthreads show that though Dthreads cannot prevent all the deadlock situations, shown by verification results of another 2 example programs, Dthreads is better than Pthreads on eliminating data races and preventing deadlocks. Considering limited scalability of Dthreads, we have introduced a new programming model to support coarse granularity in bank transfer. Our modelling is also extended by covering the synchronization operations in Liu et al work.
Subjects 1712 Software
Keyword CSP
Dthreads
modelling
Pthreads
verification
Q-Index Code E1
Q-Index Status Provisional Code
Grant ID 61321064
Institutional Status UQ

Document type: Conference Paper
Sub-type: Fully published paper
Collection: School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Thu, 22 Mar 2018, 23:48:56 EST