Статический анализ гонок в программах на разделяемой памяти тема диссертации и автореферата по ВАК РФ 05.13.18, кандидат физико-математических наук Прокопенко, Артем Сергеевич

• Прокопенко, Артем Сергеевич
• кандидат физико-математических наук
• 2010

Оглавление диссертации кандидат физико-математических наук Прокопенко, Артем Сергеевич

Введение.

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

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

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

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

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

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

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

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

1.1. Обзор основных типов современных параллельных вычислительных систем.

Классификация параллельных архитектур.

Современные направления развития параллельных вычислительных систем.

Параллельные системы.

Взаимодействие потоков через разделяемую память.

1.2. Состояние гонки.

Методы синхронизации.

Синхронизация с блокировками.

Неблокирующаяся синхронизация.

Транзакционная память.

1.3. Обзор методов проверки правильности выполнения программ.

Экспертиза.

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

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

Формальные методы.

1.4 Классификация моделей.

Исполнимые модели.

Ограничительные модели.

Аксиоматические модели.

Дополнительные виды моделей.

1.5. Классификация формальных методов.

Методы проверки моделей.

Методы дедуктивного анализа.

Выводы.

Глава 2. Математическая модель.

2.1. Математическая модель.

2.2. Сепарационная логика.

2.4. Синтаксис языка программирования.

2.5. Операционная семантика.

2.6 Утверждения. Формулы и аксиомы утверждений.

Глава 3. Метод верификации.

3.1 Обзор метода верификации Ке1у-Сиагап1ее.

Комбинирование ЯЮ и СБЬ.

Метод Шл8ер и БАвЬ.

Метод 1Жт.

3.2. Переходы.

3.4. Аксиомы и правила вывода.

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

Глава 4. Спецификация формулы корректности.

4.1. Использование ЬТЬ логик для задания формулы корректности.

4.2. Общая схема проведения анализа.

4.3. Оценка сложности анализа на наличие гонок в параллельных программах.

Глава 5. Примеры анализа многопоточных алгоритмов.

5.1 Неблокирующаяся реализация алгоритма стека.

5.2. Неблокирующаяся реализация алгоритма очереди.

5.3 Алгоритм «булочной».

Глава 6. Автоматизация.

БтаПйкЛЯО.

Обзор среды ЬаЬеПе/НОЬ.

Описание комплекса программ.

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

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

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

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

В целом проверка соответствия между требованиями к системе и свойствами работающей системы (верификация) является нетривиальной задачей. Различают два принципиально разных подхода — динамический и статический. Динамическая верификация представляет собой эмпирическую процедуру «прогона» программы при различных входных данных. Проверить сложную систему тестированием обычно невозможно, поскольку количество тестов экспоненциально зависит от размера входа, да и само число различных комбинаций входных данных в программу может быть в целом не ограничено. В итоге, несмотря на применение различных техник, отчетам динамических анализаторов свойственно большое количество ложных заключений о правильности программ.

Проверка на основе моделей (model checking) и дедуктивная верификация, относящиеся к статическим формальным методам, реализуют статический подход альтернативный динамическому. Главными проблемами верификации на основе моделей являются сложность построения модели параллельных программ и «комбинаторный взрыв» в пространстве состояний системы, иначе говоря, значительный рост объема проверок даже при небольшом усложнении комплекса программ. В этом отношении выгодно отличается дедуктивная верификация, когда посредством формальной логики устанавливается соответствие результата выполнения программы представленной спецификации. Метод R/G-Rely/Guarantee (Jones, 1983)[68] зарекомендовал себя как качественный метод верификации параллельных программ, когда спецификация параллельных программ может быть разбита на отдельные свойства, описывающие поведение небольших фрагментов системы, и может быть применима стратегия проверки каждого локального свойства, используя только тот фрагмент системы, который описывается лишь этим свойством. Допустим, что имеются п потоков Ti,T2,.Tn, исполняющихся одновременно. Поскольку поведение потока Ti зависит от поведения других потоков, именуемых средой, пользователь 'формулирует ряд допущений (Rely), которые должны выполняться средой, для того чтобы гарантировать корректность потока Ti. Поведение среды также зависит от поведения потока Ть пользователь формулирует ряд допущений (Guarantee), которые должны выполняться потоком, для того чтобы гарантировать корректность выполнения среды. Построив должным образом комбинацию допущений потоков, можно установить правильность всей системы TijjT^H - - - j[Tn.

