Information-flow models for shared memory with an application to the powerPC architecture, IEEE Transactions on Parallel and Distributed Systems, vol.14, issue.5, 2003. ,
DOI : 10.1109/TPDS.2003.1199067
The semantics of power and ARM multiprocessor machine code, Proceedings of the 4th workshop on Declarative aspects of multicore programming, DAMP '09, 2009. ,
DOI : 10.1145/1481839.1481842
Fences in Weak Memory Models, International Conference on Computer Aided Verification, 2010. ,
DOI : 10.1007/978-3-642-14295-6_25
URL : https://hal.archives-ouvertes.fr/hal-01100859
Litmus: Running tests against hardware A formal specification of the PowerPC shared memory architecture Minisat -a SAT solver with conflict-clause minimization Memory consistency models for shared-memory multiprocessors, International Conference on Tools and Algorithms for the Construction and Analysis of Systems International Conference on Theory and Applications of Satisfiability TestingInt02] Intel. A formal specification of Intel Itanium processor family memory ordering, 1995. ,
Lem: A lightweight tool for heavyweight semantics Rough Diamond " section), Proc. ITP: Interactive Theorem Proving, pp.363-369, 2011. ,
Storage in the PowerPC, IEEE Micro, vol.15, 1995. ,
Understanding POWER multiprocessors [Sup] An axiomatic memory model for Power multiprocessors ? supplementary material, Programming Language Design and Implementation, 2011. ,
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT, Correct Hardware Design and Verification Methods, 2003. ,
DOI : 10.1007/978-3-540-39724-3_9