Max Home IndustryЭто вряд ли обсуждаемая проблема, но Android — сложная платформа для параллельного программирования. В результате большинство приложений не используют его в полной мере. Facebook подарил вам инструмент, который делает его намного проще и использует его, чтобы сделать собственное приложение более быстрым и надежным.
Проект RacerD был начат, потому что команда Facebook осознала, что параллелизм в чем угодно — это сложно, особенно в Android. Причина, по которой Android сложен, отчасти объясняется моделью жизненного цикла приложения, а отчасти — отсутствием четких указаний о том, что работает, а что лучше всего. На самых низких уровнях вы не получите никакой помощи от инструментов, чтобы найти базовые вещи, такие как расовые опасности. Опасность гонки — это то, что у вас есть, если есть два или более потоков, выполняющих обновление — какой из них попадает последним, определяет, что это за обновление. Обновления расы трудно найти, потому что код, участвующий в гонке, может быть распределен по кодовой базе.
RacerD использует очень хитроумные символические рассуждения, чтобы найти код, который подвержен расовым опасностям.
«Чтобы получить представление о масштабе проблемы, скажем, программа хотела изучить каждый из различных способов, которыми два потока по 40 строк кода могут взаимодействовать одновременно (« чередование »на жаргоне). Даже учитывая эти взаимодействия на одном уровне. с невероятной скоростью в 1 миллиард взаимодействий в секунду, компьютер проработает более 3,4 миллиона лет! С другой стороны, RacerD выполняет свою работу менее чем за 15 минут для программ большего размера, чем 80 строк ».
Анализировать реальную программу методом грубой силы невозможно, поэтому команда Facebook использовала теорию параллельной логики разделения и доказательства того, что код свободен от состояний гонки. Работа стала более практичной и актуальной, когда команда, работающая над приложением News Feed для Android, планировала изменить его с преимущественно последовательного дизайна на полноценную многопоточную архитектуру. Это давление привело к получению минимально жизнеспособного продукта, и родился RacerD.
Цель RacerD — найти гонки данных. Его конструкция основана на следующих идеях:
1. Не проводите анализ всей программы; быть композиционным.
2. Не исследуйте чередование; отслеживать информацию о блокировке и потоке.
3. Не пытайтесь провести общий точный анализ псевдонимов; используйте агрессивный анализ владения для сглаживания выделенных ресурсов.
Так это работает?
Кажется, да:
«RacerD был запущен в производство в течение 10 месяцев на нашей базе кода Android и выявил более 1000 проблем с многопоточностью, которые были исправлены разработчиками Facebook до того, как код попал в производство».
RacerD выглядит достаточно простым в использовании, а аннотации, которые он применяет к вашему коду, достаточно просты для понимания. Он работает как часть инструмента статического анализа Infer Facebook для Java, C / C ++ и Objective C. Было бы неплохо, если бы Infer для Android был частью Android Studio, но …
Проект находится на GitHub со стандартной лицензией BSD.