Прогнозирующий анализ во время выполнения

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

Обзор

Неофициально, при казни $t$ , прогнозный анализ проверяет ошибки в переупорядоченной трассировке $t'$ из $t$ . $t'$ называется допустимым из $t$ (альтернативно правильное переупорядочение ^[2] из $t$ ) если какая-либо программа, способная генерировать $t$ также может генерировать $t'$ .

В контексте параллельных программ метод прогнозирования является правильным , если он прогнозирует только ошибки параллелизма при возможных выполнениях причинной модели наблюдаемой трассировки. Предполагая, что при анализе нет сведений об исходном коде программы, анализ считается полным (также называемым максимальным). ^[3]^[4]), если выведенный класс выполнения содержит все выполнения, которые имеют одинаковый порядок программы и префикс порядка связи наблюдаемой трассировки.

Приложения

Прогнозный анализ применяется для обнаружения широкого класса ошибок параллелизма, в том числе:

Гонки данных
Тупики ^[5]^[6]^[7]
атомарности Нарушения ^[8]
Нарушения порядка, например, использования после освобождения. ошибки ^[9]

Выполнение

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

Объединение данных и анализ потока управления

Статический анализ может быть сначала проведен для сбора данных и информации о зависимости потока управления исходной программы, что может помочь построить причинно-следственную модель во время онлайн-выполнения. Это позволяет прогнозному анализу вывести более широкий класс выполнения на основе наблюдаемого выполнения. Интуитивно понятно, что возможное переупорядочение может изменить последнего записывающего устройства чтения памяти (зависимость данных), если чтение, в свою очередь, не может повлиять на выполнение каких-либо обращений (зависимость управления). ^[10]^[11]

Подходы

Методы частичного порядка

Методы частичного порядка чаще всего используются для обнаружения гонок в Интернете. Во время выполнения создается частичный порядок событий в трассировке, и о любых неупорядоченных парах критических событий сообщается как о гонках. Многие методы прогнозирования для обнаружения рас основаны на отношении «произошло до» или его ослабленной версии. Такие методы обычно могут быть эффективно реализованы с помощью алгоритмов векторных часов, допускающих только один проход всей входной трассы во время ее создания, и, таким образом, подходят для онлайн-развертывания. ^[2] ^[12] ^[13]

Методы на основе SMT

Кодировки SMT позволяют при анализе извлечь уточненную причинно-следственную модель из трассировки выполнения в виде (возможно, очень большой) математической формулы. Кроме того, в модель может быть включена информация о потоке управления. Методы, основанные на SMT, могут обеспечить надежность и полноту (также называемую максимальной причинностью). ^[4] ^[3]), но имеет экспоненциальную сложность по отношению к размеру трассировки. На практике анализ обычно применяется к ограниченным сегментам трассировки выполнения, таким образом, полнота обменивается на масштабируемость. ^[10] ^[14] ^[15] ^[16]

Подходы на основе Lockset

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

Методы, основанные на графах

В контексте обнаружения гонки данных был разработан надежный анализ с прогнозированием за полиномиальное время с хорошими, близкими к максимальным, возможностями прогнозирования на основе графиков. ^[18]

Вычислительная сложность

Учитывая входной след размера $n$ исполнен $k$ потоков, общий прогноз гонки является NP-полным и даже W[1] -жестким параметризованным $k$ , но допускает алгоритм с полиномиальным временем, когда топология связи ациклична. ^[19] Происходит до того, как расы будут обнаружены в $O(n\cdot k)$ время, и эта оценка оптимальна. ^[20] Lockset мчится вперед $d$ переменные обнаруживаются в $O(n\cdot d)$ времени, и эта оценка также оптимальна. ^[20]

Инструменты

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

"Стремительный" . Гитхаб . : облегченная платформа для реализации механизмов динамического обнаружения гонок.
«РоудРаннер» . Гитхаб . : среда динамического анализа, предназначенная для быстрого создания прототипов и экспериментов с динамическим анализом параллельных Java-программ.
«РВ-Прогноз» . : прогнозирующее обнаружение гонок на основе SMT.
«НЛО» . Гитхаб . : прогнозируемое использование после освобождения на основе SMT.

См. также

Ссылки

