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

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

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

Full description

Bibliographic Details
Main Authors: Mengda He, Shengchao Qin, Zhiwu Xu
Format: Article
Language:English
Published: IEEE 2020-01-01
Series:IEEE Access
Subjects:
Program logic
formal semantics
program verification
C11 weak memory model
release-sequence
Online Access:https://ieeexplore.ieee.org/document/9200342/

Internet

https://ieeexplore.ieee.org/document/9200342/

Similar Items