Programmer-Centric Memory Consistency Modeling
Lisa Highám, Jalal Kawash, Abhijeet Pareek · Bulletin of the European Association for Theoretical Computer Science · 2013
A framework for modelling memory consistency is presented. The framework is used to specify the operation of a total-store-order write buffer multiprocessor machine. The framework is used again to specify a more abstract “programmer-centric” model that does not refer to the write-buffer architecture. Finally, we prove that the abstract model correctly captures the computations of the operational model. A mutual exclusion algorithm is used to illustrate the advantage of the programmer-centric memory consistency models and the impact on program correctness of instruction reordering resulting from hardware and software optimizations.