Однако посредством оригинального метода R/G можно проводит анализ наличия гонок лишь в простых типах программ (в программах без указателей, без локальной памяти потоков и т.д.). В целях улучшения применимости метода R/G к верификации многопотоковых программ созданы три метода дедуктивной верификации: SAGL[63], RGSep[105] и LRG[64]. Эти методы различаются как по математической модели, так и по типам программ, которые они способны верифицировать. Наиболее активно развиваются два: RGSep и LRG. Единственным серьезным преимуществом метода LRG перед RGSep является возможность верификации программ, в которых одни потоки имеют совместно используемые области данных, скрытее от других потоков. В прочих компонентах метод RGSep более проработан, это выражается в возможности верификации методом RGSep свойств живучести (живости, liveness). Он требует меньше усилий для верификации компонентов системы в различных окружениях за счет исследования устойчивости слабейших предусловии и слабейших постусловия под влиянием окружения; определенные шаги метода автоматизированы. Для того, что нивелировать недостатки одного из методов, приходиться использовать оба. Сейчас, например, если необходимо проверить дедуктивным методом библиотечную функцию, создающую при выполнении несколько потоков, на отсутствие гонок, термируемость, то надо использовать и RGSep, и LRG, что фактически означает проведение двойной работы по спецификации, формальному доказательству (выводу последовательности формул). Для того чтобы в подобных ситуациях использовать один метод, необходимо нивелировать ряд недостатков в методах R/G, RGSep, а именно:

• несколько потоков могут иметь совместно используемые ячейки памяти, скрытые от других потоков. В рамках методов R/G, RGSep, SARG нет возможности скрыть эти ячейки от других потоков, что может привести к ложному отчету о корректности программы;

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

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

Целью диссертационной работы является создание метода статического анализа условий гонок многопоточных алгоритмов, основанного на RGSep-методе, для верификации параллельных программ, в которых некоторые потоки имеют совместно используемые области памяти скрытые от других потоков, а также проведение вычислительных экспериментов для исследования прикладных аспектов этого метода. Задачи исследования:

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

2. Разработка метода задания формулы частичной корректности, специфицирующей состояние гонки;

3. Разработка метода анализа наличия гонок, используя расширение аксиоматического метода верификации Rely/Guarantee и сепарационной логики;

4. Оценка сложности алгоритма анализа гонок в параллельных программах на общей памяти в различных случаях;

5. Использование предложенного подхода и соответствующих вычислительных экспериментов для выявления состояния гонки в тестовых параллельных программах на разделяемой памяти;

6. Создание комплекса программ для автоматизации выявления совместно используемых потоками данных, декомпозиции «крупных» команд на атомарные инструкции.

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

Научная новизна работы заключается в предложенной методике формализации и анализа состояния гонки в параллельных программах на разделяемой памяти, базирующейся на аксиоматическом методе верификации R/G и сепарационной логике. По сравнению с известными формальными методами верификации Rely/Guarantee и RGSep данный подход обладает следующими достоинствами:

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

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

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

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

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

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

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

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

4. Вычислительные эксперименты для комплексного исследования наличия гонок в параллельных программах на общей памяти на основе предложенной методики с использование разработанного комплекса программ.

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

По теме диссертации опубликовано 10 работ, в том числе две [1,2] - в изданиях, рекомендованных ВАК РФ.

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

• IX международная научно-практическая конференция «Исследование, разработка и применение высоких технологий в промышленности» (Санкт-Петербург, 2010 г.);

• Седьмая международная научная молодежная школа «Высокопроизводительные вычислительные системы ВПВС-2010»,

• (Дивноморское, 2010 г.);

