Property-driven fence insertion using reorder bounded model checking

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

Full description

Bibliographic Details
Main Authors: Joshi, S, Kroening, D
Other Authors: Bjørner, N
Format: Conference item
Published: Springer 2015