Towards a program logic for C11 release-sequences

Mengda He, Shengchao Qin, Joao Ferreira

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

By accepting order weakening for memory operations, the C11 memory model allows C/C++ programs to take advantage of modern hardware architectures, where weak/relaxed memory models are now the norm. However, the weakened C11 memory model introduces many complex and counterintuitive behaviours, rendering it more difficult for people to understand or reason about concurrent C11 programs. Several program logics (RSL, GPS, FSL, GPS+) have been proposed over the last few years to support formal reasoning for C11 programs, but each of them deals with only a specific subset of C11 programs, mainly due to the high complexity of the weakened memory model. Notably none of these program logics supports the reasoning of release-sequences-a highly flexible synchronisation mechanism in C11. Very recently, Doko and Vafeiadis propose a way in their FSL++ logic to reason about C11 programs using release-sequences, but their solution is restricted to those scenarios where only atomic update operations are between the release head and the receiver. In this paper we propose a new program logic that offers full support for reasoning about C11 programs using release-sequences. Our proposed logic is built on top of our previous program logic GPS+, but with much finer control over the resource transmission by introducing restricted-shareable assertions and an enhanced protocol system. We also illustrate our approach by verifying release-sequence programs that existing logics would not be able to.

Original languageEnglish
Title of host publicationProceedings - 2018 12th International Symposium on Theoretical Aspects of Software Engineering, TASE 2018
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781538673058
DOIs
Publication statusPublished - 4 Dec 2018
Event12th International Symposium on Theoretical Aspects of Software Engineering - Guangzhou, China
Duration: 29 Aug 201831 Aug 2018
Conference number: 12

Publication series

NameProceedings - 2018 12th International Symposium on Theoretical Aspects of Software Engineering, TASE 2018
Volume2018-January

Conference

Conference12th International Symposium on Theoretical Aspects of Software Engineering
Abbreviated titleTASE 2018
CountryChina
CityGuangzhou
Period29/08/1831/08/18

Fingerprint Dive into the research topics of 'Towards a program logic for C11 release-sequences'. Together they form a unique fingerprint.

  • Cite this

    He, M., Qin, S., & Ferreira, J. (2018). Towards a program logic for C11 release-sequences. In Proceedings - 2018 12th International Symposium on Theoretical Aspects of Software Engineering, TASE 2018 [8560730] (Proceedings - 2018 12th International Symposium on Theoretical Aspects of Software Engineering, TASE 2018; Vol. 2018-January). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/TASE.2018.00012