суббота, 26 марта 2011 г.

Нахождение взаимных блокировок потоков при статическом анализе кода

Всем доброго вечера.
Когда Иван читал у нас, на мех-мате в Каразина свой спецкурс у меня появилась навящевая идея по поиску дедлоков без запуска программы, только на основании ее кода. Было сделано несколько попыток найти какой-то внятный алгоритм. К настоящему моменту я достаточно неплохо, как мне кажется, продвинулся в этом направлении.
Чтобы не усложнять до предела работу по парсингу кода на Java или C я написал простой язык для описания потоков.

Структура языка:
_listing: _thread | _listing
_thread: Thread _name {_code}
_code: _criticalPoint | _ifSection | _whileSection | _code
_crticalPoint: >_name; | <_name;
_ifSection: if(_name) {_code}
_whileSection: while(_name) {_code}
_name: [A-Za-z][A-Za-z0-9_]*

Здесь слова с префиксом "_" означают метапеременные.
Критические точки (_crticalPoint) - это секции кода, в которых захватываются или освобождаются захваченные ресурсы. Критические точки вида >_name - точки захвата ресурсов, точки вида <_name - точки освобождения ресурса.
Секции цикла (_whileSection) и ветвления (_ifSection) аналогичны, по смыслу, соответсвующим секциям в языках C и Java. Отличие состоит в том, что в качестве условия используется некоторая символная константа, которая именует соответствующую секцию.

Простейший пример взаимной блокировки на этом языке выглядит так:
Thread A {
>a;
>b;
<a;
<b;
}

Thread B {
>b;
>a;
<b;
<a;
}
Здесь мы в потоке A захватывае ресурс a, затем захватываем ресурс b, затем их последовательно отпускаем. Аналогично, в потоке B, тололько в другом порядке.

В общем случае поток может выглядеть, например, так:
Thread T {
      >a;
      if(expr1) {
            >b;
            >c;
            while(expr3) {
                  >d;
                  <d
            }
            <b;
            <c;
      }
      <a;
}
Поэкспериментировать с системой можно по ссылке: checkdeadlock.org
Буду благодарен за комментарии по идее вообще и найденным багам в частности.
Обсуждать можно здесь, и здесь

PS. Если буду предложения по сотрудничеству, с удовольствием рассмотрю.

Комментариев нет:

Отправить комментарий