МОДЕЛИ ПАМЯТИ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ: ОБЗОР И ТЕНДЕНЦИИ (2021)
Модель памяти языка программирования определяет семантику многопоточных программ, создаваемых на этом языке и оперирующих с разделяемой памятью. Наиболее известна модель последовательной согласованности, которая является слишком строгой, запрещая многие сценарии поведения, наблюдаемые при исполнении программ на современных процессорах. Попытки формально описать эти сценарии привели к возникновению так называемых слабых моделей памяти. В последние годы было предложено значительное количество слабых моделей памяти для различных языков программирования. Эти модели предлагают различные компромиссы относительно простоты/сложности рассуждений о поведении многопоточных программ и возможностей их оптимизации. Цель данной статьи заключается в обзоре существующих моделей памяти языков программирования и выработке общих рекомендаций по выбору/созданию модели памяти при создании/стандартизации языков программирования, а также при разработке компиляторов. Для данного обзора мы рассмотрели более 2000 статей, найденных по ключевым словам “Relaxed Memory Models”, “Weak Memory Models”, и “Weak Memory Consistency” поисковой системой Google Scholar. Используя разные критерии, мы сузили это множество до 40 статей, предлагающих и описывающих модели памяти языков программирования. Мы разделили эти модели на шесть классов и проанализировали их свойства и ограничения. В заключение мы показали, как дизайн языка программирования влияет на выбор модели памяти и обсудили возможные направления дальнейших исследований в этой области.
Идентификаторы и классификаторы
- eLIBRARY ID
- 46621835
Многопоточное программирование активно используется в современном программировании, позволяя достичь существенного выигрыша в производительности системного программного обеспечения – ядер операционных систем, СУБД, высоконагруженных клиент-серверных приложений и пр. Главная трудность многопоточного программирования заключается в необходимости обеспечить корректную синхронизацию между различными потоками программы. Обычно это достигается при помощи специальных примитивов синхронизации, таких как блокировки, барьеры, каналы и т.д. Однако часто использование этих примитивов не позволяет достичь нужной производительности. Распространенным примером являются различные неблокирующие (lockfree) структуры данных. В подобных случаях необходимо обращаться к средствам низкоуровневого программирования и взаимодействовать с разделяемой потоками памятью напрямую. Здесь начинаются сложности.
Список литературы
- Dijkstra E.W. “Cooperating sequential processes”, in The origin of concurrent programming. Springer, 1968. P. 65-138.
- Lamport L. “How to make a multiprocessor computer that correctly executes multiprocess programs”, IEEE Trans. Computers. 1979. V. 28. № 9. P. 690-691.
- Manson J., Pugh W., Adve S.V. “The Java memory model”, in POPL 2005. P. 378-391, ACM, 2005.
- Bender J., Palsberg J. “A formalization of Java’s concurrent access modes”, Proceedings of the ACM on Programming Languages. 2019. V. 3. № OOPSLA. P. 1-28.
- Batty M., Owens S., Sarkar S., Sewell P., Weber T. “Mathematizing C++ concurrency”, in POPL 2011. 2011. P. 55-66, ACM.
- Chakraborty S., Vafeiadis V. “Formalizing the concurrency semantics of an LLVM fragment”, in 2017 IEEE/ACM International Symposium on Code Generation and Optimization (CGO). IEEE, 2017. P. 100-110.
- Watt C., Pulte C., Podkopaev A., Barbier G., Dolan S., Flur S., Pichon-Pharabod J., Guo S.-y. “Repairing and mechanizing the JavaScript relaxed memory model”, in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 2020. P. 346-361.
- Vollmer M., Scott R.G., Musuvathi M., Newton R.R. “SC-Haskell: Sequential consistency in languages that minimize mutable shared heap”, ACM SIGPLAN Notices. 2017. V. 52. № 8. P. 283-298.
- Sewell P., Sarkar S., Owens S., Nardelli F.Z., Myreen M.O. “x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors”, Commun. ACM. 2010. V. 53. № 7. P. 89-97.
-
Alglave J., Fox A., Ishtiaq S., Myreen M.O., Sarkar S., Sewell P., Nardelli F.Z. "The semantics of Power and ARM multiprocessor machine code", in Proceedings of the 4th workshop on Declarative aspects of multicore programming. 2009. P. 13-24. -
Sarkar S., Sewell P., Alglave J., Maranget L., Williams D. "Understanding POWER multiprocessors", in PLDI 2011. ACM, 2011. P. 175-186. -
Alglave J., Maranget L., Tautschnig M. "Herding cats: Modelling, simulation, testing, and data mining for weak memory", ACM Trans. Program. Lang. Syst. 2014. V. 36. № 2. P. 7:1-7:74. -
Chong N., Ishtiaq S. "Reasoning about the ARM weakly consistent memory model", in Proceedings of the 2008 ACM SIGPLAN workshop on Memory systems performance and correctness: held in conjunction with the Thirteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'08). 2008. P. 16-19. -
Pulte C., Flur S., Deacon W., French J., Sarkar S., Sewell P. "Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8", Proceedings of the ACM on Programming Languages. 2018. V. 2. № POPL. P. 1-29. -
Flur S., Gray K.E., Pulte C., Sarkar S., Sezgin A., Maranget L., Deacon W., Sewell P. "Modelling the ARMv8 architecture, operationally: Concurrency and ISA", in POPL 2016. 2016. P. 608-621, ACM. -
Boehm H.-J., Demsky B. "Outlawing ghosts: Avoiding out-of-thin-air results", in MSPC 2014. 2014. P. 7:1-7:6, ACM. -
Kang J., Hur C.-K., Lahav O., Vafeiadis V., Dreyer D. "A promising semantics for relaxedmemory concurrency", in POPL 2017, ACM, 2017. -
Lee S.-H., Cho M., Podkopaev A., Chakraborty S., Hur C.-K., Lahav O., Vafeiadis V. "Promising 2.0: global optimizations in relaxed memory concurrency", in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 2020. P. 362-376. -
Chakraborty S., Vafeiadis V. "Grounding thin-air reads with event structures", Proceedings of the ACM on Programming Languages. 2019. V. 3. № POPL. P. 1-28. EDN: OELGYA -
Paviotti M., Cooksey S., Paradis A., Wright D., Owens S., Batty M. "Modular relaxed dependencies in weak memory concurrency", in European Symposium on Programming. P. 599-625, Springer, Cham, 2020. -
Lahav O., Vafeiadis V., Kang J., Hur C.-K., Dreyer D. "Repairing sequential consistency in C/C++11", in PLDI 2017, ACM, 2017. -
Dolan S., Sivaramakrishnan K., Madhavapeddy A. "Bounding data races in space and time", ACM SIGPLAN Notices. 2018. V. 53. № 4. P. 242-255. -
Ou P., Demsky B. "Towards understanding the costs of avoiding out-of-thin-air results", Proceedings of the ACM on Programming Languages. 2018. V. 2. № OOPSLA. P. 1-29. EDN: MPRRDS -
Jeffey A., Riely J. "On thin air reads: Towards an event structures model of relaxed memory", in LICS 2016, IEEE, 2016. -
Pichon-Pharabod J. and Sewell P., "A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions", in POPL 2016. 2016. P. 622-633, ACM. -
Marlow S. et al. "Haskell 2010 language report", Available on: https://www. haskell. org/onlinereport/haskell2010, 2010. -
Klabnik S., Nichols C. The Rust Programming Language (Covers Rust 2018). No Starch Press, 2019. -
Boehm H.-J., Adve S.V. "Foundations of the C++ concurrency memory model", ACM SIGPLAN Notices. 2008. V. 43. № 6. P. 68-78. -
Lahav O., Giannarakis N., Vafeiadis V. "Taming release-acquire consistency", ACM SIGPLAN Notices. 2016. V. 51. № 1. P. 649-662. -
Flur S., Sarkar S., Pulte C., Nienhuis K., Maranget L., Gray K.E., Sezgin A., Batty M., Sewell P. "Mixed-size concurrency: ARM, Power, C/C++ 11, and SC", ACM SIGPLAN Notices. 2017. V. 52. № 1. P. 429-442. -
"C/C++11 mappings to processors", 2011. Available at https://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html [Online; accessed 26-April-2021]. -
Marino D., Singh A., Millstein T., Musuvathi M., Narayanasamy S. "A case for an SC-preserving compiler", ACM SIGPLAN Notices. 2011. V. 46. № 6. P. 199-210. -
Liu L., Millstein T., Musuvathi M. "A volatile-by-default JVM for server applications", Proceedings of the ACM on Programming Languages. 2017. V. 1. № OOPSLA. P. 1-25. -
Muchnick S. Advanced compiler design and implementation. Morgan kaufmann, 1997. -
Lahav O., Namakonov E., Oberhauser J., Podkopaev A., Vafeiadis V. "Making weak memory models fair", arXiv preprint arXiv:2012.01067, 2020. -
Ševčík J., Aspinall D. "On validity of program transformations in the Java memory model", in European Conference on Object-Oriented Programming. P. 27-51, Springer, 2008. -
Wegman M.N., Zadeck F.K. "Constant propagation with conditional branches", ACM Transactions on Programming Languages and Systems (TOPLAS). 1991. V. 13. № 2. P. 181-210. -
Maranget L., Sarkar S., Sewell P. "A tutorial introduction to the ARM and POWER relaxed memory models", 2012. Available at https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/ test7.pdf [Online; accessed 30-April-2021]. -
Boudol G., Petri G. "A theory of speculative computation", in European Symposium on Programming. Springer, 2010. P. 165-184. -
Singh A., Narayanasamy S., Marino D., Millstein T., Musuvathi M. "End-toend sequential consistency", in 2012 39th Annual International Symposium on Computer Architecture (ISCA). IEEE, 2012. P. 524-535. -
Liu L., Millstein T., Musuvathi M. "Accelerating sequential consistency for Java with speculative compilation", in Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019. P. 16-30. -
Marino D., Singh A., Millstein T., Musuvathi M., Narayanasamy S. "DRFx: A simple and efficient memory model for concurrent programming languages", in Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation. 2010. P. 351-362. -
Demange D., Laporte V., Zhao L., Jagannathan S., Pichardie D., Vitek J. "Plan B: A buffered memory model for Java", in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 2013. P. 329-342. -
Boudol G., Petri G. "Relaxed memory models: an operational approach", ACM SIGPLAN Notices. 2009. V. 44. № 1. P. 392-403. -
Dodds M., Batty M., Gotsman A. "Compositional verification of compiler optimisations on relaxed memory", in European Symposium on Programming. Springer, 2018. P. 1027-1055. -
Doherty S., Dongol B., Wehrheim H., Derrick J. "Verifying C11 programs operationally", in Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming. 2019. P. 355-365. -
Dang H.-H., Jourdan J.-H., Kaiser J.-O., Dreyer D. "RustBelt meets relaxed memory", Proceedings of the ACM on Programming Languages. 2019. V. 4. № POPL. P. 1-29. -
Alglave J., Maranget L., McKenney P.E., Parri A., Stern A. "Frightening small children and disconcerting grownups: Concurrency in the Linux kernel", in Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems. 2018. P. 405-418. -
Zhang Y., Feng X. "An operational happens-before memory model", Frontiers of Computer Science. 2016. V. 10. № 1. P. 54-81. -
Huisman M., Petri G. "The Java memory model: a formal explanation", VAMP. 2007. V. 7. P. 81-96. -
Jagadeesan R., Pitcher C., Riely J. "Generative operational semantics for relaxed memory models", in European Symposium on Programming. Springer, 2010. P. 307-326. -
Sarkar S., Memarian K., Owens S., Batty M., Sewell P., Maranget L., Alglave J., Williams D. "Synchronising C/C++ and POWER", in Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. 2012. P. 311-322. -
Batty M., Memarian K., Owens S., Sarkar S., Sewell P. "Clarifying and compiling C/C++ concurrency: from C++ 11 to POWER", ACM SIGPLAN Notices. 2012. V. 47. № 1. P. 509-520. -
Vafeiadis V., Balabonski T., Chakraborty S., Morisset R., Nardelli F.Z. "Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it", in POPL 2015. ACM, 2015. P. 209-220. -
Batty M., Memarian K., Nienhuis K., Pichon-Pharabod J., Sewell P. "The problem of programming language concurrency semantics", in ESOP. V. 9032 of LNCS. Springer, 2015. P. 283-307. -
Batty M., Donaldson A.F., Wickerson J. "Overhauling SC atomics in C11 and OpenCL", in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2016. P. 634-648. -
Nienhuis K., Memarian K., Sewell P. "An operational semantics for C/C++ 11 concurrency", in Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 2016. P. 111-128. -
Crary K., Sullivan M.J. "A calculus for relaxed memory", in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2015. P. 623-636. -
Saraswat V.A., Jagadeesan R., Michael M., von Praun C. "A theory of memory models", in Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming. 2007. P. 161-172. -
Inc S.I., Weaver D.L. The SPARC architecture manual. Prentice-Hall, 1994. -
Lustig D., Trippel C., Pellauer M., Martonosi M. "ArMOR: Defending against memory consistency model mismatches in heterogeneous architectures", in Proceedings of the 42nd Annual International Symposium on Computer Architecture. 2015. P. 388-400. -
Podkopaev A., Lahav O., Vafeiadis V. "Bridging the gap between programming languages and hardware weak memory models", Proceedings of the ACM on Programming Languages. 2019. V. 3. № POPL. P. 1-31. EDN: BFQNGS -
Pugh W. "Fixing the Java memory model", in Proceedings of the ACM 1999 conference on Java Grande. 1999. P. 89-98. -
Diwan A., McKinley K.S., Moss J.E.B. "Type-based alias analysis", ACM Sigplan Notices. 1998. V. 33. № 5. P. 106-117. -
Svendsen K., Pichon-Pharabod J., Doko M., Lahav O., Vafeiadis V. "A separation logic for a promising semantics", in Programming Languages and Systems (A. Ahmed, ed.), (Cham). P. 357-384, Springer International Publishing, 2018. -
Choi J.-D., Gupta M., Serrano M., Sreedhar V.C., Midkiff S. "Escape analysis for Java", Acm Sigplan Notices. 1999. V. 34. № 10. P. 1-19. -
Jagadeesan R., Jeffrey A., Riely J. "Pomsets with preconditions: a simple model of relaxed memory", Proceedings of the ACM on Programming Languages. 2020. V. 4. № OOPSLA. P. 1-30. EDN: DPFTGP -
Cho M., Lee S.-H., Hur C.-K., Lahav O. "Modular data-race-freedom guarantees in the Promising semantics", in Proceedings of the 42st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2021.
Выпуск
ИНФОРМАЦИОННАЯ БЕЗОПАСНОСТЬ
ПАРАЛЛЕЛЬНОЕ И РАСПРЕДЕЛЕННОЕ ПРОГРАММИРОВАНИЕ
ЯЗЫКИ, КОМПИЛЯТОРЫ И СИСТЕМЫ ПРОГРАММИРОВАНИЯ
КОМПЬЮТЕРНАЯ ГРАФИКА И ВИЗУАЛИЗАЦИЯ
МНОГООКОННАЯ ВИЗУАЛИЗАЦИЯ АВИАЦИОННОГО ДИСПЛЕЯ С ИСПОЛЬЗОВАНИЕМ АППАРАТНОГО УСКОРЕНИЯ
АНАЛИЗ ДАННЫХ
Другие статьи выпуска
В статье рассматривается поиск ошибок помеченных данных в исходном коде программ, т.е. ошибок, вызванных небезопасным использованием данных, полученных из внешних источников, которые потенциально могут быть изменены злоумышленником. В качестве основы использовался межпроцедурный статический анализатор Svace. Анализатор осуществляет как поиск дефектов в программе, так и поиск подозрительных мест, в которых логика программы может быть нарушена. Целью является найти как можно больше ошибок при приемлемой скорости и низком уровне ложных срабатываний (<20–35%). Для поиска ошибок Svace с помощью компилятора строит низкоуровневое типизированное промежуточное представление, которое подается на вход основному анализатору SvEng. Анализатор строит граф вызовов, после чего выполняет анализ на основе резюме. При таком анализе функции обходятся в соответствии с графом вызовов, начиная с листьев. После анализа функции создается ее резюме, которое затем будет использовано для анализа инструкций вызова. Анализ имеет как высокую скорость, так и хорошую масштабируемость. Внутрипроцедурный анализ основан на символьном выполнении с объединением состояний в точках слияния путей. Для отсеивания несуществующих путей для некоторых детекторов может использоваться SMT-решатель. При этом SMT-решатель вызывается, только если есть подозрение на ошибку. Анализатор был расширен возможностью поиска дефектов, связанных с помеченными данными. Детекторы реализованы в виде плагинов по схеме источник-приемник. В качестве источников используются вызовы библиотечных функций, получающих данные извне программы, а также аргументы функции main. Приемниками являются обращение к массивам, использование переменных как шага или границы цикла, вызов функций, требующих проверенных аргументов. Реализованы детекторы, покрывающие большинство возможных типов уязвимостей, для непроверенных целых чисел и строк. Для оценки покрытия использовался проект Juliet. Уровень пропусков составил от 46.31% до 81.17% при незначительном количестве ложных срабатываний.
Современный дисплей пилота гражданского самолета основан на новой идеологии интерфейса и позволяет улучшить восприятие полетной информации из нескольких источников за счет ее объединения на одном многофункциональном дисплее. В работе рассматриваются вопросы реализации многооконной визуализации дисплея пилота при использовании OpenGL SC с аппаратным ускорением. Предложен алгоритм компоновки информации на дисплее, позволяющий применять только одно GPU устройство, доступное на борту самолета. Подробно изложен подход адаптации и модификации пакета Mesa с открытым программным кодом для получения сертифицируемого драйвера GPU. Особое внимание уделено технологии адаптации открытых кодов пакета к операционной системе реального времени и к требованиям к системам, критичным для безопасности. Реализация предложенного подхода предназначена для работы под управлением операционной системы реального времени JetOS в системах визуализации бортовых комплексов гражданской авиации. Описанная реализация многооконной визуализации предполагает в дальнейшем ее сертификацию для систем, критичных для безопасности.
В статье описывается программная реализация быстрого алгоритма поиска распределенных рассеивателей для задачи построения скоростей смещений земной поверхности на базе платформы Apache Spark. Рассматривается полная схема расчета скоростей смещений методом постоянных рассеивателей (PS). Предложенный алгоритм интегрируется в схему после этапа совмещения с субпиксельной точностью стека изображений временной серии радарных снимков космического аппарата Sentinel-1. Поиск распределенных рассеивателей происходит независимо в окнах сдвига по всей площади снимка. Наличие последних определяется путем предположения о гомогенности пар выборок в окне, составленных из векторов комплексных значений пикселей в каждом из N изображений. Данное предположение вытекает из выполнимости критерия Колмогорова–Смирнова для каждой из пар. Для оценки значений фаз гомогенных пикселей решается задача максимизации. Показано, что предложенный алгоритм не является итерационным и может быть реализован в парадигме параллельных вычислений. Применяемая платформа Apache Spark позволила распределенно обрабатывать массивы стека радарных данных (от 60 изображений) в памяти на большом количестве физических узлов в сетевой среде. При этом, время поиска распределенных рассеивателей удалось снизить в среднем в 10 раз по сравнению с однопроцессорной реализацией алгоритма. Приведены сравнительные результаты тестирования вычислительной системы на демонстрационном кластере. Алгоритм реализован на языке программирования Python c подробным описанием объектов и методов алгоритма.
Разработан метод контроля и восстановления целостности данных в многомерных системах хранения. Предложенные конструкции контроля и восстановления целостности многомерных массивов данных основаны на агрегировании методов криптографии и помехоустойчивого кодирования. На основе представленных криптокодовых конструкций показана особенность комплексирования существующих методов, заключающаяся в повышении вероятности обеспечения целостности информации в условиях разрушающих воздействий злоумышленника и среды для многомерных систем хранения данных. Получены расчетные данные вероятности обнаружения и исправления возникающих в многомерных массивах данных ошибок, приводящих к нарушению их целостности, посредством разработанного метода.
Издательство
- Издательство
- ИЗДАТЕЛЬСТВО НАУКА
- Регион
- Россия, Москва
- Почтовый адрес
- 121099 г. Москва, Шубинский пер., 6, стр. 1
- Юр. адрес
- 121099 г. Москва, Шубинский пер., 6, стр. 1
- ФИО
- Николай Николаевич Федосеенков (Директор)
- E-mail адрес
- info@naukapublishers.ru
- Контактный телефон
- +7 (495) 2767735