@inproceedings{cebc4fb2b61f4f25b595be95261b3693,
title = "Comparative Modeling and Verification of Pthreads and Dthreads",
abstract = "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 and data race problems due to the potential non-deterministic execution behaviors between parallel threads. Dthreads is another multithreading model re-implementing Pthreads, which was proposed by Liu et al. for efficient deterministic multithreading. Under specific test cases, they found out that Dthreads can effectively prevent data races. But they have not made comparison test with Pthreads. In order to formally compare Pthreads with Dthreads over deadlocks and data races, in this paper, we apply CSP (Communicating Sequential Processes) to model part of APIs in Pthreads and Dthreads, as well as two classical example programs. By using the model checker PAT (Process Analysis Toolkit), for our considered examples, we verify that deadlocks and data races exist in Pthreads, but do not exist in Dthreads. Our comparative modeling and verification of Pthreads and Dthreads show that Dthreads is better than Pthreads on eliminating data races and preventing deadlocks.",
keywords = "Dthreads, Modeling, Pthreads, Verification",
author = "Yuan Fei and Huibiao Zhu and Xi Wu and Huixing Fang",
note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016 ; Conference date: 07-01-2016 Through 09-01-2016",
year = "2016",
month = mar,
day = "1",
doi = "10.1109/HASE.2016.15",
language = "英语",
series = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",
publisher = "IEEE Computer Society",
pages = "132--140",
editor = "Radu Babiceanu and Helene Waeselynck and Jie Xu and Paul, \{Raymond A.\} and Bojan Cukic",
booktitle = "Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016",
address = "美国",
}