Анализ статических мьютексов

Question

Было бы разумно иметь язык, который статически проверяет правильность мьютекса? Т.е.,

var m 
var x guarded_by(m) 

func f1() { 
    lock(m) 
    x = 42 
    unlock(m) 
} 

func f2() { 
    x = 42 // error, accessing x w/o holding its mutex 
} 

func f3() assumes_locked(m) { 
    x = 42 
} 

func b1() { 
    f3() // error 
} 

func b2() { 
    lock(m) 
    f3() 
    unlock(m) 
} 

1. Возможно ли это? Т.е., может ли правильность использования мьютексов статически проверяться с помощью нескольких простых аннотаций, подобных этому?
2. Разве это разумно? Есть ли причина, по которой это было бы плохой идеей?
3. Есть ли какие-либо языки, на которых есть этот встроенный?

Answer 1

Статическое обнаружение состояние гонки

As delnan said in a comment, "мьютекс корректность" может означать различные вещи. From your comment, похоже, вы говорите о обнаружении состояния гонки, что удобно для меня, поскольку это было предметом моего тезиса бакалавра :-) ¹ Вы хотите знать (1), если это возможно, (2) если это разумно и (3) если это сделано. Как и с любым статическим анализом (в том числе облегченного типа-или-следственной-систему-как из них, таких, как это), первых два вопроса сводится к четырем вещам:

1. разумность: ли это позволить неправильным программам? Если да, то сколько/каких?
2. Полнота: Не правильные программы? Если да, то сколько/каких?
3. Удобство использования: Как программист накладные? ., какие аннотации необходимы, являются ли сообщения об ошибках понятными и т. Д.?
4. Голы: Где мы находимся в пространстве дизайна, ограниченном тремя ограничениями, мы пытаемся закончить?

