Concurrent data structures or classes are designed to provide safe accesses and simultaneous updates by multiple threads to shared objects in a concurrent environment, with the goal of enhancing parallelism and throughput. However, testing concurrent objects poses significant challenges due to the potential explosion of concurrency test spaces, the variety of programming vulnerabilities, and the inherent nondeterminism of concurrent test executions. In this paper, we propose an Intrathread Method Orders based Adaptive Concurrency Testing (IMOACT) framework for concurrent objects. IMOACT can capture diverse behaviors of interthread method pairs through characterizing concurrent execution contexts with intrathread method orders. Moreover, IMOACT can adaptively optimize concurrent test executions by generating scheduling sequences based on the key scheduling points visited so far, streamlining test generation and execution organically across multiple tests. Experimental case studies with typical C/C++ concurrent classes demonstrate that IMOACT outperforms baseline approaches. On average, IMOACT promotes the effectiveness of detecting concurrency bugs by 65%, and achieves a speedup of 2.43x compared to the underlying state-of-the-art concurrency testing approach.

Although machine learning models have been remarkably effective for decision-making tasks such as employment, insurance, and criminal justice, it remains urgent yet challenging to ensure model predictions are reliable and socially fair. This amounts to detecting and repairing potential discriminatory defects of machine learning models extensively with authentic testing data. In this paper, we propose a novel Mahalanobis distance guided Adaptive Exploratory Fairness Testing (MAEFT) approach, which searches for individual discriminatory instances (IDIs) through deep reinforcement learning with an adaptive extension of Boltzmann exploration, and significantly reduces overestimation. MAEFT uses Mahalanobis distances to guide the search with realistic correlations between input features. Thus, through learning a more accurate state-action value approximation, MAEFT can touch a much wider valid input space, reducing sharply the number of duplicate instances visited, and identify more unique tests and IDIs calibrated for the realistic feature correlations. Compared with state-of-the-art black-box and white-box fairness testing methods, our approach generates on average 4.65%-161.66% more unique tests and identifies 154.60%-634.80% more IDIs, with a performance speed-up of 12.54%-1313.47%. Moreover, the IDIs identified by MAEFT can be well exploited to repair the original models through retraining. These IDIs lead to, on average, a 59.15% boost in model fairness, 15.94%-48.73% higher than those identified by the state-of-the-art fairness testing methods. The models retrained with MAEFT also exhibit 37.66%-46.81% stronger generalization ability than those retrained with the state-of-the-art fairness testing methods.

Concurrent programs are normally composed of multiple concurrent threads sharing memory space. These threads are often interleaved, which may lead to some non-determinism in execution results, even for the same program input. This poses huge challenges to the testing of concurrent programs, especially on the test result verification—that is, the prevalent existence of the oracle problem. In this article, we investigate the application of metamorphic testing (MT), a mainstream technique to address the oracle problem, into the testing of concurrent programs. Based on the unique features of interleaved executions in concurrent programming, we propose an extended notion of metamorphic relations, the core part of MT, which are particularly designed for the testing of concurrent programs. A comprehensive testing approach, namely ConMT , is thus developed and a tool is built to automate its implementation on concurrent programs written in Java. Empirical studies have been conducted to evaluate the performance of ConMT, and the experimental results show that in addition to addressing the oracle problem, ConMT outperforms the baseline traditional testing techniques with respect to a higher degree of automation, better bug detection capability, and shorter testing time. It is clear that ConMT can significantly improve the cost-effectiveness for the testing of concurrent programs and thus advances the state of the art in the field. The study also brings novelty into MT, hence promoting the fundamental research of software testing.

Accuracy and individual fairness are both crucial for trustworthy machine learning, but these two aspects are often incompatible with each other so that enhancing one aspect may sacrifice the other inevitably with side effects of true bias or false fairness. We propose in this paper a new fairness criterion, accurate fairness, to align individual fairness with accuracy. Informally, it requires the treatments of an individual and the individual's similar counterparts to conform to a uniform target, i.e., the ground truth of the individual. We prove that accurate fairness also implies typical group fairness criteria over a union of similar sub-populations. We then present a Siamese fairness in-processing approach to minimize the accuracy and fairness losses of a machine learning model under the accurate fairness constraints. To the best of our knowledge, this is the first time that a Siamese approach is adapted for bias mitigation. We also propose fairness confusion matrix-based metrics, fair-precision, fair-recall, and fair-F1 score, to quantify a trade-off between accuracy and individual fairness. Comparative case studies with popular fairness datasets show that our Siamese fairness approach can achieve on average 1.02%-8.78% higher individual fairness (in terms of fairness through awareness) and 8.38%-13.69% higher accuracy, as well as 10.09%-20.57% higher true fair rate, and 5.43%-10.01% higher fair-F1 score, than the state-of-the-art bias mitigation techniques. This demonstrates that our Siamese fairness approach can indeed improve individual fairness without trading accuracy. Finally, the accurate fairness criterion and Siamese fairness approach are applied to mitigate the possible service discrimination with a real Ctrip dataset, by on average fairly serving 112.33% more customers (specifically, 81.29% more customers in an accurately fair way) than baseline models.

