Расчетная модель для нахождения состояния гонки в многопоточных алгоритмах тема диссертации и автореферата по ВАК РФ 05.13.18, кандидат физико-математических наук Заборовский, Никита Владимирович

• Заборовский, Никита Владимирович
• кандидат физико-математических наук
• 2011

Оглавление диссертации кандидат физико-математических наук Заборовский, Никита Владимирович

Оглавление.

Введение.

Актуальность темы.

Цель работы, задачи исследования.

Научная новизна.

Практическая ценность.

Положения, выносимые на защиту.

Публикации и апробация результатов.

Краткое содержание работы.

Глава 1. Обзор существующих методов.

Общие способы поиска проблем в параллельных программах.

Статический анализ.

Методы.

Типы анализа.

Алгоритмы.

Особенности работы.

Анализаторы.

Динамический анализ.

Методы.

Средства динамического анализа.

Проверка на основе моделей.

Синхронизация в многопоточных алгоритмах.

Неблокирующие алгоритмы.

Классификация исполнения параллельных программ.

Глава 2. Подходы к моделированию исполнения потоков.

Идея подхода.

Построение графа совместного исполнения п потоков.

Глава 3. Сложности и проблемы существующих подходов к моделированию исполнения потоков.

Проблемы современных систем статического анализа.

Ветвления.

Циклы.

Другие проблемы.

Анализ значений переменных.

Глава 4. Предлагаемая модель, ориентированная на реальные алгоритмы.

Предлагаемое расширение модели.

Ветвления.

Циклы.

Общее представление о расчетном графе.

Обозначение на рисунках и схемах.

Построение.

Метод неопределенных коэффициентов.

Класс анализируемых алгоримов.

Представление циклов и ветвлений.

Конструктивное построение расчетного графа.

Расчеты на графе.

Доказательство корректности подхода.

Обоснованность использования представителей класса эквивалентности в расчетном графе.

Глава 5. Практическая реализация анализа на построенной модели и результаты его работы на многопоточных алгоритмах.

Комплекс программ для полуавтоматического анализа.

Модельные эксперименты.

Выводы.

Введение диссертации (часть автореферата) на тему «Расчетная модель для нахождения состояния гонки в многопоточных алгоритмах»

Актуальность темы.

Многопоточная организация программ достаточно давно применяется программистами. При одноядерной архитектуре процессоров использование нескольких потоков обеспечивало упрощение процесса программирования, работу с блокирующими операциями и. т.д. Чтобы эффективно использовать современные аппаратные платформы, нужны совершенно новые принципы и подходы. Под «эффективностью» понимается выигрыш от использования многоядерной платформы по сравнению. с> одноядерной. Иногда программы, написанные для одноядерной архитектуры, запускают на четырехядерной в надежде получить прирост производительности, а в результате оказывается, что производительность таких программ даже уменьшается.

Универсальных способов создавать эффективные программы!, не существует. Подход для каждой - строго индивидуален. Как одно из решений можно упомянуть неблокирующие алгоритмы -альтернативу алгоритмам, использующим явные средства синхронизации.

Отсутствие универсальных подходов влечёт за собой также возможные ошибки программистов. Одной из наиболее сложных для обнаружения ошибок является состояние гонки. Состояния гонки (race condition; конкурентного доступа к памяти) — ситуация, когда состояние общей для нескольких потоков ячейки памяти зависит от распределения процессорного времени между потоками. Предугадать это состояние на уровне алгоритма невозможно. Понять аналитически, что возникло состояние гонки, очень сложно, т.к. для этого требуется анализ экспоненциально растущего количества ситуаций. Именно поэтому так важно контролировать программы ещё на стадии описания. Создание средств контроля корректности программ становится всё более необходимым с выпуском каждого нового процессора и написанием каждого нового сложного программного комплекса.

Различают два принципиально разных подхода к анализу многопоточных алгоритмов на предмет наличия состояний гонки: динамический и статический. Динамический подход представляет собой эмпирическую процедуру «прогона» программы при различных входных данных (data-race-test в Google, Intel Thread Checker). Принципиальный недостаток подхода в целом невозможно проверить сложную систему, поскольку количество тестов экспоненциально зависит от числа- входных параметров. Статический подход анализирует архитектуру программы и программный код без его запуска. К статическому анализу относится формальное доказательство корректности кода программы. Для современных программных продуктов сложность формального доказательства значительна, что делает его неприменимым в промышленных масштабах. Кроме того, есть вероятность ложного срабатывания. Один и тот же алгоритм может содержать состояние гонки и не содержать его в зависимости от значений входных параметров.

