Paper Info
Title
Verification of Static and Dynamic Barrier Synchronization Using Bounded Permissions.
Abstract
Mainstream languages such asC/C++ (with Pthreads), Java, and. NET provide programmers with both static and dynamic barriers for synchronizing concurrent threads in fork/join programs. However, such barrier synchronization in fork/join programs is hard to verify since programmers must not only keep track of the dynamic number of participating threads, but also ensure that all participants proceed in correctly synchronized phases. As barriers are commonly used in practice, verifying correct synchronization of barriers can provide compilers and analysers with important phasing information for improving the precision of their analyses and optimizations. In this paper, we propose an approach for statically verifying correct synchronization of static and dynamic barriers in fork/join programs. We introduce the notions of bounded permissions and phase numbers for keeping track of the number of participating threads and barrier phases respectively. The approach has been proven sound, and a prototype of it (named VeriBSync) has been implemented for verifying barrier synchronization of realistic programs in the SPLASH-2 benchmark suite.
Year
DOI
Venue
2013
10.1007/978-3-642-41202-8_16
Lecture Notes in Computer Science
Keywords
Field
DocType
Verification,Concurrency,Barrier,Logic,Permissions
Fork (system call),Synchronization,Programming language,Computer science,Concurrency,Thread (computing),Real-time computing,POSIX Threads,Compiler,Synchronization (computer science),Java,Distributed computing
Conference
Volume
ISSN
Citations 
8144
0302-9743
6
PageRank 
References 
Authors
0.47
22
3
Name
Order
Citations
PageRank
Duy-Khanh Le1121.92
Wei-Ngan Chin286863.37
Yong Meng Teo356454.77