Статический анализ потока: хорошая идея?

Question

Я помогаю поддерживать и строить довольно большой Swing GUI с множеством сложных взаимодействий. Часто я обнаруживаю, что исправляю ошибки, которые являются результатом того, что вещи переходят в нечетные состояния из-за некоторого состояния гонки где-то еще в коде.

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

Так что мне пришло в голову, что это должно быть что-то, что можно легко реализовать с помощью аннотаций. И вот, существует по крайней мере один инструмент статического анализа, CheckThread , который использует аннотации для достижения этой цели. Кажется, он позволяет вам объявить метод ограниченным конкретным потоком (чаще всего EDT) и помечает методы, которые пытаются вызвать этот метод, не объявляя себя как ограниченный этим потоком.

Так что на первый взгляд это просто похоже на дополнение с огромным усилением к исходному циклу и циклу сборки. Мои вопросы:

• Существуют ли истории успеха для людей, использующих CheckThread или аналогичные библиотеки для обеспечения ограничений потоков? Есть истории неудач? Почему это удалось / не удалось?
• Это хорошо в теории? Есть ли теоретические недостатки?
• Это хорошо на практике? Стоит ли оно того? Какую ценность оно принесло?
• Если это работает на практике, Какие хорошие инструменты для поддержки этого? Я только что нашел CheckThread, но признаюсь, что я не совсем уверен, что я ищу, чтобы найти другие инструменты, которые делают то же самое.

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

Answer 1

Этот ответ более сфокусирован на теоретическом аспекте вашего вопроса.

По сути, вы делаете утверждение: «Этот метод работает только в определенных потоках».Это утверждение на самом деле не отличается от любого другого утверждения, которое вы можете сделать («Метод принимает только целые числа меньше 17 для параметра X»).Проблемы

• Откуда берутся такие утверждения?
• Могут ли статические анализаторы проверять их?
• Откуда у вас такой статический анализатор?

В основном такие утверждения должны исходить от разработчиков программного обеспечения, так как они единственные люди, которые знают намерения.Традиционный термин для этого - «Проектирование по контракту», хотя большинство схем DBC находятся только в текущем состоянии программы (макрос C assert ), и они действительно должны быть в прошлом программ.и будущие состояния («временные утверждения»), например, «эта подпрограмма будет выделять блок памяти, и в конечном итоге некоторый фрагмент кода будет освобождать его».Можно создать инструменты, которые попытаются с помощью юрисдикционного определения, что такое утверждения (например, работа по индукции утверждений Энглера; другие проделали работу в этой области).Это полезно, но ложные срабатывания являются проблемой.С практической точки зрения, просьба к дизайнерам кодировать такие утверждения не кажется особенно обременительной, и это действительно хорошая долгосрочная документация.Кодируете ли вы такие утверждения с помощью конкретной языковой конструкции "Контракт" или с помощью оператора if ("if Debug && Not ( assertion ) Then Fail ();") или скрываете ихв аннотации это действительно просто вопрос удобства.Приятно, когда язык позволяет кодировать такие утверждения напрямую.

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

Где вы берете такие анализаторы?Учитывая все необходимое оборудование, их сложно построить, и поэтому следует ожидать, что они будут редкими.Если кто-то его построил, отлично.Если нет ... как правило, вы не хотите делать это самостоятельно с нуля.Лучшая долгосрочная надежда состоит в том, чтобы иметь общий механизм анализа программ для построения таких анализаторов, чтобы амортизировать расходы на создание всей инфраструктуры.(Я создаю основы инструментов анализатора программ; см. Наш DMS Software Reengineering Toolkit ).

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

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

Итог: статические анализаторы и динамические анализаторы имеют свои силы.

Answer 2

Мы не пробовали никаких инструментов статического анализа, но мы использовали AspectJ для написания простого аспекта, который обнаруживает во время выполнения, когда любой код в java.awt или javax.swing вызывается вне EDT. Он нашел несколько мест в нашем коде, в которых отсутствовал SwingUtilities.invokeLater(). Мы включаем этот аспект в течение всего цикла QA, а затем отключаем его незадолго до выпуска.

Answer 3

Как и требовалось, это не относится конкретно к Java или EDT, но я видел хорошие результаты при использовании средств проверки статического анализа Coverity для C / C ++.У них действительно был более высокий уровень ложных срабатываний, чем у менее сложных контролеров, но владельцы кода, похоже, были готовы с этим смириться, учитывая то, насколько трудоемкими могут быть ошибки при тестировании.Боюсь, детали являются конфиденциальными, но публичные статьи Доусона Энглера (например, «Ошибки как девиантное поведение») очень хороши в общем подходе «Следующие« N »экземпляров вашего кода делают« X »перед«Y »,;этот экземпляр не. "