Property-Driven Fence Insertion using Reorder Bounded Model Checking

Journal article

Modern architectures provide weaker memory consistency guarantees than sequential consistency. These weaker guarantees allow programs to exhibit behaviours where the program statements appear to have executed out of program order. Fortunately, modern architectures provide memory barriers (fences) to enforce the program order between a pair of statements if needed. Due to the intricate semantics of weak memory models, the placement of fences is challenging even for experienced programmers. Too...

Expand abstract

Authors: Joshi, S; Kroening, D

• Publication status: Not published
• Peer review status: Reviewed (other)
• Language: English