Recent studies have shown that ad-hoc image transformations are effective for defending certain adversarial attacks. It is desirable to determine which transformations are more effective than others for adversarial defenses before these transformations are being deployed in practice. We propose in this paper the notion of Critical Transformation Robustness (CTR), which can indicate potentially the detection performance of an input transformation through the difference between its CTR on clean inputs and that on adversarial ones. Then, based on this new notion, we further present a general training framework that can deliver an effective and efficient adversarial detector, which features in a customized combination of specific input transformations for defending the given, possibly mixed, adversarial attacks. We evaluate our training framework on 3 typical image datasets with 17 types of popular input transformations for detecting a mixture of 22 types of adversarial attacks. Experimental results show that the CTR differences between the clean and adversarial inputs can essentially guide the selection of an effective combination of input transformations with their nearly-optimal parameter values. Furthermore, compared with the state-of-the-art input transformation-based adversarial detection methods, the detectors generated by our training framework exhibit on average 73.4% - 87.5% higher performance on the mixed adversarial attacks.

A deep learning model always misclassifies an out-of-distribution input, which is not of any category that the deep learning model is trained for. Hence, out-of-distribution detection is practically an important task for ensuring the safety and reliability of a deep learning based system. We present in this paper the notion of relative activation and deactivation to interpret the inference behavior of the deep learning model. Then, we propose a relative activation-deactivation abstraction approach to characterize the decision logic of the deep learning model. The relative activation-deactivation abstractions enjoy close intra-class aggregation for each category under training, as well as diverse inter-class separation between various categories under training. We further propose an out-of-distribution detection algorithm based on the relative activation-deactivation abstraction approach, following the underlying principle that the relative activation-deactivation abstraction of a deep learning model under an out-of-distribution input is far away from the one for the predicted category the deep learning model outputs. Our detection algorithm does not require any designed perturbation to the input data, nor any hyperparameter tuning to the deep learning model with out-of-distribution data. We evaluate the detection algorithm with 8 typical benchmark datasets in literature. The experimental results show that our detection algorithm can achieve better and more stable performance than the state-of-the-art white-box abstraction based detection algorithms, with significantly more true positive and less false positive alerts for out-of-distribution detection.

Machine learning models play an important role for decision-making systems in areas such as hiring, insurance, and predictive policing. However, it still remains a challenge to guarantee their trustworthiness. Fairness is one of the most critical properties of these machine learning models, while individual discriminatory cases may break the trustworthiness of these systems severely. In this paper, we present a systematic approach of testing the fairness of a machine learning model, with individual discriminatory inputs generated automatically in an adaptive manner based on the state-of-the-art deep reinforcement learning techniques. Our approach can explore and exploit the input space efficiently, and find more individual discriminatory inputs within less time consumption. Case studies with typical benchmark models demonstrate the effectiveness and efficiency of our approach, compared to the state-of-the-art black-box fairness testing approaches.

Linearizability is an important correctness criterion that guarantees the safety of concurrent data structures.Due to the nondeterminism of concurrent executions, reproduction and localization of a linearizability fault still remain challenging.The existing work mainly focuses on model checking the thread schedule space of a concurrent program on a fine-grained (state) level, and hence suffers from the severe problem of state space explosion.This paper presents a tool called CGVT to build a small test case that is sufficient enough for reproducing a linearizability fault.Given a possibly long history that has been detected non-linearizable, CGVT first locates the operations causing a linearizability violation, and then synthesizes a short test case for further investigation.Moreover, we present several optimization techniques to improve the effectiveness and efficiency of CGVT.We have applied CGVT to 10 concurrent objects, while the linearizability of some of the concurrent objects is unknown yet.The experiments show that CGVT is powerful and efficient enough to build the test cases adaptable for a fine-grained analysis.