В статическом анализе есть ряд известных проблем. В частности, многие алгоритмы используют в своей логике значения разделяемых переменных (алгоритм Петерсона[4], стек Трейбера[7]). Без учета значений при анализе таких алгоритмов получится заведомо неверный результат - это связано с тем, что логика поведения алгоритмов построена на проверке значений

разделяемых переменных. Большинству средств анализа алгоритмов не удается обнаруживать ошибки в логике алгоритмов, подобных алгоритму Петерсона. Поиск ошибок в таких алгоритмах- серьёзная исследовательская задача.

Отдельные задачи, неразрывно связанные со статическим анализом программ — задача об* идентификации разделяемых ресурсов и задача о превдонимах.

Помимо упомянутых методов, можно также отметить методы проверки на основе моделей (проверка, при которой варианты получаются из-модели, описывающей функциональность системы) и метод аналитического доказательства корректности [9] программ. Оба метода сложно применить на практике из-за того, что они занимают много времени и требуют больших человеческих усилий. Однако, иногда втречаются экзотические случаи их использования [27].

Цель работы, задачи исследования.

Существует несколько подходов к статическому анализу кода неблокирующих алгоритмов в поисках состояния гонки. Однако, большая часть из них носит чисто теоретический характер, подходит только для модельных задач и дает неточные результаты (большой процент ложных срабатываний и не обнаружений гонки, когда она есть, false-negative). Необходим подход к анализу исходных кодов современных прикладных программ, учитывающий их сложность и специфику.

Для этого, во-первых, необходимо разработать математическую модель, представляющую ход исполнения потоков с точки зрения работы с общими разделяемыми переменными. Модель должна быть применима для анализа реальных современных программ и моделировать исполнение современной многопоточной программы.

Во-вторых, на основе этой модели должен быть разработан метод, позволяющий:

• определять состояние гонки, если оно есть, не давая ложных срабатываний в определенном классе задач;

• давать результат за время, приемлемое для использования при тестировании программных продуктов внутри компании-разработчика.

Кроме модели и метода должен быть создан комплекс программ, анализирующий многопоточные алгоритмы с целью выявления состояний гонки и обладающий следующими свойствами:

• возможность анализировать исходный код на языках высокого уровня и выдавать промежуточное представление исходного кода, аналогичное тому, которое получается на стадии компиляции программы;

• реализация разработанного метода и указание мест возникновения гонки и приводящих к ней условий.

Научная новизна.

Научная новизна работы заключается в математическом моделировании поведения многопоточных алгоритмов, содержащих вервления и циклы, использующих разделяемую память. Математическая модель, предлагаемая в работе, учитывает начальные и промежуточные значения разделяемых переменных. Для модели разработана методика поиска состояний гонки в программном коде для определенного класса задач.

Хорошо известен ряд динамических и синтаксических анализаторов, обладающих следующими недостатками: тяжеловесность, зависимость от контекста, малая точность. Разработанный метод не зависит от контекста, определяет состояние гонки, если оно есть, и не даёт ложных срабатываний в рамках определенного класса алгоритмов. Что касается тяжеловесности, то для статических анализаторов эта проблема стоит менее остро, чем для динамических. В работе в качестве примера приведён легковесный алгоритм анализа.

Практическая г\енностъ.

Созданные модель и метод ориентированы на практическую реализацию. В работе предложены методика анализа кода на присутствие состояния гонки, использующая некое промежуточное представления кода, и техническая реализация получения промежуточного представления из исходного кода. В качестве средства обработки исходного кода может быть использовано любое другое подходящее средство, позволяющее получить специфицированное промежуточное представление.

Положения, выносилше на защиту.

1. Математическая модель исполнения многопоточных программ, учитывающая зависимость исполнения от начальных значений разделяемых переменных и описывающая, в том числе, такие конструкции программного кода как циклы, ветвления и атомарные операции.

2. Общий метод анализа многопоточных алгоритмов на предмет наличия гонок, в основе которого лежит анализ значений разделяемых переменных, и критерии корректности алгоритмов в понятиях разработанной модели.

3. Комплекс программ и результаты вычислительных экспериментов для выявления наличия гонок в некоторых многопоточных алгоритмах, в том числе неблокирующих.

Публикации и апробация результатов.

По теме диссертации опубликовано 12 работ, в том числе три [39, 40, 41] - в изданиях, рекомендованных ВАК РФ для опубликования основных научных результатов диссертаций.

Результаты работы докладывались и получили одобрение специалистов на научных семинарах и конференциях:

- XXXVI международная молодежная научная конференция «Гагаринские чтения» (Москва, 2009 г.),

- XXVII международные молодежные научные конференции «Гагаринские чтения» (Москва, 2010 г.),

