Top

Published in:

2017 | OriginalPaper | Chapter

Modeling and Verifying Multi-core Programs

Authors : Nan Zhang, Zhenhua Duan, Cong Tian, Hongwei Du, Kai Yang

Published in: Combinatorial Optimization and Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

To model and verify multi-core programs, this paper formalizes an operational semantics for Cylinder Computation Model (CCM). Further, the advantages of CCM over other concurrency models are highlighted. Moreover, the principle of programming with CCM is presented. In addition, a unified model checking approach in code level to verifying CCM programs is briefly demonstrated. Finally, an example is given to show how multi-core programs with CCM can be realized and verified.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Longest Previous Non-overlapping Factors Table Computation

next chapter Planar Vertex-Disjoint Cycle Packing: New Structures and Improved Kernel

Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14(1), 25–59 (1987)CrossRef

Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 387–393 (2016)

Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), San Diego, CA, USA (2008)

Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49–66. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_4 CrossRef

Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)

Fischer, B., Inverso, O., Parlato, G.: CSeq: a concurrency pre-processor for sequential C verification tools. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering, pp. 710–713. IEEE Press (2013)

Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming, Elsevier, Waltham (2008). ISBN 978-0-12-370591-4

Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 26(1), 100–106 (1983)CrossRef

Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3–4), 213–254 (2007)CrossRef

10.

King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)CrossRefMATHMathSciNet

11.

Koutney, M., Pietkiewicz-Koutney, M.: Synthesis of petri nets with localities. Sci. Ann. Comput. Sci. 19, 1–23 (2009)MathSciNet

12.

Liang, Y., Li, S., Zhang, H., et al.: Timing-sequence testing of parallel programs. J. Comput. Sci. Technol. 15(1), 84–95 (2000)CrossRefMATHMathSciNet

13.

Milner, R.: A Calculus of Communicating Systems, vol. 92. LNCS, Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3 MATH

14.

Navabpour, S., Joshi, Y., Wu, W., Berkovich, S., Medhat, R., Bonakdarpour, B., Fischmeister, S.: RiTHM: a tool for enabling time-triggered runtime verification for c programs. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 603–606. ACM (2013)

15.

Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: Verifying concurrent programs by memory unwinding. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 551–565. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_52

16.

Wang, M., Tian, C., Duan, Z.: Full regular temporal property verification as dynamic program execution. In: Proceedings of ICSE 2017, pp. 226–228. IEEE Press (2017)

17.

Yang, C.S.D., Pollock, L.L.: All-uses testing of shared memory parallel programs. Softw. Test. Verification Reliab. 13(1), 3–24 (2003)CrossRef

18.

Yang, X., Duan, Z.: Operational semantics of Framed Tempura. J. Logic Algebraic Program. 78(1), 22–51 (2008)CrossRefMATHMathSciNet

19.

Yang, K., Duan, Z., Tian, C., Zhang, N.: A compiler for MSVL and its applications. Theoret. Comput. Sci. (2017). https://doi.org/10.1016/j.tcs.2017.07.032

20.

Zhang, N., Duan, Z., Tian, C.: A complete axiom system for propositional projection temporal logic with cylinder computation model. Theoret. Comput. Sci. 609, 639–657 (2016)CrossRefMATHMathSciNet

Title: Modeling and Verifying Multi-core Programs
Authors: Nan Zhang
Zhenhua Duan
Cong Tian
Hongwei Du
Kai Yang
Publisher: Springer International Publishing
Book: Combinatorial Optimization and Applications
Print ISBN: 978-3-319-71146-1

Electronic ISBN: 978-3-319-71147-8

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-71147-8_36

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner