Верификация методов бесконфликтного доступа к памяти

Для проверки свойств программы с целью определения корректности или некорректности ее работы во время проектирования и разработки используются различные средства верификации [kulyamin]. Среди таких средств наибольшее применение на практике имеют статический анализ, динамические методы (тестирование) и формальные методы. Исправление ошибок, выявленных статическим анализом, и положительные результаты тестирования не позволяют с гарантированной уверенностью рассуждать о наличии у программы определенных свойств, определяющих корректность ее выполнения. Данные методы лишь повышают доверие к программе. При разработке методов бесконфликтного доступа к памяти важно гарантировать наличие ряда свойств у алгоритмов, реализующих данные методы. Подобные гарантии могут дать лишь формальные методы верификации, одним из которых является метод проверки моделей или на моделях (англ. model checking) [karpov]. Данный метод наиболее прост и эффективно применяется на практике. Одним из самых известных и широко используемых инструментов, в котором реализуется метод проверки моделей, является рассматриваемый в данном пособии верификатор Spin [spin].

Проверяемые свойства алгоритмов бесконфликтного доступа к памяти, впрочем как и для любых других алгоритмов, подразделяются на два больших класса [tel]:

1. свойства безопасности; свойство из данного класса можно сформулировать как «для любого выполнения алгоритма утверждение P истинно в каждой конфигурации выполнения», «утверждение P всегда истинно» или «ничего плохого никогда не произойдет»;

2. свойства живости; свойство из данного класса можно сформулировать как «для любого выполнения алгоритма утверждение P истинно в некоторой конфигурации выполнения», «утверждение P когда-то обязательно становится истинным» или «рано или поздно произойдет что-то хорошее».

В случае проверки свойства, принадлежащего классу свойств безопасности, верификатору необходимо найти вычисления, которые ведут к нарушению свойства; при проверки свойства живости верификатору необходимо найти вычисления, которые не приводят к конфигурации, в которой утверждение P становится истинным, т. е. «что-то хорошее» может откладываться до бесконечности.

Во многих случаях выполнение свойств, определяющих корректное функционирование (выполнение свойств безопасности или живости) модели, должно проводиться только на тех вычислениях, на которых выполняется некоторое дополнительное условие, которое по разным причинам называется требованием справедливости (англ. fairness) [karpov]. Первая причина состоит в том, что анализируемая система будет работать в некотором окружении, к функционированию которого мы предъявляем эти требования, поскольку только с этими дополнительными требованиями к окружению наша система может выполнять полезную функциональность (например, справедливый планировщик процессов в реальной системе, который реализует справедливую стратегию планирования — самая простая: round-robin). Т.е. в данном случае требования предъявляются к окружению, которое мы не верифицируем (не можем, не нужно). Вторая причина другая: она состоит в том, что в той модели переходов, которая используется при верификации для представления реальных систем, могут существовать нереалистичные, нереализуемые вычисления, возникшие из-за ограниченных выразительных средств модели (например, бесконечная потеря сообщения в ненадежном канале модели, в то время как передача сообщения в реальном канале всегда отлична от нуля). Т.е. в данном случае учитывать при верификации такие нереалистичные вычисления нет необходимости [karpov]. Или, другими словами, «условия справедливости позволяют исключить из рассмотрения такие выполнения, в которых некоторые события оказываются допустимыми всегда (или бесконечно часто), но при этом ни разу не осуществляются в виде переходов (из-за того что выполнение продолжается всякий раз за счет осуществления других событий)» [tel].

Различают следующие виды справедливости:

· слабая справедливость: выполнение считается слабо справедливым, если никакое событие не может оказаться допустимым в каждой из бесконечного числа подряд идущих конфигураций, не осуществившись при этом ни разу в этом выполнении [tel]; т. е., другими словами, «если процесс запрашивает обслуживание постоянно (неопределенно долго), он получает его неопределенно часто» или «действие не может бесконечно игнорироваться, если оно все время готово к выполнению» [karpov];

· сильная справедливость: выполнение считается сильно справедливым, если никакое событие, не может оказаться допустимым в бесконечном множестве конфигураций, не осуществившись при этом ни разу в этом выполнении [tel]; т. е., другими словами, «если процесс запрашивает обслуживание неопределенно часто, он получает его неопределенно часто» или «действие не может все время игнорироваться, если оно готово к выполнению неопределенно часто» [karpov];

· безусловная справедливость — «каждый процесс получает обслуживание неопределенно часто».