publication . Article . 2018

MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models

Allan Blanchard; Nikolai Kosmatov; Frédéric Loulergue;
Open Access English
  • Published: 01 Sep 2018
  • Publisher: HAL CCSD
  • Country: France
Abstract
International audience; With the wide expansion of multiprocessor architectures, the analysis and reasoning for programs under weak memory models has become an important concern. This work presents MMFilter, an original constraint solver for generating program behaviors respecting a particular memory model. It is implemented in Prolog using CHR (Constraint Handling Rules). The CHR formalism provides a convenient generic solution for specifying memory models. It benefits from the existing optimized implementations of CHR and can be easily extended to new models. We present MMFilter design, illustrate the encoding of memory model constraints in CHR and discuss the...
Persistent Identifiers
Subjects
free text keywords: constraint solving, constraint handling rules, logic programming, weak memory models, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], weak memory models, constraint solving, logic programming, constraint handling rules, Computer Networks and Communications, Software, Prolog, computer.programming_language, computer, Logic programming, Parallel computing, Memory model, Encoding (memory), Computer science, Solver, Multiprocessing, Constraint Handling Rules, Constraint satisfaction problem
Funded by
EC| VESSEDIA
Project
VESSEDIA
VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS
  • Funder: European Commission (EC)
  • Project Code: 731453
  • Funding stream: H2020 | RIA
Validated by funder
30 references, page 1 of 2

[1] S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer Society, 29(12):66{76, 1996. doi: 10.1109/2. 546611.

[2] J. Alglave. A Shared Memory Poetics. PhD thesis, Universite Paris VII - Denis Diderot, 2010. URL http://www0.cs.ucl.ac.uk/staff/j. alglave/these.pdf.

[3] J. Alglave and L. Maranget. The diy7 tool suite. http://diy.inria.fr/, 2011 { 2017.

[4] J. Alglave, A. C. J. Fox, S. Ishtiaq, M. O. Myreen, S. Sarkar, P. Sewell, and F. Z. Nardelli. The semantics of Power and ARM multiprocessor machine code. In Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, DAMP 2009, Savannah, GA, USA, January 20, 2009, pages 13{24. ACM, 2009. doi: 10.1145/1481839.1481842.

[5] J. Alglave, D. Kroening, V. Nimal, and D. Poetzl. Don't sit on the fence { a static analysis approach to automatic fence insertion. In Computer Aided Veri cation - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18- 22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 508{524. Springer, 2014. doi: 10.1007/978-3-319-08867-9 33.

[6] J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1{7:74, 2014. doi: 10.1145/2627752. [OpenAIRE]

[7] M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 55{66. ACM, 2011. doi: 10.1145/ 1926385.1926394.

[8] H. Boehm and S. V. Adve. Foundations of the C++ concurrency memory model. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, Tucson, AZ, USA, June 7-13, 2008, pages 68{78. ACM, 2008. doi: 10.1145/1375581.1375591.

[9] G. Boudol and G. Petri. Relaxed memory models: An operational approach. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 392{403. ACM, 2009. doi: 10.1145/1480881.1480930. [OpenAIRE]

[10] J. F. Cantin, M. H. Lipasti, and J. E. Smith. The complexity of verifying memory coherence and consistency. IEEE Trans. Parallel Distrib. Syst., 16 (7):663{671, 2005. doi: 10.1109/TPDS.2005.86.

TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in computer Science, pages 212{227. Springer, 2009. doi: 10.1007/978-3-642-03359-9 16.

[12] E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Program veri cation using Constraint Handling Rules and array constraint generalizations. In Second International Workshop on Veri cation and Program Transformation, VPT 2014, part of the Vienna Summer of Logic 2014 and co-located with the 26th International Conference on Computer Aided Veri cation, CAV 2014, July 17-18, 2014, Vienna, Austria, volume 28 of EPiC Series in Computing, pages 3{18. EasyChair. URL http://www.easychair.org/publications/?page=735874241.

[13] G. J. Duck, P. J. Stuckey, M. J. G. de la Banda, and C. Holzbaur. The re ned operational semantics of Constraint Handling Rules. In Logic Programming, 20th International Conference, ICLP 2004, SaintMalo, France, September 6-10, 2004, Proceedings, volume 3132 of Lecture Notes in Computer Science, pages 90{104. Springer, 2004. doi: 10.1007/978-3-540-27775-0 7.

[14] T. Fruhwirth. Constraint Handling Rules. Cambridge University Press, 2009. ISBN 9780521877763.

[15] T. Fruhwirth. Theory and practice of Constraint Handling Rules. The Journal of Logic Programming, 37:95 { 138, 1998. doi: 10.1016/S0743-1066(98) 10005-5.

30 references, page 1 of 2
Any information missing or wrong?Report an Issue