Comparative Modeling and Verification of Pthreads and Dthreads

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

Full description

Saved in:
Bibliographic Details
Main Authors: Yuan Fei, Huibiao Zhu, Xi Wu, Huixing Fang
Format: Conference Proceeding
Language:English
Subjects:
Concurrent computing
Data models
Dthreads
Instruction sets
Message systems
Modeling
Pthreads
Runtime
Synchronization
System recovery
Verification
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
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 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.
ISSN:1530-2059
2640-7507
DOI:10.1109/HASE.2016.15