Cited By
View all- Jakobs M(2021)PatEC: Pattern-Based Equivalence CheckingModel Checking Software10.1007/978-3-030-84629-9_7(120-139)Online publication date: 12-Jul-2021
Verifying Parallel Code After Refactoring Using Equivalence Checking
Pages 59 - 73
Abstract
To take advantage of multi-core systems, programmers are replacing sequential software with parallel software. Software engineers often avoid writing their parallel software from scratch and prefer refactoring their legacy application, either manually or with the help of a refactoring tool. In either case, it is extremely challenging to produce correct parallel code, taking into account all synchronization issues. Furthermore, the complexity of parallel code makes its verification extremely difficult. We introduce a method for the verification of parallel code after refactoring. Our method, which is based on symbolic interpretation, leverages the original sequential code that in most cases was already tested and/or verified, and checks whether it is equivalent to the code after refactoring. The advantage of this method is that it can generically find any problem in the parallel code that does not exist in the original sequential code. As a result, it can help create higher quality and safer parallel code.
References
[1]
Parkhurst, J., Darringer, J., Grundmann, B.: From single core to multi-core: preparing for a new exponential. In: Proceedings of the 2006 IEEE/ACM International Conference on Computer-Aided Design, ICCAD'06, pp. 67---72. ACM, New York (2006)
[2]
Sutter, H.: The free lunch is over: a fundamental turn toward concurrency in software. Dr. Dobb's J. 30(3), 202---210 (2005)
[3]
Dig, D., Marrero, J., Ernst, M.D.: Refactoring sequential Java code for concurrency via concurrent libraries. In: Proceedings of the 31st International Conference on Software Engineering, ICSE'09, pp. 397---407. IEEE Computer Society, Washington, DC (2009)
[4]
Aldinucci, M., Torquati, M., Meneghin, M.: Fastflow: efficient parallel streaming applications on multi-core. CORR (2009). arXiv:0909.1187
[5]
Broquedis, F., Diakhaté, F., Thibault, S., Aumage, O., Namyst, R., Wacrenier, P.-A.: Scheduling dynamic openMP applications over multicore architectures. In: Eigenmann, R., Supinski, B. (eds.) OpenMP in a New Era of Parallelism. Lecture Notes in Computer Science, vol. 5004, pp. 170---180. Springer, Berlin (2008)
[6]
Lea, D.: A Java fork/join framework. In: Proceedings of the ACM 2000 Conference on Java Grande, JAVA'00, pp. 36---43. ACM, New York (2000)
[7]
Pheatt, C.: Intel$${}^{\textregistered }$$® threading building blocks. J. Comput. Sci. Coll. 23(4), 298---298 (2008)
[8]
Janjic, V., Brown, C., Mackenzie, K., Hammond, K., Danelutto, M., Aldinucci, M., Garcia, J.D.: RPL: a domain-specific language for designing and implementing parallel C++ applications. In: 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), pp. 288---295. IEEE (2016)
[9]
Chen, F., Yang, H., Chu, W.C.C., Xu, B.: A program transformation framework for multicore software reengineering. In: 2012 12th International Conference on Quality Software, pp. 270---275 (Aug. 2012)
[10]
Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: ACM Sigplan Notices, vol. 40, pp. 213---223. ACM (2005)
[11]
Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball T., Jones R.B. (eds.) Computer Aided Verification (CAV), pp. 419---423. Springer, Berlin (2006).
[12]
Cadar, C., Godefroid, P., Khurshid, S., Pă?să?reanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 1066---1071. ACM (2011)
[13]
Pă?să?reanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transf. 11(4), 339---353 (2009)
[14]
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI 8, 209---224 (2008)
[15]
Barner, S., Eisner, C., Glazberg, Z., Kroening, D., Rabinovitz, I.: ExpliSAT: guiding SAT-based software verification with explicit states. In: Hardware and Software, Verification and Testing, pp. 138---154. Springer (2007)
[16]
Chockler, H., Pidan, D., Ruah, S.: Improving representative computation in ExpliSAT. In: Hardware and Software: Verification and Testing, pp. 359---364. Springer (2013)
[17]
Torquati, M.: Single-producer/single-consumer queues on shared cache multi-core systems. CoRR (2010). arXiv:1012.1824
[18]
The mandelbrot set in C++11. http://solarianprogrammer.com/2013/02/28/mandelbroot-set-cpp-11
[19]
Escape time algorithm. https://en.wikipedia.org/wiki/Mandelbrot_set#Escape_time_algorithm
[20]
Boyer, R.S., Elspas, B., Levitt, K.N.: Select--a formal system for testing and debugging programs by symbolic execution. In: Proceedings of the International Conference on Reliable Software, pp. 234---245
[21]
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385---394 (1976)
[22]
Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 119---135. Springer (2012)
[23]
Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: incremental upgrade checker for C. In: Piterman N., Smolka S.A. (eds.) 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 292---307. Springer, Berlin (2013)
[24]
Schuts, M., Hooman, J., Vaandrager, F.: Refactoring of legacy software using model learning and equivalence checking: an industrial experience report. In: International Conference on Integrated Formal Methods, pp. 311---325. Springer (2016)
[25]
Cranen, S., Groote, J.F., Keiren, J.J., Stappers, F.P., de Vink, E.P., Wesselink, W., Willemse, T.A.: An overview of the mCRL2 toolset and its recent advances. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 199---213. Springer (2013)
[26]
Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Proceedings of the 2006 International Symposium on Software Testing and Analysis, pp. 157---168. ACM (2006)
[27]
Siegel, S.F., Zirkel, T.K.: Automatic formal verification of MPI-based parallel programs. SIGPLAN Not. 46(8), 309---310 (2011)
- Verifying Parallel Code After Refactoring Using Equivalence Checking
Recommendations
Prioritising Refactoring Using Code Bad Smells
ICSTW '11: Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation WorkshopsWe investigated the relationship between six of Fowler et al.'s Code Bad Smells (Duplicated Code, Data Clumps, Switch Statements, Speculative Generality, Message Chains, and Middle Man) and software faults. In this paper we discuss how our results can ...
Refactoring verification using model transformation
IWoR 2016: Proceedings of the 1st International Workshop on Software RefactoringSoftware refactoring is an effective way for dealing with technical debt accumulated in a software system; however, regression risk prevents developers from refactoring their code. Herein, we propose an approach to check the equivalence of source code ...
Verifying verified code
AbstractA recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow-up case study that explores the methodology from the perspective of three research ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2019 Springer Science+Business Media, LLC, part of Springer Nature.
Publisher
Kluwer Academic Publishers
United States
Publication History
Published: 01 February 2019
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 11 Jan 2025
Other Metrics
Citations
Cited By
View all- Jakobs M(2021)PatEC: Pattern-Based Equivalence CheckingModel Checking Software10.1007/978-3-030-84629-9_7(120-139)Online publication date: 12-Jul-2021