В Meta разработали статический анализатор, который фиксирует взаимоблокировки в Java-коде для Android, даже не запуская сам код. Он способен проводить ревизии в кодовых базах с сотнями миллионов строк.

Анализатор развернули в системе непрерывной интеграции Meta, где он сканирует каждую фиксацию в семействе приложений Android. За последние два года разработчики внесли более 200 исправлений в ответ на отчеты о взаимоблокировках, что составляет около 54% всех исправлений.

Анализатор Meta имеет открытый исходный код и является частью системы статического анализа Infer.

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

Центральной частью метода является набор критических пар. Критическая пара (A,B) фиксирует следующий факт: метод пытается получить блокировку B, и в это время он уже удерживает ровно столько блокировок в наборе A. Этих данных, вычисленных по всем методам, достаточно, чтобы ответить на вопрос о том, возможна ли взаимоблокировка между двумя параллельными методами.

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

Разработчики утверждают, что их подход делает анализатор достаточно масштабируемым, чтобы его можно было развернуть на больших кодовых базах в Meta.

Meta представила новый статический анализатор для Android