nach oben

International Journal of Parallel Programming

Erschienen in:

06.01.2018

Verifying Parallel Code After Refactoring Using Equivalence Checking

verfasst von: Moria Abadi, Sharon Keidar-Barner, Dmitry Pidan, Tatyana Veksler

Erschienen in: International Journal of Parallel Programming | Ausgabe 1/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Compiler Optimization of Accelerator Data Transfers

Nächster Artikel The RePhrase Extended Pattern Set for Data Intensive Parallel Computing

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

The precise classification into these different flavors of symbolic program analysis may be arguable, and in particular the distinction between “symbolic execution” and “symbolic interpretation”, which are sometimes used interchangeably.

We used the ExpliSAT API, which is described in Sect. 2.2.

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)

Sutter, H.: The free lunch is over: a fundamental turn toward concurrency in software. Dr. Dobb’s J. 30(3), 202–210 (2005)

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)

Aldinucci, M., Torquati, M., Meneghin, M.: Fastflow: efficient parallel streaming applications on multi-core. CORR (2009). arXiv:0909.1187

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)CrossRef

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)

Pheatt, C.: Intel\({}^{\textregistered }\) threading building blocks. J. Comput. Sci. Coll. 23(4), 298–298 (2008)

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)

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). https://doi.org/10.1007/11817963_38

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)CrossRef

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)MathSciNetCrossRefMATH

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)CrossRef

Titel: Verifying Parallel Code After Refactoring Using Equivalence Checking
verfasst von: Moria Abadi
Sharon Keidar-Barner
Dmitry Pidan
Tatyana Veksler
Publikationsdatum: 06.01.2018
Verlag: Springer US
Erschienen in: International Journal of Parallel Programming / Ausgabe 1/2019
Print ISSN: 0885-7458
Elektronische ISSN: 1573-7640
DOI: https://doi.org/10.1007/s10766-017-0548-4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2019

The RePhrase Extended Pattern Set for Data Intensive Parallel Computing

HitFlow: A Dataflow Programming Model for Hybrid Distributed- and Shared-Memory Systems

Multi-device Controllers: A Library to Simplify Parallel Heterogeneous Programming

Efficient Dynamic Pinning of Parallelized Applications by Distributed Reinforcement Learning

Compiler Optimization of Accelerator Data Transfers

Parallel SIMD CPU and GPU Implementations of Berlekamp–Massey Algorithm and Its Error Correction Application