- 5-ая международная конференция им. П.Л. Чебышева (Ногинск, 2011 г.),

- XVI Международная научная конференция студентов, аспирантов и молодых учёных «ЛОМОНОСОВ- 2009» (Москва, 2009 г.),

- 49-ая научная конференция МФТИ (Москва, 2007),

- 53-ая научная конференция МФТИ (Москва, 2009 г).

Краткое содержание работы.

Во введении обосновывается актуальность диссертации, и формулируются ее цели, характеризуются научная новизна и практическая ценность работы.

В главе 1 приводится краткий обзор существующих методов анализа исходного кода, а также программных средств, реализующих их.

Приводятся примеры статических анализаторов, приводятся известные проблемы и возможные пути решений. Рассматриваются такие анализаторы как Viva64, Intel thread checker, data-race-test, KISS, CHESS и другие.

В главе 2 описывается один из модельных подходов к описанию многопоточного исполнения алгоритмов, взятый за основу в данной работе.

В главе 3 излагаются сложности и узкие места при статическом анализе программного кода существующими методами. Рассматривается реальный практический код, часто имеющий сложную структуру, содержащий циклы и ветвления, а также атомарные операции.

В главе 4 автором предлагается и обосновывается расширенный подход к статическому анализу практических не модельных задач, включающий специфическую терминологию и методы.

В заключительной главе 5 приведены аспекты практической реализации комплекса программ для анализа многопоточных алгоритмов, а также результаты его работы на известных многопоточных алгоритмах с оценками сложности анализа.

Заключение диссертации по теме «Математическое моделирование, численные методы и комплексы программ», Заборовский, Никита Владимирович

Заключение.

1. Разработана математическая модель исполнения многопоточных программ, учитывающая зависимость исполнения от начальных значений разделяемых переменных и позволяющая анализировать многопоточные алгоритмы, содержащие циклы, ветвления и атомарные операции.

2. Предложен метод полуавтоматического поиска состояний гонки (конкурентного доступа к памяти) в классе алгоритмов, содержащих только линейные операции с разделяемыми переменными, а также сформулированы критерии корректности для нескольких алгоритмов.

3. Создан комплекс программ для исследования многопоточных алгоритмов, содержащих циклы, ветвления и атомарные операции с целью выявления состояний гонки.

4. На основании результатов серии вычислительных экспериментов с использованием предложенной математической модели, методов и комплекса программ получены численные оценки сложности для ряда алгоритмов.

Список литературы диссертационного исследования кандидат физико-математических наук Заборовский, Никита Владимирович, 2011 год

1. Herlihy М., Shavit N. The Art of Multiprocessor Programming. Elsevier, 2008.

2. Serebryany K. Data race test Электронный ресурс. Режим дост.: http://code.google.com/p/data-race-test)3.|Qadeer S., Wu D. KISS: keep it simple and sequential. PLDI, 2004.

3. Peterson G. L. Myths About the Mutual Exclusion Problem // Information Processing Letters — 1981. -12(3). P. 1 15-1 16.

4. Bodden E., Havelund K. Racer: effective race detection using Aspectj. ISSTA, 2008.

5. Michael M., Scott M. Nonblocking Algorithms and Preemption-Safe Locking on Multiprogrammed Shared Memory Multiprocessors Электронный ресурс. — 1997. — Режим дост.:http ://f-cpu. seul. org/new/michae 19 8 nonblocking.pdf

6. Hendler D., Shavit N., Yerushalmi L. A Scalable Lock-free Stack Algorithm Электронный ресурс. — 2004. — Режим дост.: http://www.cs.tau.ac.il/~shanir/nir-pubs-web/Papers/LockFree.pdf

7. Патил Р. В., Джордж Б. Средства и приемы для выявления проблем параллельного выполнения Электронный ресурс. Режим дост.:-http://msdn.microsoft.com/ru-ru/magazine/cc5465 69.aspx

8. Карпов А. Тестирование параллельных программ Электронный ресурс. 2008. — Режим дост.: http://www.viva64.eom/ru/a/0031/

9. Романовский Е. Отладка многопоточных ОрепМР-программ // Мир ПК. 2008. - №02.

10. Herlihy М. Obstruction-Free Synchronization: Double-Ended Queues as an Example -Электронный ресурс. — 2003. — Режим дост.: http://citeseerx. is t. psu.edu/vie w doc/down load? do i= 1 0.1.1.83.7992&rep = repl &type=pdf

11. Skiena S. Combinatorics and Graph Theory with Mathematica 2004. — Электронный ресурс. - Режим до ст.: http://www.es .sunysb.edu/~skiena/talks/talk-combinatorica.pdf

