Concurrent programs must be thoroughly tested as concurrency bugs are notoriously hard to detect. Code coverage criteria can be used to quantify the richness of a test suite (e.g., whether a program has been tested sufficiently) or provide practical guidelines on test case generation (e.g., as objective functions used in program fuzzing engines). Traditional code coverage criteria are however designed for sequential programs and thus ineffective for concurrent programs. In this work, we introduce a novel code coverage criteria for testing thread-safe classes called MAP (short for memory-access patterns) coverage. The motivation is that concurrency bugs are often correlated with certain memory-access patterns and thus it is desirable to comprehensively cover all memory-access patterns. Furthermore, we propose a testing method for maximizing MAP-coverage. Our method has been implemented as a self-contained toolkit and the experiment results on 20 benchmark programs show that our toolkit outperforms existing testing methods. Lastly, we show empirically that there exists positive correlation between MAP-coverage and the effectiveness of a set of test executions.

Zan Wang

College of Intelligence and Computing, Tianjin University

China

Yingquan Zhao

College of Intelligence and Computing, Tianjin University

Shuang Liu

College of Intelligence and Computing, Tianjin University

Jun Sun

Singapore Management University, Singapore

Singapore

Xiang Chen

School of Information Science and Technology, Nantong University

China

Huarui Lin

College of Intelligence and Computing, Tianjin University

This paper investigates using compiler technology to automatically convert sequential C++ data abstractions, e.g., queues, stacks, maps, and trees, to concurrent lock-free implementations. By automatically tailoring a number of state-of-the-practice synchronization methods to the underlying sequential implementations of different data structures, our automatically synchronized code can attain performance competitive to that of manually-written concurrent data structures by experts and much better performance than heavier-weight support by software transactional memory (STM).

Jiange Zhang

University of Colorado Colorado Springs

Qing Yi

University of Colorado Colorado Springs

Damian Dechev

University of Central Florida

United States

While CUDA has been the dominated parallel computing platform and programming model for general-purpose GPU computing, CUDA synchronization undergoes significant challenges for GPU programmers due to its intricate parallel computing mechanism and coding practices. In this paper,we propose AuCS, the first general framework to automate synchronization for CUDA kernel functions. AuCS transforms the original LLVM-level CUDA program control flow graph in a semantic-preserving manner for exploring the possible barrier function locations. Accordingly, AuCS develops mechanisms to correctly place barrier functions for automating synchronization in multiple erroneous (challenging-to-be-detected) synchronization scenarios, including data race, barrier divergence, redundant barrier functions. To evaluate the effectiveness and efficiency of AuCS, we conduct an intensive set of experiments and the results suggest that AuCS can automate 20 out of 24 erroneous synchronization scenarios.

Mingyuan Wu

Southern University of Science and Technology

Lingming Zhang

The University of Texas at Dallas

Cong Liu

Eindhoven University of Technology

Shin Hwei Tan

Southern University of Science and Technology

China

Yuqun Zhang

Southern University of Science and Technology

Existing replay techniques record inter-thread access event orders on shared memory locations to facilitate replay. Some techniques propose strategies to reduce the recorded events often at the expense of deterministic trace reproduction. We propose a technique based on the division of a thread’s execution trace into sequential code blocks called transactions. Our insight is that there are usually few to no atomicity violations reported during a program execution. Based on our insight, we present TPLAY, a novel deterministic replay technique which records thread access interleavings on shared memory locations at a transactional level. TPLAY also generates an artificial pair of interleavings when an atomicity violation is reported on a transaction. We present an experiment and analyze the results of our experiment using the Splash2x extension of the PARSEC benchmark suite. The experimental results indicate that on average, TPLAY experiences a 13-fold improvement in record log sizes and achieves 98% replay probability on subject programs in comparison to existing work.

Ernest Bota Pobee

City University of Hong Kong

Xiupei Mei

City University of Hong Kong

Wing-Kwong Chan

City University of Hong Kong, Hong Kong

China

Swarm-based verification methods split a verification problem into a large number of independent simpler tasks and so exploit the availability of large numbers of cores to speed up verification. Lazy-CSeq is a BMC-based bug-finding tool for C programs using POSIX threads that is based on sequentialization. Here we present the tool VeriSmart 2.0, which extends Lazy-CSeq with a swarm-based bug-finding method. The key idea of this approach is to constrain the interleavings such that context switches can only happen within selected tiles (more specifically, contiguous code segments within the individual threads). This under-approximates the program’s behaviors, with the number and size of tiles as additional parameters, which allows us to vary the complexity of the tasks. Overall, this significantly improves peak memory consumption and (wall-clock) analysis time.

Sources: http://www.cs.sun.ac.za/~bfischer/verismart.tgz

Bernd Fischer

Stellenbosch University

South Africa

Salvatore La Torre

Università degli Studi di Salerno

Italy

Gennaro Parlato

University of Molise

Concurrency vulnerabilities are extremely harmful and can be frequently exploited to launch severe attacks. Due to the non-determinism of multithreaded executions, it is very difficult to detect them. Recently, data race detectors and techniques based on maximal casual model have been applied to detect concurrency vulnerabilities. However, the former are ineffective and the latter report many false negatives. In this paper, we present CONVUL, an effective tool for concurrency vulnerability detection. CONVUL is based on exchangeable events, and adopts novel algorithms to detect three major kinds of concurrency vulnerabilities. To illustrate the competitiveness of CONVUL, we performed a comparison with three widely-used data race detectors and one recent tool based on maximal casual model. In our experiments, CONVUL detected 9 of 10 known vulnerabilities and found 6 zero-day vulnerabilities on MySQL, while other tools only detected at most 3 out of these 16 vulnerabilities. Our tool and data are available at CONVUL web page: https://sites.google.com/site/convultool. A demonstration video is available at https://youtu.be/-26C6ULxtbk

Ruijie Meng

University of Chinese Academy of Sciences

Biyun Zhu

University of Chinese Academy of Sciences

Hao Yun

University of Chinese Academy of Sciences

Haicheng Li

University of Chinese Academy of Sciences

Yan Cai

Institute of Software, Chinese Academy of Sciences

China

Zijiang Yang

Western Michigan University