• Международная научно-техническая конференция "Многопроцессорные вычислительные и управляющие системы 2009" (Дивноморское, 2009 г.);

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

• XLIX и L научные конференции МФТИ (Москва, 2006, 2007 гг.);

• Научные семинары кафедры информатики МФТИ (Москва, 20082010 гг.).

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

Диссертация состоит из Введения, шести глав, Заключения и Списка использованных источников, включающего 105 наименований. Общий объем работы составляет 107 страниц текста.

Список литературы диссертационного исследования кандидат физико-математических наук Прокопенко, Артем Сергеевич, 2010 год

1. Акишев, И.Р. Разработка и анализ параллельных поисковых структур данных, нечувствительных к размеру кеша / И.Р. Акишев. -Бакалаврская работа. Кафедра компьютерных технологий. -СПбГУИТМО, 2008. Режим доступа: http://is.ifmo.ru/present/

2. Norrish, M. С formalized in HOL / M. Norrish. PhD thesis. Univ. of Cambridge. Computer Lab., 1998. - 57 p.

3. Vafeiadis V. Modular fine-grained concurrency verification. PhD thesis. -Univ. of Cambridge. Computer Lab., 2008. 148 p.Монографии

4. Алешина, H.A. Логика и компьютер. Моделирование рассуждений и проверка правильности программ / H.A. Алешина, A.M. Анисов, П.И. Быстрое. М.: Наука, 1990. - 240 с.

5. Кларк, Э.М. Верификация моделей программ: Model Checking / Э.М. Кларк, О. Грамберг, Д. Пелед / ред. Р. Смелянский. М.: МЦНМО, 2002.-416 с.

6. Бройдо В.Л., Ильина О.П, Архитектура ЭВМ / В.Л. Бройдо, О.П. Ильина. М.: Научный мир, 2005. - 272 с.

7. Левин, М.П. Параллельное программирование с использованием ОрепМР / М.П. Левин. М.: Интернет-Университет Информационных Технологий. БИНОМ. Лаборатория знаний, 2008. - 118 с. - Лит.: С. 113-118.

8. Бурдонов, И.Б. Обзор подходов к верификации распределенных систем / И.Б. Бурдонов, A.C. Косачев, В.Н. Пономаренко, В.З. Шнитман. М.: ИСП РАН, 2003. - 52 с. - Ли.: С. 49-52.

9. Гуц, А.К. Математическая логика и теория алгоритмов: Учебное пособие. Омск: Наследие, 2003. - 108 с. - Лит.: С. 105-108.Ю.Дейкстра, Э. Дисциплина программирования / Э. Дейкстра. М.: «Мир», 1978. - 275 с.

10. Игошин, В.И. Математическая логика и теория алгоритмов: учебное пособие / В.И. Игошин. М.: «Академия», 2008. - 448 с. - Лит.: С. 435442.

11. Серебряков, В.А. Теория и реализация языков программирования / В.А. Серебряков, М.П. Галочкин, Д.Р. Гончар, М.Г. Фуругян. М.: МЗ-Пресс, 2003. - 296 с.

12. Хоар, Ч. Взаимодействующие последовательные процессы / Ч. Хоар. -М.: Мир, 1989.-264 с. -Избр. лит.: С. 254.

13. Intel Architecture Software Developer's Manual. Volume 1. - 244 p. -Режим доступа: http://www.intel.com/Assets/PDF/manual/245317.pdf

14. Fraser, К. Practical lock-freedom / K. Fraser . — University of Cambridge, 2004.-116 p.

15. Herlihy, M. The Art of Multiprocessor Programming / M. Herlihy, N. Shavit. Elsevier: Morgan Kaufmann, 2008. - 508 p.

16. Reed, J.N. Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development // J.N. Reed, J.E. Sinclair, F. Guigard. Oxford Brookes, 1999.

17. Использование Thread Analyzer для поиска конфликтов доступа к данным. Режим доступа:http://ru.sun.com/developers/sunstudio/articles/tha using ru. html

