Modeling and verifying multi-core programs

Nan Zhang; Zhenhua Duan; Cong Tian; Hongwei Du; Kai Yang

doi:10.1007/978-3-319-71147-8_36

Modeling and verifying multi-core programs

Nan Zhang
, Zhenhua Duan^*
, Cong Tian
, Hongwei Du
, Kai Yang

^*Corresponding author for this work

Xidian University
State Key Laboratory of Integrated Services Networks
Harbin Institute of Technology Shenzhen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings
Editors	Xiaofeng Gao, Hongwei Du, Meng Han
Publisher	Springer Verlag
Pages	492-500
Number of pages	9
ISBN (Print)	9783319711461
DOIs	https://doi.org/10.1007/978-3-319-71147-8_36
State	Published - 2017
Externally published	Yes
Event	11th International Conference on Combinatorial Optimization and Applications, COCOA 2017 - Shanghai, China Duration: 16 Dec 2017 → 18 Dec 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10628 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Combinatorial Optimization and Applications, COCOA 2017
Country/Territory	China
City	Shanghai
Period	16/12/17 → 18/12/17

Keywords

Formal method
Multi-core
Operational semantics
Parallel

Access to Document

10.1007/978-3-319-71147-8_36

Cite this

Zhang, N., Duan, Z., Tian, C., Du, H., & Yang, K. (2017). Modeling and verifying multi-core programs. In X. Gao, H. Du, & M. Han (Eds.), Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings (pp. 492-500). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10628 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-71147-8_36

Zhang, Nan ; Duan, Zhenhua ; Tian, Cong et al. / Modeling and verifying multi-core programs. Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings. editor / Xiaofeng Gao ; Hongwei Du ; Meng Han. Springer Verlag, 2017. pp. 492-500 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{98e2828e07f84dcbb29467e59ea22988,

title = "Modeling and verifying multi-core programs",

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.",

keywords = "Formal method, Multi-core, Operational semantics, Parallel",

author = "Nan Zhang and Zhenhua Duan and Cong Tian and Hongwei Du and Kai Yang",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 11th International Conference on Combinatorial Optimization and Applications, COCOA 2017 ; Conference date: 16-12-2017 Through 18-12-2017",

year = "2017",

doi = "10.1007/978-3-319-71147-8\_36",

language = "英语",

isbn = "9783319711461",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "492--500",

editor = "Xiaofeng Gao and Hongwei Du and Meng Han",

booktitle = "Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings",

address = "德国",

}

Zhang, N, Duan, Z, Tian, C, Du, H & Yang, K 2017, Modeling and verifying multi-core programs. in X Gao, H Du & M Han (eds), Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10628 LNCS, Springer Verlag, pp. 492-500, 11th International Conference on Combinatorial Optimization and Applications, COCOA 2017, Shanghai, China, 16/12/17. https://doi.org/10.1007/978-3-319-71147-8_36

Modeling and verifying multi-core programs. / Zhang, Nan; Duan, Zhenhua; Tian, Cong et al.
Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings. ed. / Xiaofeng Gao; Hongwei Du; Meng Han. Springer Verlag, 2017. p. 492-500 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10628 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Modeling and verifying multi-core programs

AU - Zhang, Nan

AU - Duan, Zhenhua

AU - Tian, Cong

AU - Du, Hongwei

AU - Yang, Kai

N1 - Publisher Copyright: © Springer International Publishing AG 2017.

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - Formal method

KW - Multi-core

KW - Operational semantics

KW - Parallel

UR - https://www.scopus.com/pages/publications/85038210440

U2 - 10.1007/978-3-319-71147-8_36

DO - 10.1007/978-3-319-71147-8_36

M3 - 会议稿件

AN - SCOPUS:85038210440

SN - 9783319711461

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 492

EP - 500

BT - Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings

A2 - Gao, Xiaofeng

A2 - Du, Hongwei

A2 - Han, Meng

PB - Springer Verlag

T2 - 11th International Conference on Combinatorial Optimization and Applications, COCOA 2017

Y2 - 16 December 2017 through 18 December 2017

ER -

Zhang N, Duan Z, Tian C, Du H, Yang K. Modeling and verifying multi-core programs. In Gao X, Du H, Han M, editors, Combinatorial Optimization and Applications - 11th International Conference, COCOA 2017, Proceedings. Springer Verlag. 2017. p. 492-500. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-71147-8_36

Modeling and verifying multi-core programs

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this