The shift-left principle in the industry requires us to test a software application as early as possible. In particular, when code changes in a microservice application are committed to the code repository, we have to efficiently identify all public microservice interfaces affected by the changes so that the impacted interfaces can be tested as soon as possible. However, developing an efficient change impact analysis is extremely challenging in microservices due to the multilingual problem: microservice applications are often implemented using varying programming languages and involve diverse frameworks and configuration files. To address this issue, this paper presents MICROSCOPE, a language-agnostic change impact analysis that uniformly represents code, configuration files, frameworks, and code changes by relational Datalog rules. MICROSCOPE then benefits from an efficient Datalog solver to identify impacted interfaces. Experiments based on the use of MICROSCOPE in Ant Group, a leading software vendor, demonstrate that MICROSCOPE is both effective and fast, as it successfully identifies interfaces affected by 112 code commits, with moderate time overhead, and could reduce 97% of interfaces to test and save 73% of testing time after code changes.

A FinTech system is a cluster of FinTech applications that intensively interact with databases containing a large quantity of user data. To ensure data consistency, it is a common practice to specify data constraints to validate data at runtime. However, data constraints often evolve according to changes in business requirements. Meanwhile, the developers can hardly keep up with the latest requirements during the development cycle. Such an information barrier increases the communication burden and prevents FinTech applications from being updated in time, impeding the development cycle significantly. In this paper, we present a comprehensive empirical study on data constraints in FinTech systems, investigating how they evolve and affect the development process. Our results show that developers find it hard to update their code timely because no mapping from data constraint changes to code is provided. Inspired by the findings from code updates respecting data constraint changes, we propose DCLINK, a traceability link analysis for linking each data constraint change to target methods demanding the code update in the FinTech application. We extensively evaluate DCLINK upon real-world change cases in Ant Group. The results show that DCLINK can effectively and efficiently localize the target methods.

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV1 and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.

MPI is widely used in high performance computing. In this extended abstract, we report our current status of analyzing MPI programs. Our method can provide coverage of both input and non-determinism for MPI programs with mixed blocking and non-blocking operations. In addition, to improve the scalability further, a deadlock-oriented guiding method for symbolic execution is proposed. We have implemented our methods, and the preliminary experimental results are promising.

Asynchrony based overlapping of computation and communication is commonly used in MPI applications. However, this overlapping introduces synchronization errors frequently in asynchronous MPI programming. In this paper, we propose a symbolic execution based method for detecting input-related synchronization errors. The path space of an MPI program is systematically explored, and the related operations of the synchronization errors in the program are checked specifically. In addition, two optimizations are proposed to improve the efficiency. We have implemented our method as a prototype tool based on the symbolic executor Cloud9. The results of the extensive experiments indicate the effectiveness of our method.