18. Калугин, А. Верификатор программ на языке Си LINT / А. Калугин. -Режим доступа: http://www.viva64.com/go.php?url=224

19. Карпов, А. Что такое "Parallel Lint"? / А. Карпов. Режим доступа: http://software.intel.com/ru-ru/articles/parallel-lint/

20. Карпов, А. Тестирование параллельных программ / А. Карпов. -Режим доступа: http://www.softwaretesting.ru/library/testing/functionaltesting/5 81 -parallelprogramtesting

21. Прокопенко A.C. Дедуктивный метод анализа логических гонок с использованием сепарационной логики/Прокопенко A.C., Тормасов А.Г. // Труды МФТИ. — М.,2010. Т.2. № 3. - С. 175-184.

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

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

24. Кулямин, В. В. Интеграция методов верификации программных систем. Режим доступа: http://panda.ispras.ru/~kuliamin/docs/IntVer-2009-ru.pdf

25. Патил, Рахул В. и Джордж, Б. Средства и приемы для выявления проблем параллельного выполнения / Рахул В. Патил, и Б. Джордж //Журнал MSDN Magazine. 2008. - Июнь. - Режим доступа: http://msdn.microsoñ.com/ru-ru/magazine/cc546569.aspx

26. Adve S. V. Shared memory consistency models: A tutorial / S. V. Adve, K. Gharachorloo // Computer. 1996. - Vol. 29. - № 12. - 32 p. - Режим доступа: http://www.hpl.hp.com/techreports/Compaq-DEC/WRL-95-7.pdf

27. Arora, N.S. Thread scheduling for multiprogrammed multiprocessors /N.S. Arora, R.D. Blumofe, and C.G. Plaxton // Proc. of the Tenth Annual ACM Symposium on Parallel Algorithms and Architectures. ACM Press, 1998. -P. 119-129.

28. Balasundaram, V. Compile -time detection of race conditions in a parallel program / V. Balasundaram , K. Kennedy // Proceedings of the 3rd International conference on Supercomputing. Crete (Greece), 1989. - P. 175-185.

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

30. Barnes, G. A method for implementing lock -free shareddata structures / G. Barnes Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures. Velen (Germany), 1993. - P. 261-270.

31. Berdine, J. Symbolic execution with separation logic / J. Berdine, C. Calcagno, and Peter W. O'Hearn // APLAS. Vol. 3780 of Lecture Notes in Computer Science. 2005. - Springer. - P. 52-68.

32. Bach, M. The design of the UNIX operating system / M. Bach // Software. Series. Sec 5. 12.-Prentice-Hall, 1986.-P. 111-119.

33. Bodden, E. Racer: effective race detection using AspectJ / E. Bodden, K. Havelund. ISSTA, 2008. - Режим доступа: http://www.havelund.com/Publications/issta2008.pdf

34. Bornat, R. Permission accounting in separation logic / R. Bornat, C. Calcagno, P. W. O'Hearn, and M. J. Parkinson // 32nd ACM Symposium onPrinciples of Programming Languages (POPL 2005). ACM. 2005. - P. 259-270.

35. Bornat, R. Variables as resource in separation logic / R. Bornat, C. Calcagno, and H. Yang // Electronic Notes in Theoretical Computer Science. 2006. - 155. - P. 247-276.

36. Brookes, St. D. A semantics for concurrent separation logic // St. D. Brookes // 15th International Conference on Concurrency Theory (CONCUR). Vol. 3170 of Lecture Notes in Computer Science r. Springe. -2004.-P. 16-34.

37. Brookes, St. D. Variables as resource for shared-memory programs: Semantics and soundness / St. D. Brookes // Electronic Notes in Theoretical Computer Science. 2006. - 158. - P. 123-150.

38. Calcagno, C. Modular safety checking for fine-grained concurrency / C. Calcagno, M. Parkinson, and V. Vafeiadis // 14th International Static Analysis Symposium (SAS 2007). Vol. 4634 of Lecture Notes in Computer Science. 2007. - August. - P. 233-238.

