Диссертация (1149932), страница 25
Текст из файла (страница 25)
Это позволит свести дальнейшие доказательства корректности компиляциииз обещающей модели к доказательству корректности компиляции в обобщенную аксиоматическую модель, что сводится к рассуждениям об ацикличности ивложенности путей на графах. Кроме того, актуальной является задача разработки эффективной программной логики на базе логики многопоточного разделения(concurrent separation logic) для операционного аналога модели памяти C/С++11 иобещающей модели памяти.
Такая логика позволит формально доказывать в рамках моделей сложные свойства программ, такие как соответствие спецификации.127Список сокращений и условных обозначенийCASC/C++11 MMDRJMMLBMMMPOOTAOpC11 MMPOPPromise MMQSBRRCURMWSBSCSEСтр.compare-and-set, инструкция атомарного сравнения и за- 51писи, частный случай RMWC/C++11 memory model, модель памяти C/C++1124data race, гонка по данным40Java memory model, модель памяти Java21load buffering, шаблон “буферизация чтения”19memory model, модель памяти15message passing, шаблон “передача сообщения”13out-of-thin-air values, “значения из воздуха”12операционная модель памяти для C/C++11, предложен- 33ная диссертантомpartial order propagation, подсистема памяти модели 73ARMv8 POP, основанная на частичных порядкахобещающая модель памяти69quiescent state-based reclamation, стратегия “освобожде- 62ние памяти в момент затишья”read-copy-update, структура данных, поддерживающая 62неблокирующую синхронизацию для ситуации “один писатель много читателей”read-modify-write, атомарное чтение-запись24store buffering, шаблон “буферизация записи”40sequential consistency, модель последовательной конси- 12стентностиspeculative execution, шаблон “спекулятивное исполне- 37ние”128Список литературы1.
Lamport, L. How to Make a Multiprocessor Computer That Correctly ExecutesMultiprocess Programs / L. Lamport // IEEE Trans. Computers. — 1979. —Vol. 28, no. 9. — P. 690–691.2. Adve, S. V. Shared Memory Consistency Models: A Tutorial / S. V. Adve,K. Gharachorloo // IEEE Computer. — 1996. — Vol. 29, no. 12. — P. 66–76.3. Manson, J. The Java Memory Model / J. Manson, W. Pugh, S.
V. Adve // Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12–14,2005. — ACM, 2005. — P. 378–391.4. Batty, M. Mathematizing C++ Concurrency / M. Batty, S. Owens, S. Sarkar,P. Sewell, T. Weber // Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA,January 26–28, 2011. — ACM, 2011. — P. 55–66.5.
Boehm, H.-J. Outlawing Ghosts: Avoiding Out-of-thin-air Results / H.-J. Boehm,B. Demsky // MSPC 2014. — ACM, 2014. — P. 7:1–7:6.6. Alglave, J. Herding Cats: Modelling, Simulation, Testing, and Data Mining forWeak Memory / J. Alglave, L. Maranget, M. Tautschnig // ACM Trans. Program.Lang. Syst. — 2014. — Vol. 36, no.
2. — P. 7:1–7:74.7. Sewell, P. x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors / P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, M. O. Myreen //Commun. ACM. — 2010. — Vol. 53, no. 7. — P. 89–97.8. Owens, S. A Better x86 Memory Model: x86-TSO / S.
Owens, S. Sarkar,P. Sewell // Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. —2009. — P. 391–407.9. Flur, S. Modelling the ARMv8 Architecture, Operationally: Concurrency andISA / S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin, L. Maranget, W. Deacon,129P. Sewell // Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL,USA, January 20–22, 2016. — ACM, 2016.
— P. 608–621.10. Pulte, C. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8 / C. Pulte, S. Flur, W. Deacon, J. French, S. Sarkar,P. Sewell // POPL 2018. — 2018.11. Kang, J. A Promising Semantics for Relaxed-Memory Concurrency / J. Kang,C.-K. Hur, O.
Lahav, V. Vafeiadis, D. Dreyer // Proceedings of the 44th ACMSIGPLAN Symposium on Principles of Programming Languages, POPL 2017,Paris, France, January 18–20, 2017. — ACM, 2017.12. Keller, R. M. Formal Verification of Parallel Programs / R. M. Keller // Commun.ACM. — 1976. — Vol. 19, no. 7. — P. 371–384.13. Felleisen, M. The Revised Report on the Syntactic Theories of Sequential Controland State / M. Felleisen, R. Hieb // Theor. Comput. Sci. — 1992.
— Vol. 103,no. 2. — P. 235–271.14. Lynch, N. A. Forward and Backward Simulations: I. Untimed Systems /N. A. Lynch, F. W. Vaandrager // Inf. Comput. — 1995. — Vol. 121, no. 2.— P. 214–233.15. Lynch, N. A. Forward and Backward Simulations, II: Timing-Based Systems /N. A. Lynch, F. W. Vaandrager // Inf. Comput. — 1996. — Vol. 128, no. 1.
—P. 1–25.16. Flatt, M. — Reference: Racket. PLT-TR-2010-1 [Электронный ресурс]. — URL:https://racket-lang.org/tr1/ (дата обращения: 29.12.2017).17. Язык программирования Racket [Электронный ресурс]. — URL: http://racket-lang.org/ (дата обращения: 29.12.2017).18. Felleisen, M. Semantics Engineering with PLT Redex / M. Felleisen, R. B.
Findler,M. Flatt. — MIT Press, 2009.19. Run your research: on the effectiveness of lightweight mechanization / C. Klein,J. Clements, C. Dimoulas, C. Eastlund, M. Felleisen, M. Flatt, J. A. McCarthy,130J. Rafkind, S. Tobin-Hochstadt, R. B. Findler // Proceedings of the 39th ACMSIGPLAN Symposium on Principles of Programming Languages, POPL 2017,Philadelphia, Pennsylvania, USA, January, 2012. — ACM, 2012. — P. 285–296.20. Lahav, O. Explaining Relaxed Memory Models with Program Transformations /O. Lahav, V.
Vafeiadis // FM 2016: Formal Methods — 21st International Symposium, Limassol, Cyprus, November 9–11, 2016, Proceedings. — Springer, 2016.21. Подкопаев, А. О корректности компиляции подмножествa обещающей модели памяти в аксиоматическую модель ARMv8.3 / А. Подкопаев, О. Лахав,В. Вафеядис // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации.
Управление. — 2017. — Т. 10, № 4. — С. 51–69.22. Подкопаев, А. Обещающая компиляция в ARMv8.3 / А. Подкопаев, О. Лахав,В. Вафеядис // Труды ИСП РАН. — 2017. — Т. 29, № 5. — С. 149–164.23. Podkopaev, A. Promising Compilation to ARMv8 POP / A. Podkopaev, O. Lahav, V. Vafeiadis // Leibniz International Proceedings in Informatics (LIPIcs),31st European Conference on Object-Oriented Programming (ECOOP 2017) /Ed. by Peter Müller. — Vol. 74. — Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017.
— P. 22:1–22:28. — URL: http://drops.dagstuhl.de/opus/volltexte/2017/7266.24. Подкопаев, А. Обещающая компиляция в ARMv8 / А. Подкопаев, О. Лахав,В. Вафеядис // Труды конференции, Языки программирования и компиляторы / Под ред. Д.В. Дубров. — Труды конференции. — Ростов-на-Дону,Россия: 2017.25. Podkopaev, A. Operational Aspects of C/C++ Concurrency / A. Podkopaev,I.
Sergey, A. Nanevski // CoRR. — 2016. — Vol. abs/1606.01400. — URL:http://arxiv.org/abs/1606.01400.26. Kshemkalyani, A. D. Distributed computing: principles, algorithms, and systems /A. D. Kshemkalyani, M. Singhal. — Cambridge University Press, 2011.27. Hennessy, J. L. Computer Architecture — A Quantitative Approach (5. ed.) /J.
L. Hennessy, D. A. Patterson. — Morgan Kaufmann, 2012.13128. Aho, A. V. Compilers: Principles, Techniques, and Tools / A. V. Aho, R. Sethi,J. D. Ullman. Addison-Wesley series in computer science / World student seriesedition. — Addison-Wesley, 1986.29. Muchnick, S. S.
Advanced Compiler Design and Implementation / S. S. Muchnick. — Morgan Kaufmann, 1997.30. ISO/IEC 9899:2011. Programming language C. — 2011.31. ISO/IEC 14882:2011. Programming language C++. — 2011.32. Unger, S. H. Hazards, Critical Races, and Metastability / S. H. Unger // IEEETrans. Computers. — 1995.
— Vol. 44, no. 6. — P. 754–768.33. Sarkar, S. Understanding POWER Multiprocessors / S. Sarkar, P. Sewell, J. Alglave, L. Maranget, D. Williams // Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, SanJose, CA, USA, June 4–8, 2011. — ACM, 2011. — P. 175–186.34. Kavanagh, R. A Denotational Semantics for SPARC TSO / R. Kavanagh,S. Brookes // CoRR. — 2017. — Vol.
abs/1711.00931. — URL: http://arxiv.org/abs/1711.00931.35. Crary, K. A Calculus for Relaxed Memory / K. Crary, M. J. Sullivan // Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL 2015, Mumbai, India, January 15–17, 2015. —2015.
— P. 623–636.36. Boudol, G. Relaxed Operational Semantics of Concurrent Programming Languages / G. Boudol, G. Petri, B. P. Serpette // EXPRESS 2012. — 2012. —P. 19–33.37. Boudol, G. Relaxed memory models: an operational approach / G. Boudol,G. Petri // POPL 2009. — 2009. — P. 392–403.38. Pichon-Pharabod, J. A Concurrency Semantics for Relaxed Atomics that PermitsOptimisation and Avoids Thin-Air Executions / J. Pichon-Pharabod, P. Sewell //Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St.
Petersburg, FL, USA, January20–22, 2016. — ACM, 2016. — P. 622–633.13239. Jeffrey, A. On Thin Air Reads Towards an Event Structures Model of RelaxedMemory / A. Jeffrey, J. Riely // Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5–8,2016. — 2016. — P. 759–767.40. Nienhuis, K. An operational semantics for C/C++11 concurrency / K.
Nienhuis,K. Memarian, P. Sewell // Proceedings of the 2016 ACM SIGPLAN InternationalConference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands,October 30 – November 4, 2016.
— 2016. — P. 111–128.41. Diehl, S. Abstract machines for programming language implementation / S. Diehl,P. H. Hartel, P. Sestoft // Future Generation Comp. Syst. — 2000. — Vol. 16, no. 7.— P. 739–751.42. Vafeiadis, V. Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it / V. Vafeiadis, T. Balabonski,S. Chakraborty, R. Morisset, F. Zappa Nardelli // Proceedings of the 42nd AnnualACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,POPL 2015, Mumbai, India, January 15–17, 2015. — 2015. — P.
209–220.43. Morisset, R. Compiler testing via a theory of sound optimisations in theC11/C++11 memory model / R. Morisset, P. Pawan, F. Zappa Nardelli // ACMSIGPLAN Conference on Programming Language Design and Implementation,PLDI ’13, Seattle, WA, USA, June 16–19, 2013. — 2013. — P. 187–196.44. Sevcík, J. On Validity of Program Transformations in the Java Memory Model /J. Sevcík, D. Aspinall // ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings. — 2008. —P.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
