Demystifying Performance Regressions in String SolversVirtual
Abstract—Over the past few years, SMT string solvers have found their applications in an increasing number of domains, such as program analyses in mobile and Web applications, which require the ability to reason about string values. A series of research has been carried out to find quality issues of string solvers in terms of its correctness and performance. Yet, none of them has considered the performance regressions happening across multiple versions of a string solver. To fill this gap, in this paper, we focus on solver performance regressions (SPRs), i.e., unintended slowdowns introduced during the evolution of string solvers. To this end, we develop SPRFinder to not only generate test cases demonstrating SPRs, but also localize the probable causes of them, in terms of commits. We evaluated the effectiveness of SPRFinder on three state-of-the-art string solvers, i.e., Z3Seq, Z3Str3, and CVC4. The results demonstrate that SPRFinder is effective in generating SPR-inducing test cases and also able to accurately locate the responsible commits. Specifically, the average running time on the target versions is 13.2× slower than that of the reference versions. Besides, we also conducted the first empirical study to peek into the characteristics of SPRs, including the impact of random seed configuration for SPR detection, understanding the root causes of SPRs, and characterizing the regression test cases through case studies. Finally, we highlight that 149 unique SPR-inducing commits were discovered in total by SPRFinder, and 16 of them have been confirmed by the corresponding developers. The original paper can be accessed from https://ieeexplore.ieee.org/abstract/document/9760153
Wed 12 OctDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Technical Session 19 - Formal Methods and Models IResearch Papers / Journal-first Papers / Tool Demonstrations at Ballroom C East Chair(s): Michalis Famelis Université de Montréal | ||
16:00 20mResearch paper | Automatic Comment Generation via Multi-Pass Deliberation Research Papers Fangwen Mu Institute of Software Chinese Academy of Sciences, Xiao Chen Institute of Software Chinese Academy of Sciences, Lin Shi ISCAS, Song Wang York University, Qing Wang Institute of Software at Chinese Academy of Sciences | ||
16:20 10mDemonstration | Building recommender systems for modelling languages with DroidVirtual Tool Demonstrations Lissette Almonte Universidad Autónoma de Madrid, Esther Guerra Universidad Autónoma de Madrid, Iván Cantador Universidad Autónoma de Madrid, Juan de Lara Autonomous University of Madrid Pre-print Media Attached | ||
16:30 10mDemonstration | RobSimVer: A Tool for RoboSim Modeling and AnalysisVirtual Tool Demonstrations Dehui Du East China Normal University, Ana Cavalcanti University of York, JihuiNie East China Normal University | ||
16:40 20mResearch paper | Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural NetworksVirtual Research Papers Zhaodi Zhang East China Normal University, Yiting Wu East China Normal University, Si Liu ETH Zurich, Jing Liu East China Normal University, Min Zhang East China Normal University | ||
17:00 20mResearch paper | Efficient Synthesis of Method Call Sequences for Test Generation and Bounded VerificationVirtual Research Papers Yunfan Zhang Peking University, Ruidong Zhu Peking University, Yingfei Xiong Peking University, Tao Xie Peking University | ||
17:20 20mPaper | Demystifying Performance Regressions in String SolversVirtual Journal-first Papers Yao Zhang , Xiaofei Xie Singapore Management University, Singapore, Yi Li Nanyang Technological University, Yun Lin National University of Singapore, Sen Chen Tianjin University, Yang Liu Nanyang Technological University, Xiaohong Li TianJin University Link to publication DOI | ||
17:40 20mResearch paper | Detecting Semantic Code Clones by Building AST-based Markov Chains ModelVirtual Research Papers Yueming Wu Nanyang Technological University, Siyue Feng Huazhong University of Science and Technology, Deqing Zou Huazhong University of Science and Technology, Hai Jin Huazhong University of Science and Technology |