39. Chase, D.R. Analysis of pointers and structures / D.R. Chase, M. Wegman, and F. K. Zadeck // Proceedings of the SIGPLAN '90 Conference on Programming Language Design and Implementation. June 1990. - P. 296310.

40. Cliff, B. J. Wanted: a compositional approach to concurrency / B,J. Cliff // Programming Methodology. Springer-Verlag. - 2003. - P. 5-15.

41. Cliff, B.J. Specification and design of (parallel) programs / B.J. Cliff // IFIP Congress. 1983. - P. 321-332.

42. Coleman, J. W. A structural proof of the soundness of rely/guarantee rules / J.W. Coleman and B.J. Cliff // Technical Report CS-TR-987. School of Computing Science. Newcastle University. - 2006. - October. - P. 807841.

43. Deutsch, A. Interprocedural May-Alias Analysis for Pointers : Beyond k-limiting / A. Deutsch // Proc. Programming Language Designand Implementation. ACM Press. 1994. - Vol. 29. - № 6. - P. 230-241.

44. Dodds, M. Deny-guarantee reasoning / M. Dodds, X. Feng, M. Parkinson, and V. Vafeiadis // Proc. ESOP. 2009. - P. 363-377.

45. Emanuelsson, P. A Comparative Study of Industrial Static Analysis Tools / P. Emanuelsson, U. Nilsson. Elsevier Science Publishers В. V. Amsterdam, The Netherlands, The Netherlands, 2008. Vol. 217. - P. 5-21.

46. Farzan, A. Algorithms for Atomicity / A. Farzan, P. Madhusudan. 2007.- Режим доступа:http ://scholar. google. com/scholar?q=25 .%09Farzan,+A.+Algorithms+forhA tomicity&hl=en&assdt=0&asvis=l&oi=scholart

47. Feng, X. Local rely-guarantee reasoning / X. Feng // ACM Symposium on Principles of Programming Languages. — 2009. P. 315-327.

48. Feng, X. On the relationship between concurrent separation logic and assume-guarantee reasoning / X. Feng, F. Rodrigo, S. Zhong // Proc. 16th European Symp. on Prog. (ESOP'07). Lecture Notes in Computer Science.- 2007.-Vol. 4421.-P. 173-188.

49. Flanagan, С. Types for atomicity / C. Flanagan and Sh. Qadeer // ACM Workshop on Types in Language Design and Implementation. ACM. -2003. January. - P. 1-12.

50. Gao, H. A general lock-free algorithm using compare-and-swap / H. Gao , W.H. Hesselink // Information and Computation, February, 2007. P. 225241.

51. Gotsman, A. Proving that non-blocking algorithms don't block / A. Gotsman, B. Cook, M. Parkinson, V. Vafeiadis // Proc. 36th ACM. Symp. on Principles of Prog. Lang. (POPL'09). ACM Press. - 2009. - P. 16-28.

52. Jones, C. Specification and design of (parallel) programs / C. Jones // Proceedings ofIFIP'83. -North-Holland, 1983. -P. 321-332.

53. Jones, C. Wanted: a compositional approach.to concurrency / C. Jones // In Programming Methodology, pages 5-15. Springer-Verlag, 2003.

54. Herlihy, M. Impossibility and Universality Results for Wait / M. Herlihy // . Free Synchronization, Proceedings of the seventh annual ACM Symposiumon Principles of distributed computing, 1988. — P. 276-290.

55. Herlihy, M.P. Linearizability: a correctness condition for concurrent objects // M.P. Herlihy and. J.M. Wing // ACM Transactions onProgramming Languages and Systems (TOPLAS). 1990. - Vol. 12. - № 3.-P. 463-492.

56. Herlihy, M.P. Wait-free synchronization / M.P. Herlihy // ACM Transactions on Programming Languages and Systems (TOPLAS). 1991. -13(1).-P. 124-149.

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

58. Herlihy, M.P. Obstruction-free synchronization: Double-ended queues as an example / M.P. Herlihy, V. Luchangco, and M. Moir // 23rd IEEE International Conference on Distributed Computing Systems. — 2003. -May.-P. 522-529.