^ «Прогнозирующий анализ времени выполнения» . 10 ноября 2008 г.
^ Перейти обратно: ^а ^б Смарагдакис, Яннис; Эванс, Джейкоб; Садовски, Кейтлин; Йи, Джехон; Фланаган, Кормак (2012). «Надежное прогнозирующее обнаружение расы за полиномиальное время». Уведомления ACM SIGPLAN . 47 (1): 387. дои : 10.1145/2103621.2103702 . ISSN 0362-1340 .
^ Перейти обратно: ^а ^б Шербанута, Траян Флорин; Чен, Фэн; Рошу, Григоре (2013). «Максимальные причинные модели для последовательно согласованных систем». Проверка времени выполнения . Конспекты лекций по информатике. Том 7687. С. 136–150. два : 10.1007/978-3-642-35632-2_16 . hdl : 2142/27708 . ISBN 978-3-642-35631-5 . ISSN 0302-9743 .
^ Перейти обратно: ^а ^б ^с Хуанг, Джефф (2015). «Модель без гражданства, проверяющая параллельные программы с максимальным уменьшением причинности». Материалы 36-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 165–174. дои : 10.1145/2737924.2737975 . ISBN 9781450334686 . S2CID 15196006 .
^ Калхауге, Кристиан Грам; Палсберг, Йенс (2018). «Звучное предсказание тупиковой ситуации» . Труды ACM по языкам программирования . 2 (OOPSLA): 1–29. дои : 10.1145/3276516 . ISSN 2475-1421 .
^ «Надежное динамическое прогнозирование тупиковой ситуации в линейном времени» (PDF) .
^ Тунч, Хюнкар Джан; Матур, Уманг; Павлояннис, Андреас; Вишванатан, Махеш (2023), «Звуковое динамическое прогнозирование тупиковой ситуации в линейном времени» , Proceedings of ACM on Programming Languages , 7 : 1733–1758, doi : 10.1145/3591291 , получено 29 сентября 2023 г.
^ «Проверка атомарности в линейном времени с использованием векторных часов» (PDF) .
^ Хуанг, Джефф (2018). "НЛО". Материалы 40-й Международной конференции по программной инженерии . стр. 609–619. дои : 10.1145/3180155.3180225 . ISBN 9781450356381 . S2CID 3730958 .
^ Перейти обратно: ^а ^б Хуанг, Джефф; Мередит, Патрик О'Нил; Рошу, Григоре (2013). «Максимально надежное прогнозируемое обнаружение гонок с абстракцией потока управления». Материалы 35-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 337–348. дои : 10.1145/2594291.2594315 . ISBN 9781450327848 . S2CID 8883624 .
^ Генч, Каан; Ремер, Джейк; Сюй, Юфань; Бонд, Майкл Д. (2019). «Обнаружение гонок с учетом зависимостей и неограниченным звуком» . Труды ACM по языкам программирования . 3 (OOPSLA): 1–30. arXiv : 1904.13088 . дои : 10.1145/3360605 . ISSN 2475-1421 .
^ Кини, Дилип; Матур, Уманг; Вишванатан, Махеш (2017). «Динамический прогноз гонок в линейном времени». Материалы 38-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 157–170. arXiv : 1704.02432 . дои : 10.1145/3062341.3062374 . ISBN 9781450349888 . S2CID 6855894 .
^ Ремер, Джейк; Генч, Каан; Бонд, Майкл Д. (2018). «Обнаружение гонок с высоким охватом и неограниченным звуком». Материалы 39-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 374–389. дои : 10.1145/3192366.3192385 . ISBN 9781450356985 . S2CID 47018225 .
^ Лю, Пэн; Трипп, Омер; Чжан, Сянюй (2016). «IPA: улучшение прогнозного анализа с помощью анализа указателей». Материалы 25-го Международного симпозиума по тестированию и анализу программного обеспечения . стр. 59–69. дои : 10.1145/2931037.2931046 . ISBN 9781450343909 .
^ Ван, Чао; Кунду, Судипта; Ганай, малайский; Гупта, Аарти (2009). «Символический прогнозный анализ для параллельных программ». FM 2009: Формальные методы . Конспекты лекций по информатике. Том. 5850. стр. 256–272. дои : 10.1007/978-3-642-05089-3_17 . ISBN 978-3-642-05088-6 . ISSN 0302-9743 .
^ Саид, Махмуд; Ван, Чао; Ян, Цзыцзян; Сакалла, Карем (2011). «Создание свидетелей гонки данных с помощью анализа на основе SMT». Формальные методы НАСА . Конспекты лекций по информатике. Том. 6617. стр. 313–327. дои : 10.1007/978-3-642-20398-5_23 . ISBN 978-3-642-20397-8 . ISSN 0302-9743 .
^ Сэвидж, Стефан; Берроуз, Майкл; Нельсон, Грег; Собальварро, Патрик; Андерсон, Томас (1997). «Ластик» . Транзакции ACM в компьютерных системах . 15 (4). Ассоциация вычислительной техники (ACM): 391–411. дои : 10.1145/265924.265927 . ISSN 0734-2071 . S2CID 1492924 .
^ Павлояннис, Андреас (2020). «Быстрое, надежное и эффективное динамическое предсказание гонок» . Труды ACM по языкам программирования . 4 (ПОПЛ): 1–29. arXiv : 1901.08857 . дои : 10.1145/3371085 . ISSN 2475-1421 .
^ Матур, Уманг; Павлояннис, Андреас; Вишванатан, Махеш (2020). «Сложность прогнозирования динамической гонки данных». Материалы 35-го ежегодного симпозиума ACM/IEEE по логике в информатике . Ассоциация вычислительной техники. стр. 713–727. arXiv : 2004.14931 . дои : 10.1145/3373718.3394783 . ISBN 9781450371049 . S2CID 210171694 .
^ Перейти обратно: ^а ^б Кулкарни, Руча; Матур, Уманг; Павлояннис, Андреас (2021). «Динамическое обнаружение гонок данных через мелкозернистую линзу» . 32-я Международная конференция по теории параллелизма (CONCUR 2021) . Международные труды Лейбница по информатике (LIPIcs). 203 . Замок Дагштуль - Центр информатики Лейбница: 16:1–16:23. doi : 10.4230/LIPIcs.CONCUR.2021.16 . ISBN 9783959772037 . S2CID 235765773 .

