Algebraic Semantics for C++11 Memory Model

Lili Xiao; Huibiao Zhu; Mengda He; Shengchao Qin

doi:10.1109/COMPSAC54236.2022.00240

Algebraic Semantics for C++11 Memory Model

Lili Xiao, Huibiao Zhu, Mengda He, Shengchao Qin

Centre for Digital Innovation

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

Abstract

The C++11 standard introduced a language level weak memory model (i.e., the C++11 memory model) to improve the performance of the execution of C/C++ programs. Algebra is well-suited for direct use by engineers in symbolic calculation of parameters. It is a challenge to investigate the algebraic semantics for the C++11 memory model. Inspired by the promising semantics, in this paper, we explore the algebraic laws for the C++11 memory model, including a set of sequential and parallel expansion laws. We introduce the concept of guarded choice, and every program under the C++11 memory model can be converted into the head normal form of guarded choice. In addition, the proposed algebraic laws are implemented in the rewriting engine Maude.

Original language	English
Title of host publication	2022 IEEE 46th Annual Computers, Software, and Applications Conference
Subtitle of host publication	Proceedings
Editors	Hong Va Leong, Sahra Sedigh Sarvestani, Yuuichi Teranishi, Alfredo Cuzzocrea, Hiroki Kashiwazaki, Dave Towey, Ji-Jiang Yang, Hossain Shahriar
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	1513-1518
Number of pages	6
ISBN (Electronic)	9781665488105
DOIs	https://doi.org/10.1109/COMPSAC54236.2022.00240
Publication status	Published - 10 Aug 2022
Event	46th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2022 - Virtual, Online, United States Duration: 27 Jun 2022 → 1 Jul 2022

Publication series

Name	Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022

Conference

Conference	46th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2022
Abbreviated title	COMPSAC
Country/Territory	United States
City	Virtual, Online
Period	27/06/22 → 1/07/22

Bibliographical note

Funding Information:
In the future, we will continue our work on the C++11 memory model. We would like to investigate the semantics linking theories of this memory model. Acknowledgements. This work was partly supported by the National Key Research and Development Program of China (Grant No. 2018YFB2101300), the National Natural Science Foundation of China (Grant Nos. 61872145, 62032024), Shanghai Trusted Industry Internet Software Collaborative Innovation Center, and the Dean’s Fund of Shanghai Key Laboratory of Trustworthy Computing (East China Normal University).

Publisher Copyright:
© 2022 IEEE.

Access to Document

10.1109/COMPSAC54236.2022.00240Licence: Unspecified

Cite this

