Comparative Modeling and Verification of Pthreads and Dthreads

Yuan Fei; Huibiao Zhu; Xi Wu; Huixing Fang

doi:10.1109/HASE.2016.15

Comparative Modeling and Verification of Pthreads and Dthreads

Yuan Fei
, Huibiao Zhu
, Xi Wu
, Huixing Fang

Software Engineering Institute

East China Normal University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Scopus citations

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.

Original language	English
Title of host publication	Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016
Editors	Radu Babiceanu, Helene Waeselynck, Jie Xu, Raymond A. Paul, Bojan Cukic
Publisher	IEEE Computer Society
Pages	132-140
Number of pages	9
ISBN (Electronic)	9781467399128
DOIs	https://doi.org/10.1109/HASE.2016.15
State	Published - 1 Mar 2016
Event	17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016 - Orlando, United States Duration: 7 Jan 2016 → 9 Jan 2016

Publication series

Name	Proceedings of IEEE International Symposium on High Assurance Systems Engineering
Volume	2016-March
ISSN (Print)	1530-2059

Conference

Conference	17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016
Country/Territory	United States
City	Orlando
Period	7/01/16 → 9/01/16

Keywords

Dthreads
Modeling
Pthreads
Verification

Access to Document

10.1109/HASE.2016.15

Cite this

Fei, Y., Zhu, H., Wu, X., & Fang, H. (2016). Comparative Modeling and Verification of Pthreads and Dthreads. In R. Babiceanu, H. Waeselynck, J. Xu, R. A. Paul, & B. Cukic (Eds.), Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016 (pp. 132-140). Article 7423144 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering; Vol. 2016-March). IEEE Computer Society. https://doi.org/10.1109/HASE.2016.15

Fei, Yuan ; Zhu, Huibiao ; Wu, Xi et al. / Comparative Modeling and Verification of Pthreads and Dthreads. Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016. editor / Radu Babiceanu ; Helene Waeselynck ; Jie Xu ; Raymond A. Paul ; Bojan Cukic. IEEE Computer Society, 2016. pp. 132-140 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering).

@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 = "美国",

}

Fei, Y, Zhu, H, Wu, X & Fang, H 2016, Comparative Modeling and Verification of Pthreads and Dthreads. in R Babiceanu, H Waeselynck, J Xu, RA Paul & B Cukic (eds), Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016., 7423144, Proceedings of IEEE International Symposium on High Assurance Systems Engineering, vol. 2016-March, IEEE Computer Society, pp. 132-140, 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016, Orlando, United States, 7/01/16. https://doi.org/10.1109/HASE.2016.15

Comparative Modeling and Verification of Pthreads and Dthreads. / Fei, Yuan; Zhu, Huibiao; Wu, Xi et al.
Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016. ed. / Radu Babiceanu; Helene Waeselynck; Jie Xu; Raymond A. Paul; Bojan Cukic. IEEE Computer Society, 2016. p. 132-140 7423144 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering; Vol. 2016-March).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Comparative Modeling and Verification of Pthreads and Dthreads

AU - Fei, Yuan

AU - Zhu, Huibiao

AU - Wu, Xi

AU - Fang, Huixing

PY - 2016/3/1

Y1 - 2016/3/1

N2 - 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.

AB - 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.

KW - Dthreads

KW - Modeling

KW - Pthreads

KW - Verification

UR - https://www.scopus.com/pages/publications/84962791846

U2 - 10.1109/HASE.2016.15

DO - 10.1109/HASE.2016.15

M3 - 会议稿件

AN - SCOPUS:84962791846

T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering

SP - 132

EP - 140

BT - Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016

A2 - Babiceanu, Radu

A2 - Waeselynck, Helene

A2 - Xu, Jie

A2 - Paul, Raymond A.

A2 - Cukic, Bojan

PB - IEEE Computer Society

T2 - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016

Y2 - 7 January 2016 through 9 January 2016

ER -

Fei Y, Zhu H, Wu X, Fang H. Comparative Modeling and Verification of Pthreads and Dthreads. In Babiceanu R, Waeselynck H, Xu J, Paul RA, Cukic B, editors, Proceedings - 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016. IEEE Computer Society. 2016. p. 132-140. 7423144. (Proceedings of IEEE International Symposium on High Assurance Systems Engineering). doi: 10.1109/HASE.2016.15

Comparative Modeling and Verification of Pthreads and Dthreads

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this