> Насчёт макросов понял (хотя им с этого начинать надо бы - что вот так пишется на приличных плюсах, но для легаси тоже есть костыль), но есть и более серьёзные проблемы

Я согласен. Я думаю это связано с тем, что документация писалась в 2011 году, когда C++11 был менее распространен.

> 1) эти аннотации отделены от собственно кода синхронизации. То есть никто их соответствие реальному положению вещей не гарантирует.

Я не понял, что имеется ввиду. Анализ проверяет, что при обращении к переменной вызывающий код удерживает мьютексы, указанные в аттрибуте guarded_by у этой переменной. Что значит "никто их соответствие реальному положению вещей не гарантирует"? Анализ как раз проверяет, что взятие мьютексов согласованно с аттрибутами guarded_by.

Или ты имеешь ввиду, что аттрибуты guarded_by могут не соответствовать реальной логике работы программы? Ну здесь ничего не поможет. Компьютер не может знать какие данные защищены какими мьютексами.

Даже в RacerD есть guarded_by: http://fbinfer.com/docs/infer-bug-types.html#anonymous_inner

> 2) необходимость заменять мьютекс своим типом.

Почему ты так считаешь? В libc++ (реализация стандартной библиотеки идущая с clang) std::mutex аннотированы: https://github.com/llvm-mirror/libcxx/blob/276a69c18b3eeb6e8... Реализации стандарных библиотек других компиляторов не аннотированы аттрибутами, которые эти компиляторы не поддерживают, это предсказуемо.

> 3) необходимость вообще писать эти аннотации.

Тогда тебе будет не нравится статик-анализ вообще. Поскольку, как правило без дополнительных аннотаций он имеет либо много false-positive, либо много false-negative. А аннотации делают статик-анализ применимым на практике.