Xiao, L., Zhu, H., He, M., & Qin, S. (2022). Algebraic Semantics for C++11 Memory Model. In H. Va Leong, S. S. Sarvestani, Y. Teranishi, A. Cuzzocrea, H. Kashiwazaki, D. Towey, J.-J. Yang, & H. Shahriar (Eds.), 2022 IEEE 46th Annual Computers, Software, and Applications Conference: Proceedings (pp. 1513-1518). (Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/COMPSAC54236.2022.00240

Xiao, Lili ; Zhu, Huibiao ; He, Mengda et al. / Algebraic Semantics for C++11 Memory Model. 2022 IEEE 46th Annual Computers, Software, and Applications Conference: Proceedings . editor / Hong Va Leong ; Sahra Sedigh Sarvestani ; Yuuichi Teranishi ; Alfredo Cuzzocrea ; Hiroki Kashiwazaki ; Dave Towey ; Ji-Jiang Yang ; Hossain Shahriar. Institute of Electrical and Electronics Engineers Inc., 2022. pp. 1513-1518 (Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022).

@inproceedings{161da764d89f4028b2ad0d78c07b57a2,

title = "Algebraic Semantics for C++11 Memory Model",

abstract = "The C++11 standard introduced a language level weak memory model (i.e., the C++11 memory model) to improve the performance of the execution of C/C++ programs. Algebra is well-suited for direct use by engineers in symbolic calculation of parameters. It is a challenge to investigate the algebraic semantics for the C++11 memory model. Inspired by the promising semantics, in this paper, we explore the algebraic laws for the C++11 memory model, including a set of sequential and parallel expansion laws. We introduce the concept of guarded choice, and every program under the C++11 memory model can be converted into the head normal form of guarded choice. In addition, the proposed algebraic laws are implemented in the rewriting engine Maude.",

author = "Lili Xiao and Huibiao Zhu and Mengda He and Shengchao Qin",

note = "Funding Information: In the future, we will continue our work on the C++11 memory model. We would like to investigate the semantics linking theories of this memory model. Acknowledgements. This work was partly supported by the National Key Research and Development Program of China (Grant No. 2018YFB2101300), the National Natural Science Foundation of China (Grant Nos. 61872145, 62032024), Shanghai Trusted Industry Internet Software Collaborative Innovation Center, and the Dean{\textquoteright}s Fund of Shanghai Key Laboratory of Trustworthy Computing (East China Normal University). Publisher Copyright: {\textcopyright} 2022 IEEE.; 46th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2022, COMPSAC ; Conference date: 27-06-2022 Through 01-07-2022",

year = "2022",

month = aug,

day = "10",

doi = "10.1109/COMPSAC54236.2022.00240",

language = "English",

series = "Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "1513--1518",

editor = "{Va Leong}, Hong and Sarvestani, {Sahra Sedigh} and Yuuichi Teranishi and Alfredo Cuzzocrea and Hiroki Kashiwazaki and Dave Towey and Ji-Jiang Yang and Hossain Shahriar",

booktitle = "2022 IEEE 46th Annual Computers, Software, and Applications Conference",

address = "United States",

}

Xiao, L, Zhu, H, He, M & Qin, S 2022, Algebraic Semantics for C++11 Memory Model. in H Va Leong, SS Sarvestani, Y Teranishi, A Cuzzocrea, H Kashiwazaki, D Towey, J-J Yang & H Shahriar (eds), 2022 IEEE 46th Annual Computers, Software, and Applications Conference: Proceedings . Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022, Institute of Electrical and Electronics Engineers Inc., pp. 1513-1518, 46th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2022, Virtual, Online, United States, 27/06/22. https://doi.org/10.1109/COMPSAC54236.2022.00240

Algebraic Semantics for C++11 Memory Model. / Xiao, Lili; Zhu, Huibiao; He, Mengda et al.
2022 IEEE 46th Annual Computers, Software, and Applications Conference: Proceedings . ed. / Hong Va Leong; Sahra Sedigh Sarvestani; Yuuichi Teranishi; Alfredo Cuzzocrea; Hiroki Kashiwazaki; Dave Towey; Ji-Jiang Yang; Hossain Shahriar. Institute of Electrical and Electronics Engineers Inc., 2022. p. 1513-1518 (Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022).

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

TY - GEN

T1 - Algebraic Semantics for C++11 Memory Model

AU - Xiao, Lili

AU - Zhu, Huibiao

AU - He, Mengda

AU - Qin, Shengchao

N1 - Funding Information: In the future, we will continue our work on the C++11 memory model. We would like to investigate the semantics linking theories of this memory model. Acknowledgements. This work was partly supported by the National Key Research and Development Program of China (Grant No. 2018YFB2101300), the National Natural Science Foundation of China (Grant Nos. 61872145, 62032024), Shanghai Trusted Industry Internet Software Collaborative Innovation Center, and the Dean’s Fund of Shanghai Key Laboratory of Trustworthy Computing (East China Normal University). Publisher Copyright: © 2022 IEEE.

PY - 2022/8/10

Y1 - 2022/8/10

N2 - The C++11 standard introduced a language level weak memory model (i.e., the C++11 memory model) to improve the performance of the execution of C/C++ programs. Algebra is well-suited for direct use by engineers in symbolic calculation of parameters. It is a challenge to investigate the algebraic semantics for the C++11 memory model. Inspired by the promising semantics, in this paper, we explore the algebraic laws for the C++11 memory model, including a set of sequential and parallel expansion laws. We introduce the concept of guarded choice, and every program under the C++11 memory model can be converted into the head normal form of guarded choice. In addition, the proposed algebraic laws are implemented in the rewriting engine Maude.

AB - The C++11 standard introduced a language level weak memory model (i.e., the C++11 memory model) to improve the performance of the execution of C/C++ programs. Algebra is well-suited for direct use by engineers in symbolic calculation of parameters. It is a challenge to investigate the algebraic semantics for the C++11 memory model. Inspired by the promising semantics, in this paper, we explore the algebraic laws for the C++11 memory model, including a set of sequential and parallel expansion laws. We introduce the concept of guarded choice, and every program under the C++11 memory model can be converted into the head normal form of guarded choice. In addition, the proposed algebraic laws are implemented in the rewriting engine Maude.

UR - http://www.scopus.com/inward/record.url?scp=85136917721&partnerID=8YFLogxK

U2 - 10.1109/COMPSAC54236.2022.00240

DO - 10.1109/COMPSAC54236.2022.00240

M3 - Conference contribution

AN - SCOPUS:85136917721

T3 - Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022

SP - 1513

EP - 1518

BT - 2022 IEEE 46th Annual Computers, Software, and Applications Conference

A2 - Va Leong, Hong

A2 - Sarvestani, Sahra Sedigh

A2 - Teranishi, Yuuichi

A2 - Cuzzocrea, Alfredo

A2 - Kashiwazaki, Hiroki

A2 - Towey, Dave

A2 - Yang, Ji-Jiang

A2 - Shahriar, Hossain

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 46th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2022

Y2 - 27 June 2022 through 1 July 2022

ER -

Xiao L, Zhu H, He M, Qin S. Algebraic Semantics for C++11 Memory Model. In Va Leong H, Sarvestani SS, Teranishi Y, Cuzzocrea A, Kashiwazaki H, Towey D, Yang JJ, Shahriar H, editors, 2022 IEEE 46th Annual Computers, Software, and Applications Conference: Proceedings . Institute of Electrical and Electronics Engineers Inc. 2022. p. 1513-1518. (Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022). doi: 10.1109/COMPSAC54236.2022.00240

Algebraic Semantics for C++11 Memory Model

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this