[1] «Прогнозирующий анализ времени выполнения» . 10 ноября 2008 г.

[SmaragdakisEvans2012-2] Перейти обратно: ^а ^б Смарагдакис, Яннис; Эванс, Джейкоб; Садовски, Кейтлин; Йи, Джехон; Фланаган, Кормак (2012). «Надежное прогнозирующее обнаружение расы за полиномиальное время». Уведомления ACM SIGPLAN . 47 (1): 387. дои : 10.1145/2103621.2103702 . ISSN 0362-1340 .

[ŞerbănuţăChen2013-3] Перейти обратно: ^а ^б Шербанута, Траян Флорин; Чен, Фэн; Рошу, Григоре (2013). «Максимальные причинные модели для последовательно согласованных систем». Проверка времени выполнения . Конспекты лекций по информатике. Том 7687. С. 136–150. два : 10.1007/978-3-642-35632-2_16 . hdl : 2142/27708 . ISBN 978-3-642-35631-5 . ISSN 0302-9743 .

[Huang2015-4] Перейти обратно: ^а ^б ^с Хуанг, Джефф (2015). «Модель без гражданства, проверяющая параллельные программы с максимальным уменьшением причинности». Материалы 36-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 165–174. дои : 10.1145/2737924.2737975 . ISBN 9781450334686 . S2CID 15196006 .

[KalhaugePalsberg2018-5] Калхауге, Кристиан Грам; Палсберг, Йенс (2018). «Звучное предсказание тупиковой ситуации» . Труды ACM по языкам программирования . 2 (OOPSLA): 1–29. дои : 10.1145/3276516 . ISSN 2475-1421 .

[6] «Надежное динамическое прогнозирование тупиковой ситуации в линейном времени» (PDF) .

[7] Тунч, Хюнкар Джан; Матур, Уманг; Павлояннис, Андреас; Вишванатан, Махеш (2023), «Звуковое динамическое прогнозирование тупиковой ситуации в линейном времени» , Proceedings of ACM on Programming Languages , 7 : 1733–1758, doi : 10.1145/3591291 , получено 29 сентября 2023 г.

[8] «Проверка атомарности в линейном времени с использованием векторных часов» (PDF) .

[Huang2018-9] Хуанг, Джефф (2018). "НЛО". Материалы 40-й Международной конференции по программной инженерии . стр. 609–619. дои : 10.1145/3180155.3180225 . ISBN 9781450356381 . S2CID 3730958 .

