A Program Logic for Reasoning About C11 Programs With Release-Sequences

Mengda He

doi:10.1109/ACCESS.2020.3024681

Return

A Program Logic for Reasoning About C11 Programs With Release-Sequences

2020-01-01

Mengda He

Shengchao Qin *

Zhiwu Xu

DOI：10.1109/ACCESS.2020.3024681

Original

Save

View PDF

Abstract

En 中文

With the popularity of weak/relaxed memory models widely used in modern hardware architectures, the C11 standard introduced a language level weak memory model, A.K.A the C11 memory model, that allows C/C++ programs to exploit the optimisation provided by the hardware platform in memory ordering and gain benefits in efficiency. On the other hand, with the weakened memory ordering allowed, more program behaviours are introduced, among which some are counterintuitive and make it even more challenging for programmers to understand or to formally reason about C11 multithread programs. To support the formal verification of the C11 weak memory programs, several program logics, e.g. RSL, GPS, FSL, and GPS+, have been developed during the last few years. However, due to the complexity of the weakened memory model, some intricate C11 features still cannot be handled in these logics. A notable example is the lack of supporting to the reasoning about a highly flexible C11 synchronisation mechanism, the release-sequence. Recently, the FSL++ logic proposed by Doko and Vafeiadis moves one step forward to address this problem, but FSL++ only considers the scenarios with atomic update operations in a release-sequence. In this article, we propose a new program logic, GPS++, that supports the reasoning about C11 programs with fully featured release-sequences. We also introduce fractional read permissions to GPS++, which are essential to the reasoning about a large number of real-world concurrent programs. GPS++ is a successor of our previous program logic GPS+, but it comes with much finer control over the resource transmission with the newly introduced restricted-shareable assertions and an enhanced protocol system. A more sophisticated resource model is devised to support the soundness proof of our new program logic. We also demonstrate GPS++ in action by verifying C11 programs with release-sequences that could not be handled by existing program logics.

Keywords:

Cognition

Synchronization

Hardware

Global Positioning System

Instruction sets

Load modeling

Radio frequency

Program logic

formal semantics

program verification

C11 weak memory model

release-sequence

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.