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

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

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

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

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

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

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

Ответ 1

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

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

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

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

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

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

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

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

Нижняя линия: статические анализаторы и динамические анализаторы имеют свою силу.

Ответ 2

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

Ответ 3

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