[HuangMeredith2013-10] Перейти обратно: ^а ^б Хуанг, Джефф; Мередит, Патрик О'Нил; Рошу, Григоре (2013). «Максимально надежное прогнозируемое обнаружение гонок с абстракцией потока управления». Материалы 35-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 337–348. дои : 10.1145/2594291.2594315 . ISBN 9781450327848 . S2CID 8883624 .

[GençRoemer2019-11] Генч, Каан; Ремер, Джейк; Сюй, Юфань; Бонд, Майкл Д. (2019). «Обнаружение гонок с учетом зависимостей и неограниченным звуком» . Труды ACM по языкам программирования . 3 (OOPSLA): 1–30. arXiv : 1904.13088 . дои : 10.1145/3360605 . ISSN 2475-1421 .

[KiniMathur2017-12] Кини, Дилип; Матур, Уманг; Вишванатан, Махеш (2017). «Динамический прогноз гонок в линейном времени». Материалы 38-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 157–170. arXiv : 1704.02432 . дои : 10.1145/3062341.3062374 . ISBN 9781450349888 . S2CID 6855894 .

[RoemerGenç2018-13] Ремер, Джейк; Генч, Каан; Бонд, Майкл Д. (2018). «Обнаружение гонок с высоким охватом и неограниченным звуком». Материалы 39-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . стр. 374–389. дои : 10.1145/3192366.3192385 . ISBN 9781450356985 . S2CID 47018225 .

[LiuTripp2016-14] Лю, Пэн; Трипп, Омер; Чжан, Сянюй (2016). «IPA: улучшение прогнозного анализа с помощью анализа указателей». Материалы 25-го Международного симпозиума по тестированию и анализу программного обеспечения . стр. 59–69. дои : 10.1145/2931037.2931046 . ISBN 9781450343909 .

[WangKundu2009-15] Ван, Чао; Кунду, Судипта; Ганай, малайский; Гупта, Аарти (2009). «Символический прогнозный анализ для параллельных программ». FM 2009: Формальные методы . Конспекты лекций по информатике. Том. 5850. стр. 256–272. дои : 10.1007/978-3-642-05089-3_17 . ISBN 978-3-642-05088-6 . ISSN 0302-9743 .

[SaidWang2011-16] Саид, Махмуд; Ван, Чао; Ян, Цзыцзян; Сакалла, Карем (2011). «Создание свидетелей гонки данных с помощью анализа на основе SMT». Формальные методы НАСА . Конспекты лекций по информатике. Том. 6617. стр. 313–327. дои : 10.1007/978-3-642-20398-5_23 . ISBN 978-3-642-20397-8 . ISSN 0302-9743 .

[Eraser-17] Сэвидж, Стефан; Берроуз, Майкл; Нельсон, Грег; Собальварро, Патрик; Андерсон, Томас (1997). «Ластик» . Транзакции ACM в компьютерных системах . 15 (4). Ассоциация вычислительной техники (ACM): 391–411. дои : 10.1145/265924.265927 . ISSN 0734-2071 . S2CID 1492924 .

[Pavlogiannis2020-18] Павлояннис, Андреас (2020). «Быстрое, надежное и эффективное динамическое предсказание гонок» . Труды ACM по языкам программирования . 4 (ПОПЛ): 1–29. arXiv : 1901.08857 . дои : 10.1145/3371085 . ISSN 2475-1421 .

[Mathur2020-19] Матур, Уманг; Павлояннис, Андреас; Вишванатан, Махеш (2020). «Сложность прогнозирования динамической гонки данных». Материалы 35-го ежегодного симпозиума ACM/IEEE по логике в информатике . Ассоциация вычислительной техники. стр. 713–727. arXiv : 2004.14931 . дои : 10.1145/3373718.3394783 . ISBN 9781450371049 . S2CID 210171694 .

[Mathur2021-20] Перейти обратно: ^а ^б Кулкарни, Руча; Матур, Уманг; Павлояннис, Андреас (2021). «Динамическое обнаружение гонок данных через мелкозернистую линзу» . 32-я Международная конференция по теории параллелизма (CONCUR 2021) . Международные труды Лейбница по информатике (LIPIcs). 203 . Замок Дагштуль - Центр информатики Лейбница: 16:1–16:23. doi : 10.4230/LIPIcs.CONCUR.2021.16 . ISBN 9783959772037 . S2CID 235765773 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]