12. Кудрин М.Ю., Прокопенко А.С., Тормасов А.Г. Метод нахождения состояний гонки в потоках, работающих на разделяемой памяти // Сборник научных трудов МФТИ. М.: МФТИ, 2009. - № 4. - Том 1. - С. 181-201.

13. О 'Callahan R., Choi J.-D. Hybrid Dynamic Data Race Detection PpoPP'03, San Diego, California, USA. - 2003.

14. Карпов А. Тестирование параллельных программ Электронный ресурс. — Режим дост.: http://www.softwaretesting. ru/library/testing/functionalte sting/5 8 1 -parallelprogramtesting

15. Savage S., Burrows M., Nelson G., Sobalvarro P., Anderson T. Eraser: A dynamic data race detector for multithreaded programs // ACM Trans, on Computer Systems. 15(4). - 1997.

16. Davies B. Whither Mathematics? // Notices of the American Mathematical Society. 2005. - V. 52, N.ll.

17. Emanuelsson P., Nilsson U. A Comparative Study of Industrial Static Analysis Tools // Elsevier Science Publishers. 2008. - Amsterdam, Netherlands.

18. Chelf В., Engler D., Hallem S. How to Write Systemspecic, Static Checkers in Metal // In PASTE '02: Proceedings of the 2002 ACM SIGPL AN-SIGSOFT workshop on Program Analysis for Software Tool and Engineering. 2002. P. 51-60.

19. Deutsch A. Interprocedural May-Alias Analysis for Pointers : Beyond k-limiting // In Proc. Programming Language Design and Implementation. ACM Press, 1994.

20. Sleensgaard B. Points-to Analysis in Almost Linear Time // In ACM POPL. 1996.

21. Калугин А. Верификатор программ на языке Си LINT Электронный ресурс. Режим дост.: http://www. viva 6 4 .com/go.php?url:=224

22. Карпов А. Что такое "Parallel Lint"? Электронный ресурс. — Режим дост.: http://software.intel.com/ru-ru/articles/par all el -lint/

23. Static Source Code Analysis Tools for C. Электронный ресурс. — Режим до ст. : http ://www. spinr о ot. com/static/

24. Gao H., Groote G.F., Hesselink W.H. Almost Wait-free Resizable Hashtables Электронный ресурс. — 2005. Режим дост.: http://www.cs.rug.nl/~wim/pub/hashtable.ps

25. Каличкин С.В. Обзор средств статической отладки. — Новосибирск: 2004. С. 12-22.

26. Terboven С. Comparing Intel Thread Checker and Sun Thread Analyze // Center for Computing and Communication RWTH Aachen University, Germany. -2007.

27. Использование Thread Analyzer для поиска конфликтов доступа к данным Электронный ресурс. — Режим дост.: http://ru.su п. com/de velopers/sunstudio/articles/thausin gru.html

28. Dinning A., Schonberg E. An empirical comparison of monitoring algorithms for access anomaly detection // In Proceedings of the Second ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP). 1990. - C. 1-10.

29. Mellor-Crummey J. On-the-fly detection of data races for programs with nested fork-join parallelis // In Proceedings of the 1991 ACM/IEEE conference on Supercomputing. ACM Press, 1991. - P. 24-33.

30. Perkovic D., Keleher P. Online data-race detection via coherency guarantees // In Proceedings of the 2nd Symposium on Operating Systems Design and Implementation (OSDI'96). 1996. - P. 47-57.

31. Ball T., Rajamani S. The SLAM project: debugging system software via static analysis // In Proceedings of the 29th ACM SIGPLAN-SIG ACT Symposium on Principles of Programming Languages (POPL'02). -ACM Press, 2002. C. 1-3.

32. Das M. Unification-based pointer analysis with directional assignments // In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI'00). ACM Press, 2000. - P. 35-46.

33. Chase D. R., Wegman M., Zadeck F. K. Analysis of pointers and structures. In Proceedings of the SIGPLAN '90 Conference on Programming Language Design and Implementation. 1990. - P. 296-310.

34. Orlovich M. On flow-insensitive points-to analyses Электронный ресурс. — Режим дост.:http://www.cs.cornell.edu/courses/cs7 1 l/2005fa/slides/s ер 1 3 .pdf

35. Кудрин М.Ю., Соколов Е.В., Тормасов А.Г. Выявление состояний гонки с помощью графа совместного исполнения потоков // Научно-технические ведомости СПбГПУ, Серия

36. Информатика, телекоммуникации, управление». — СПб.: Изд-во Политехи, ун-та, 2009. № 5 (83). - С. 125-134.

