A Load-Buffer Semantics for Total Store Ordering

We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixe...

Full description

Bibliographic Details
Main Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2018-01-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/3109/pdf