Обратите внимание, что мы никогда не сможем получить 100% -ную точность как для 1, так и 2, из-за проблемы с остановкой (и ее более общего большого брата Rice's theorem). Например, большинство систем типов ² нацелены на обоснованность и удобство использования (№ 1 и № 3); то есть они стремятся быть просты в использовании, не допуская никаких небезопасных программ, и попытаться исключить только нереалистичные типа безопасных программ. (Их адвокаты, как я, будет утверждать, что они в целом удалось на достижение этой цели.)

Простая система типа блокировки проверки: RaceFreeJava

Ваш пример кажется, что он пытается максимально упростить (# 3) : вы предоставили минимальные аннотации, которые соответствуют тому, что вы надеялись, что программист будет иметь в виду все равно, а затем захотите провести анализ, который их проверяет. Общая схема звучит довольно похоже на RaceFreeJava (Abadi et al., 2006). RaceFreeJava является расширением Java, где:

• Классы могут быть параметризованы замками (так называемые ghost замки);
• Поля могут содержать guarded_by аннотации, указывающие, какие замки должны их защищать; и
• Методы могут содержать requires аннотации, указывающие, какие блокировки должны удерживаться для их вызова.

Как вы, возможно, предположили, идея состоит в том, что каждое поле имеет связанный замок, который должен храниться каждый раз при обращении к полю; анализ отслеживает, какие блокировки хранятся в каждой программной точке, и если к переменной обращаются, когда ее блокировка не находится в текущем наборе блокировок, сообщается об ошибке. Это немного тонче с параметрами блокировки ghost; Например, вы можете иметь

class RunningTotals<ghost Object m> { 
    private int sum  = 0 guarded_by m; 
    private int product = 1 guarded_by m; 

    public void include(int x) requires m { 
    sum  += x; 
    product *= x; 
    } 

    public int getSum() requires m { 
    return sum; 
    } 

    public int getProduct() requires m { 
    return product; 
    } 
} 

Теперь я могу встроить RunningTotals объект в каком-то другом объекте o и защитить его с замком o «s, что очень удобно; Тем не менее, анализ тогда должен быть осторожным, о котором действительно стоит замок m. Также обратите внимание, что методы в RunningTotalsне могут синхронизировать по m, так как m не является областью действия и является просто уровнем ghost; синхронизация должна выполняться клиентом. Подобно тому, как мы можем объявлять блокированные параметрами классы, другой особенностью RaceFreeJava является возможность объявлять классы thread_local; этим классам никогда не разрешается делиться между потоками и, следовательно, не нужно защищать свои поля замками.

Как вы отметили в комментарии, выяснение того, правильная программа с этими аннотациями, в общем, будет неразрешимой, особенно потому, что Java позволяет синхронизировать с произвольными выражениями. RaceFreeJava ограничивает синхронизацию final выражения, для здравого смысла; то, как и все аннотации типа, он использует консервативную синтаксическую проверку для блокировки. Abadi et al. что большинство правильных программ можно успешно проверить таким образом. Таким образом, они очень сильно раскалываются (действительно, анализ звучит по модулю некоторых выходных люков, которые они вставляют) и к удобству использования, за счет полноты. Чтобы проверить удобство использования - что сильно связано с полнотой, поскольку слишком много ложных предупреждений делают статический анализ непригодным для использования - Abadi et al. также написал инструмент (rccjava) для проверки этих аннотаций и выполнения небольших количеств вывода аннотации, а также использовал его для создания более крупного инструмента (Houdini/rcc) для выполнения еще большего вывода. Оценивая эти (таблицы I-IV), они нашли реальные ошибки без слишком много необходимых аннотаций или ложных предупреждений. Однако обратите внимание, что это не идеально; там будут некоторые действительные Java-программы, на которые этот анализ будет жаловаться.

Другие детекторы статические гонки

Потому что у меня есть естественная склонность к многословно, а потому, что (как я уже говорил) я написал дипломную работу на этом, я также расскажу о нескольких других анализов, но это звучит для меня, как RaceFreeJava, вероятно, наиболее актуальным. Если вы хотите просто пропустить до конца, после этого раздела будет подведение итогов.

Другой анализ на основе системы основан на Boyapati et al. (2002). Эта система типов обнаруживает как условия гонки, так и взаимоблокировки, но использует другую технику; он основан на типах собственности, которые отслеживают, какие потоки разрешены для доступа к каким переменным; переменные могут быть доступны только при блокировке их владельцев. Опять же, методы могут потребовать аннотации accesses или необходимо locks. Для проверки взаимоблокировок Boyapati et al. также добавьте понятие уровней блокировки, которые размещают все блоки в частичном порядке. Обеспечивая, что блокировки всегда приобретаются в этом порядке, блокировки автоматически исключаются. Опять же, этот алгоритм звучит (хотя доказательство, к сожалению, опущено), но не является полным и пытается быть полезным. Для этого они должны выполнять обширную работу по умозаключениям, поскольку запись аннотаций будет слишком большой работой.

Существуют и другие анализы, которые не являются системами типа. Они должны моделировать выполнение программы, а не просто выполнять синтаксические проверки, и, как правило, не должны быть ни звуковыми, ни полными, но полностью использовать для удобства использования, не требуя аннотаций (даже если они позволяют) и пытается сообщить Полезно ошибок. RacerX (Engler and Ashcraft, 2003) делает это, в некотором смысле, путем создания достаточной статической информации для приближения к запуску a dynamic Lockset-type algorithm, such as that used by Eraser (Savage et al., 1997). Для этого требуется много настроек, так как аппроксимировать проверку времени статично непросто, а Lockset уже приближается к истине. RacerX также выполняет проверку взаимоблокировки с использованием высоконастроенного подхода с распространением ограничений, где ограничения - блокировки. Engler и Ashcraft удалось использовать RacerX, чтобы найти некоторые ошибки в реальных операционных системах, хотя они получают ложные срабатывания и находят доброкачественные расы (таблица 5).

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

// Thread 1: 
acquire(superman_lock); 
*superman_bank_account += 100; // Saved Metropolis and got rewarded! 
release(superman_lock); 

// Thread 2: 
acquire(clark_kent_lock); 
*clark_kent_bank_account -= 100; // More bills... 
release(clark_kent_lock); 

, предполагающий, что superman_lock и clark_kent_lock различны, зная, следует ли этот код безопасен, требуется знать superman_bank_account ли такое же, как clark_kent_bank_account. И это очень сложно понять!

The Chord algorithm (Naik et al., 2006) ³ - это другой детектор гонки всей цепочки, который имеет в качестве ключевого шага детектор псевдонимов; опять же, мы сталкиваемся с теоремой Райса, и такой анализ не может быть как звуковым, так и полным. Chord трек может быть сглаженной информацией (эквивалентно, определенно-unaliased информации), и поэтому является необоснованным.

Подведение итогов

So. Вы хотели знать три вещи: ваша схема (1) возможна, (2) разумна и (3) выполнена в реальном мире? Все эти анализы показывают, что это вполне разумная и возможная идея; RaceFreeJava, в частности, демонстрирует, что идеи аннотации, которые у вас были, довольно близки к проверенной системе звукового типа. Тем не менее, я не знаю ни одного языка, на котором это встроено. Я считаю, что каждая работа, которую я привел здесь, реализовала их алгоритм, но я не смотрел на все, чтобы увидеть, доступны ли эти инструменты свободно, коммерчески доступные, под активным развитием, или что. Конечно, однако, реальный статический анализ действительно существует; например, Coverity's (commercial) static analyzer находит среди многих других условий гонки и тупиков. Они имеют недостатки, а именно потенциальные ложные жалобы на хороший код или отсутствие жалоб на плохой код, но это происходит с территорией, и часто это не является большой проблемой на практике.

---

Сноски

¹ Ну, обнаружение динамического состояния гонки, в любом случае. Все это означает, что я выкалываю из соответствующего раздела работы, который я написал в то время, что особенно удобно! Это также означает, что это может отсутствовать, особенно последние события (я написал диссертацию в 2011-2012 учебном году). Это означает, что это было давно, так как я думал обо всем этом, так что, возможно, есть вопиющие недостающие цитаты или (надеюсь, малые) ошибки выше; если кто-нибудь замечает такую ​​вещь, пожалуйста, дайте мне знать или просто отредактируйте этот пост!

² Большинство чувственные системы типа, говорит Haskell партизана :-) C не волнует вообще, например, и Java получает наиболее пути там, но прибегать к динамическим проверкам благодаря вещам как понижение и ковариантность массива (* содрогание *).

³ Извините за ссылку в цифровой библиотеке ACM; Я не мог найти свободно доступную PDF-версию этой статьи, но нашел a PostScript version.

---

Библиография

• Martin Abadi, Cormac Flanagan, and Stephen N. Freund. "Types for Safe Locking: Static Race Detection for Java." In ACM Transactions on Programming Languages and Systems (TOPLAS) 28(2), June 2006, pp. 207–255.

• Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. "Ownership Types for Safe Programming: Preventing Data Races and Deadlocks." In In Proceedings of the 17th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Volume 37, November 2002, pp. 211–230.

• Dawson Engler and Ken Ashcraft. "RacerX: Effective, Static Detection of Race Conditions and Deadlocks." In Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP), Volume 37, 2003, pp. 237–252.

• Mayur Найк, Алекс Aiken, и Джон Уэйли. «Эффективное обнаружение статической гонки для Java». В Труды конференции ACM SIGPLAN 2006 года по программированию и внедрению языка программирования (PLDI), том 41, 2006, стр. 308-319. Доступно at the ACM Digital Library и as a PostScript file.

• Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. "Eraser: A Dynamic Data Race Detector for Multithreaded Programs." ACM Transactions on Computer Systems 15(4), 1997, pp. 391–411.