Linearizability is an important correctness criterion that guarantees the safety of concurrent data structures. Due to the nondeterminism of concurrent executions, reproduction and localization of a linearizability fault still remain challenging. The existing works mainly focus on model checking the thread schedule space of a concurrent program on a fine-grained (state) level, and hence suffer from the severe problem of state space explosion. This paper presents a tool called CGVT to build a small test case that is sufficient enough for reproducing a linearizability fault. Given a possibly long history that has been detected nonlinearizable, CGVT first locates the operations causing a linearizability violation and then synthesizes a minimum test case for further investigation. Moreover, we present several optimization techniques to improve the effectiveness and efficiency of CGVT. We have applied CGVT to 10 concurrent objects, while the linearizability of some of the objects is unknown yet. The experiments show that CGVT is powerful and efficient enough to build the test cases more adaptable for fine-grained fault localization.

The state-of-the-art model-checkers for probabilistic timed automata (PTAs) use separate representations for the dense-time and discrete parts of PTA states. In the literature, integrated state-space representations based on decision diagrams, e.g., RED diagrams (the underlying symbolic representation in the model checker RED), have shown considerable performance enhancement in model-checking timed automata (TAs) and linear hybrid automata (LHAs). A RED diagram for a TA can represent the dense-time and discrete parts of TA states in a single and integrated decision diagram. In this work, we experiment to investigate whether such performance enhancement can be duplicated with PTA model-checking. Specifically, we propose a lightweight extension to RED diagrams to represent quantitative states of PTAs in an integrated manner, yet preserving the structure-sharing capacity of RED diagrams. We then develop and implement a symbolic reachability analysis algorithm for PTAs based on the extended RED diagrams. We further carry out experiments with the PTA benchmarks from a popular probabilistic model checker PRISM to evaluate the performance of such integrated decision diagrams and the reachability analysis algorithm. Experimental results show that our approach can indeed help to improve the time-efficiency and scalability of PTA model-checking.

It is still a challenge to select "good" test inputs for concurrent programs within limited testing resources. We present in this paper a test case diversity metric for multi-threaded programs, which evaluates a test input with its effect in exposing concurrent thread interactions. We then propose an input-driven active testing approach with two test input selection strategies based on our test case diversity metric. We implement our testing approach based on Maple, an interleaving coverage-driven active testing tool. The effectiveness and efficiency of our testing approach are compared closely with Maple, which on its own is supplied with random test inputs. Experimental results show that our testing approach can outperform the original active testing approach in the number of test inputs executed and the time usage for fulfilling the interleaving coverage criterion of Maple. The selected test inputs based on our test case diversity metric are very cost-effective in exposing concurrent thread interactions and hence can help detect concurrency bugs with less cost and effort.

Model checking has been widely applied to the verification of network protocols. Alternatively, optimisation based approaches have been proposed to reason about the large scale dynamics of networks, particularly with regard to congestion and rate control protocols such as TCP. This paper intends to provide a first bridge and explore synergies between these two approaches. We consider a series of discrete approximations to the optimisation based congestion control algorithms. Then we use branching time temporal logic to specify formally the convergence criteria for the system dynamics and present results from implementing these algorithms on a state-of-the-art model checker. We report on our experiences in using the abstraction of model checking to capture features of the continuous dynamics typical of optimisation based approaches.

We present an implementation of model checking for probabilistic and stochastic extensions of the pi-calculus, a process algebra which supports modelling of concurrency and mobility. Formal verification techniques for such extensions have clear applications in several domains, including mobile ad-hoc network protocols, probabilistic security protocols and biological pathways. Despite this, no implementation of automated verification exists. Building upon the pi-calculus model checker MMC, we first show an automated procedure for constructing the underlying semantic model of a probabilistic or stochastic pi-calculus process. This can then be verified using existing probabilistic model checkers such as PRISM. Secondly, we demonstrate how for processes of a specific structure a more efficient, compositional approach is applicable, which uses our extension of MMC on each parallel component of the system and then translates the results into a high-level modular description for the PRISM tool. The feasibility of our techniques is demonstrated through a number of case studies from the pi-calculus literature.

A predicate sequencing constraint logic (PSCL) is proposed to represent test purpose for concurrent program testing. The logic is capable of expressing not only sequencing relationships among input and output events, but also data dependencies between event parameters. A PSCL-based symbolic test generation method is developed to automatically derive symbolic test cases that incorporate given data dependency constraints as verdict conditions. The method works in a syntactic way without referring to concrete program states and the derived test cases allow dynamic test data selection according to the response from the software under test. The advantage of the approach is demonstrated with a case study.

An enhanced version of metamorphic testing, namely n-iterative metamorphic testing, is proposed to systematically exploit more information out of metamorphic tests by applying metamorphic relations in a chain style. A contrastive case study, conducted within an integrated testing environment MTest, shows that n-iterative metamorphic testing exceeds metamorphic testing and special case testing in terms of their fault detection capabilities. Another advantage of n-iterative metamorphic testing is its high efficiency in test case generation.