Datalog-based Scalable Semantic Diffing of Concurrent Programs
| Autor: | Shuvendu K. Lahiri, Chungha Sung, Chao Wang, Constantin Enea |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Model checking
FOS: Computer and information sciences Atomicity Computer Science - Programming Languages Theoretical computer science Computer science Concurrency 020207 software engineering 02 engineering and technology Static analysis Datalog Software Engineering (cs.SE) Computer Science - Software Engineering Program analysis 020204 information systems Scalability Synchronization (computer science) 0202 electrical engineering electronic engineering information engineering Rule of inference computer computer.programming_language Programming Languages (cs.PL) |
| Zdroj: | ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering-ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering -ASE 2018 |
| DOI: | 10.48550/arxiv.1807.03777 |
| Popis: | When an evolving program is modified to address issues related to thread synchronization, there is a need to confirm the change is correct, i.e., it does not introduce unexpected behavior. However, manually comparing two programs to identify the semantic difference is labor intensive and error prone, whereas techniques based on model checking are computationally expensive. To fill the gap, we develop a fast and approximate static analysis for computing synchronization differences of two programs. The method is fast because, instead of relying on heavy-weight model checking techniques, it leverages a polynomial-time Datalog-based program analysis framework to compute differentiating data-flow edges, i.e., edges allowed by one program but not the other. Although approximation is used our method is sufficiently accurate due to careful design of the Datalog inference rules and iterative increase of the required data-flow edges for representing a difference. We have implemented our method and evaluated it on a large number of multithreaded C programs to confirm its ability to produce, often within seconds, the same differences obtained by human; in contrast, prior techniques based on model checking take minutes or even hours and thus can be 10x to 1000x slower. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|