59. Herlihy, M. A lock-free concurrent skiplist with wait-free search / M. Herlihy, Y. Lev, N. Shavit. Unpublished Manuscript. Sun Microsystems Laboratories. Burlington (Massachusetts), 2007.

60. Hoare, C.A.R. An axiomatic basis for computer programming / C.A.R. Hoare // Communications ACM. 1969. - Vol. 12. - № 1. - P. 576-580.

61. Hussak, W. Specifyning Strict Serializability of Iterated Transactions in Propositional Temporal Logic / W. Hussak // International Journal of Computer Science. 2007. - Vol. 2. - № 2. - Режим доступа: http ://www.ij csi.org/

62. Marginean, P. Lock-Free Queues / P. Marginean // Dr. Dobb's Journal. -July 2008. P. 43- 47. - Режим доступа:http://www.nxtbook.com/nxtbooks/cmp/ddj0708/index.php?startid=43#/46

63. McKenney, P.E. Selecting locking primitives for parallel programming / P.E. McKenney // Communications of the ACM. ACMPress. 1996. - Vol. 39. - № 10. - P. 75-82. - Режим доступа: http://portal.acrn.org/citation.cfm?id=236156.236174

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

65. Michael, M.M. Simple, fast, and practical nonblocking and blocking concurrent queue algorithms / M.M. Michael, M.L. Scott // Proc. of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing. ACM Press, 1996. - P. 267-275.

66. Mostefaoui, A. The combined power of conditions and failure detectors to solve asynchronous set agreement / A. Mostefaoui, S. Rajsbaum, M. Raynal // Proceedings of Symposium on Principles of Distributed Computing. ACM. Germany, 2005. - P. 179-188.

67. Li, M. How to share concurrent wait-free variables / M. Li, J. Tromp, and P.M.B. Vitanyi // Journal of the ACM. 1996. -Vol. 43. - № 4. - P. 723746.

68. Luchangco, V. Nonblocking k-compare-single-swap / V. Luchangco, M. Moir, N. Shavit // Proceedings of the fifteenth annual ACM symposium on Parallel algorithms and architectures. San Diego, 2003. - P. 314-323.

69. Naik, M. Effective Static Race Detection for Java / M. Naik, A. Aiken, J. Whaley // ACM SIGPLAN Notices. Proceedings of the 2006. PLDI Conference. 2006. - Vol. 41. - № 6. - P. 308-319.

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

71. Purcell, С. Non-blocking hashtables with open addressing / C. Purcell, T. Harris. — University of Cambridge, 2005. Режим доступа: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-639.html

72. Reynolds, С. Separation logic: A logic for shared mutable data structures / C. Reynolds // Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02). IEEE Computer Society, 2002. - P. 55-74.

73. Michiel Ronsse, Koen De Bosschere, Non-Intrusive on-the-Fly Data Race Detection Using Execution Replay, Automated And Algorithmic Debugging: Proceedings of the IVIW on AD. Vol. I. Germany, 2000.

74. Qadeer, S. KISS: keep it simple and sequential / S. Qadeer, D. Wu. PLDI, 2004. - Режим доступа: http://faculty.ist.psu.edu/wu/papers/kiss.pdf

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

76. Scott, M.L. Non-blocking timeout in scalable queue-based spin locks / M.L. Scott // PODC Гf02: Proc. of the Twenty-first Annual Symposium on Principles of Distributed Computing. ACM Press. N.-Y., 2002. - P. 3140.

77. Shavit, N., Touitou, D. Software transactional memory / N. Shavit, D. Touitou // Proceedings of the 14th ACM Symposium on Principles of Distributed Computing. ACM. NY, 1995. - P. 204-213.

78. Steensgaard, B. Points-to Analysis in Almost Linear Time / B. Steensgaard // ACM POPL. 1996. - P. 1-10. - Режим доступа: http://www.cs.cornell.edu/courses/cs71 l/2005fa/papers/steensgaard-popl96.pdf