37. Заборовский Н.В., Тормасов А.Г. Моделирование многопоточного исполнения программы и метод статического анализа кода на предмет состояний гонки // Прикладная информатика — М.: 2011, №4(34). С. 105-110.

38. Заборовский Н.В., Торлгасов А.Г. Расчетный подход к статическому анализу программного кода на предмет наличия состояний гонки // Программная инженерия М.: 2011, №7. - С.46-54.

39. Заборовский Н.В., Тормасов А.Г. Статическое обнаружение гонок в коде, содержащем ветвления и циклы // Прикладная информатика — М.: 2011, №6(36).- С. 75-87.

40. Заборовский Н.В., Тормасов А.Г. Подход к нахождению состояния гонки в практических многопоточных программах // Сборник научных трудов «Математические модели и задачи управления»- М.: МФТИ, 2011. С. 198-207.

41. Кудрин М.Ю. Выявление состояний гонки с помощью графа совместного исполнения потоков // Материалы международной научно-технической конференции «Компьютерные науки и технологии» — Белгород: Изд-во БелГУ, 2009. С. 45-46.

42. Прокопенко A.C. Обнаружение состояний гонки в потоках, работающих на разделяемой памяти // Модели и методы обработки информации, сборник научных трудов М.: МФТИ, 2009. - С. 93-98.

43. Кудрин М.Ю., Соколов Е.В. Выявление состояний гонки с помощью аппарата атрибутных грамматик // Научное творчество молодежи. Материалы XIII Всероссийской научно-практической конференции. -Кемерово: Кемеровский гос. универ-т, 2009. — С. 112.

44. Purcell С., Harris Т. Non-blocking hashtables with open addressing. University of Cambridge, 2005.

45. Intel Architecture Software Developer's Manual. -Volume 1- 3 Электронный ресурс. Режим дост.: http ¡//download .intel .с om/design/intarch/manuals/243 1 9 101.pdf

46. Klein P. N., Lu H., Netze R. Detecting Race Conditions in Parallel Programs that Use Semaphores. -Lecture Notes in Computer Science. Springer Berlin/Heidelberg, 2008.

47. Fraser K. Practical lock-freedom. University of Cambridge, 2004.

48. Slonneger K., Kurtz B. Formal syntax and semantics of programming languages. — Addison-Wesley, 1995.5 1. Серебряков В.А., Галочкин М.П., Гончар Д.P., Фуругян М.Г. Теория и реализация языков программирования. М. : МЗ Пресс, 2006.

49. Herlihy М. Impossibility and Universality Results for Wait Free Synchronization // Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, 1988. - P. 276-290.

50. Заборовский H.B. Подход к моделированию вычислений в нескольких потоках // Сборник тезисов 5-й международной конференции им. П.Л. Чебышева — Обнинск: МИФИ, 2011. С. ИЗ.

51. Заборовский Н.В. Моделированиефункциональности системного реестра ОС Windows для использования в виртуализо ванных системах // Сборник тезисов XXXV Гагаринских чтений. — М. МАТИ: 2009. С. 126-127.

52. Заборовский Н.В. Сборник тезисов XVI Международной научной конференции студентов, аспирантов и молодых учёных «Ломоносов-2009», секция «Вычислительная математика и кибернетика». М.:МГУ, 2009 - С. 31-32.

53. Заборовский Н.В., Пепгров В.Н. Разработка и реализация технологии шаблонного хранения данных в реестре Windows // Современные проблемы фундаментальных и прикладных наук. Часть VII.

54. Прикладная математика и экономика: Труды XLIX научной конференции. /Моск. физ. — техн. ин-т. — М.- Долгопрудный, 2006. С. 55.

55. Заборовский Н.В. Поиск состояния гонки в многопоточных алгоритмах // Современные проблемы фундаментальных и прикладных наук. Часть VII. Прикладная математика и экономика: Труды LIII научной конференции. /Моск. физ. — техн. ин-т. — М.

56. Долгопрудный, 2010. С. 164.

57. Заборовский Н.В. Моделирование реестра ОС Windows для использования в виртуализованных системах // Сборник научных трудов «Модели и методы обработки информации» М.:МФТИ, 2009. -С. 194-197.

58. Barnes G. A method for implementing lock-free shared data structures // Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures. — Velen, Germany, 1993. P. 261-270.

59. Gao H., Hessel ink W. H. A general lock-free algorithm using compare-and-swap. — Information and Computation, February, 2007. P. 225-241.

60. Herlihy M. A methodology for implementing highly concurrent data objects // ACM Transactions on Programming Languages and Systems (TOPLAS). November, 1993. P. 745-770.