Автореферат диссертации на соискание ученой степени

1   2

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

Технология разработки распределенных вычислительных систем. Распределенная вы­числительная система обеспечивает решение задачи в режиме взаимодействия автономных программных компонентов, которые выполняются в различных узлах вычислительной сети. Функционирование каж­дого компонента сводится к (многократному) выполнению заданной последова­тельности арифметических действий над числовыми данными. Функциональные требования предъявляются к такой системе в целом, а не к отдельным компонентам, и имеют вид правил преобразования входных данных в выходные, заданных математической моделью вычислительной задачи. Поэтому при ее разработке сначала строятся модели вычислений и алгоритмов, а затем выполняется декомпозиция – разбиение на компоненты.

Спецификация требований эффективности к распределенным вычислительным системам проведена на базе стандарта ISO/IEC 9126¹. Идентифицированы следующие ключевые нефункциональные характеристики:

1. алгебраическая абстрактность (ALG) – ориентация на абстрактный математический язык вычислительных задач, независимость от концепций компьютерных систем;
   
2. производительность (PERF) – максимальная длительность выполнения различных вариантов использования;
   
3. ресурсоемкость (RES) – объем ресурсов, выделяемых для хранения данных;
   
4. надежность (RELY) – способность функционировать в нештатных условиях.
   

На основе этих характеристик построена формальная модель качества (quality model), описанная при помощи декларативного языка NoFun². В рамках этой модели значения показателей -, образующих абстрактный модуль, определяются на таких структурных компонентах формальной функциональной спецификации, как варианты использования и типы данных.

Проанализированы возможности явной спецификации и верификации требований -, предоставляемые основными математическими методами разработки программных систем. Результаты анализа представлены в следующей таблице (знаком «+» отмечено наличие явной поддержки соответствующего требования средствами формализма, а знаком «–» – отсутствие).

№	Формализм	ALG	PERF	RES	RELY
	Семантические сети и онтологии	+	–	–	–
	Абстрактные типы данных	+	–	–	–
	Частичная интерпретация	+	–	+	+
	Денотационное описание поведения	–	+	+	+
	Алгебры процессов	–	–	–	+
	Логический (дедуктивный) подход	+	–	–	–
	Структуры Крипке	–	+	+	+
	Мутирующие алгебры	+	–	–	+
	Структурный анализ	–	–	–	–
	Объектно-ориентированный подход	–	–	–	+
	Компонентное проектирование	–	+	+	+

Базовый технологический цикл разработки распределенных вычислительных систем, ориентированный на обеспечение эффективности при использовании формальных методов, состоит из следующих фаз.

0. формирование спецификации моделей вычислений с учетом требований к диапазону и точности обрабатываемых чисел;
   
1. проектирование вычислительных алгоритмов;
   
2. компонентная декомпозиция и разработка дисциплины обмена данными с учетом требований к производительности;
   
3. реализация и верификация компонентов;
   
4. реализация протоколов обмена данными и развертывание системы;
   
5. сборочное тестирование;
   
6. ввод в эксплуатацию и сопровождение системы.
   

Детальному рассмотрению фаз - посвящена настоящая работа.

Формальная спецификация моделей вычислений. Для выполнения фазы предложен метод частичной интерпретации (). Потребность в нем связана с тем, что алгебраические методы типа , позволяющие обеспечить нефункциональное требование к абстрактности (ALG), не предоставляют средств абстрактного моделирования бесконечных сущностей на конечных структурах, необходимого для спецификации ресурсных ограничений (RES). Если такое моделирование и проводится, то ad hoc, что может привести к кардинальному изменению свойств исходных абстрактных типов данных (в том числе теоретико-доказательственных). В свою очередь, переход к «сильным» семантическим методам типа или влечет отказ от алгебраической абстрактности и внесение в спецификацию явной зависимости от парадигм компьютерных систем.

Отправным пунктом метода частичной интерпретации служит представление функциональных требований в виде теории T – множества предложений подходящего языка первого порядка. Затем фиксируется некоторое конечное множество C моделируемых объектов, обозначаемых константными символами языка теории T, и строится модель такой подтеории T, которая содержит только утверждения об элементах C. Ресурсные ограничения формализуются в виде условий на мощность C. Верификация функциональных требований сводится к подстановке имен объектов из C в формулы теории T. Отметим, что при интерпретации объектов, не входящих в C, могут нарушаться даже аксиомы равенства. Построение изоморфного вложения множества C в универсумы моделей различных теорий позволяет формализовать явление полиморфизма. В отличие от алгебраических методов спецификации, частичная интерпретация позволяет работать с теориями самого общего вида (что вообще характерно для теоретико-модельного подхода), а также обеспечивает значительную гибкость при выборе множества реализуемых объектов.

Перейдем к точным определениям.

Определение 2.1. Будем рассматривать языки первого порядка без равенства. Пусть  – сигнатура, содержащая символ равенства , T – теория сигнатуры , содержащая стандартные аксиомы равенства, ₀ – конечная подсигнатура сигнатуры . Проекцией T₀ называется множество таких бескванторных предложений  сигнатуры ₀, что T   и для любого терма t, входящего в , существует константный символ c₀, такой, что T  tc. Частичной интерпретацией теории T в сигнатуре ₀ называется пара áA,₀, где A – такая алгебраическая система сигнатуры (A)₀, что AT₀.

Пусть C(₀)  {c₁,…,c_n} – множество константных символов сигнатуры ₀. Релятивизацией формулы  на ₀ называется формула ₀, получающаяся из  заменой всех подформул вида x₀(x₀,x₁,…,x_k) конъюнкциями _i=1,…,n(c_i,x₁,…,x_k) и вида x₀(x₀,x₁,…,x_k) – дизъюнкциями _i=1,…,n(c_i,x₁,…,x_k). Будем говорить, что пара áA,₀ñ поддерживает предложение , если A ₀.

Пусть D₀(A) – множество бескванторных предложений сигнатуры ₀, истинных в A. Полиморфной структурой áA,₀ñ называется совокупность таких пар áB,₀ñ, что (B)₀ и D₀(A) совпадает с D₀(B). Гомоморфизмом пар áA,₀ñ, áB,₁ñ называется отображение h:|A||B|, которое является гомоморфизмом обеднения A(₀₁) в обеднение B(₀₁). □

Корректность определения частичной интерпретации вытекает из следующей теоремы.

Теорема 2.1. Если теория T непротиворечива, то она имеет частичную интерпретацию в любой конечной подсигнатуре сигнатуры (T). □

Формальными спецификациями машинных арифметик служат частичные интерпретации арифметических теорий с конечными универсумами. Гомоморфизмы стандартных моделей соответствующих арифметик в такие частичные интерпретации называются моделями вычислений. С целью анализа основных моделей вычислений в целых числах рассмотрим теорию сигнатуры _  {, 0, S}{c_i| i>0} со следующими аксиомами:

1. x (¬0Sx) (0 является начальным элементом);
   
2. xy (SxSyxy) (функция следования S инъективна);
   
3. для всякой формулы (x₀,x₁,…,x_k) сигнатуры _ верно
   

x₁…x_k[(0,x₁,…,x_k)  (x₀(x₀,x₁,…,x_k)(Sx₀,x₁,…,x_k)) 

x₀(x₀,x₁,…,x_k)]

(схема аксиом индукции);

4. для всякого i>0 выполнено c_iSⁱ0, где Sⁱ  S…S (i раз).
   

Пусть S  áA,₀ñ – частичная интерпретация этой теории в сигнатуре ₀, содержащей символ равенства, S и хотя бы одну константу. Начальным отрезком чисел называется множество E_m+1  [0,m]  {0,c₁,…,с_m}.

Теорема 2.2. Для того чтобы S поддерживала все частные случаи схемы аксиом индукции , необходимо и достаточно, чтобы множество C(₀) константных символов сигнатуры ₀ совпадало с некоторым начальным отрезком {0,c₁,…,с_m}. □

Следствие 2.2.1. Если частичная интерпретация S поддерживает схему индукции, то она также поддерживает схему . □

Теорема 2.3. Пусть S поддерживает схему индукции, и n>0 таково, что C(₀)=[0,n-1]. Тогда S поддерживает аксиому инъективности в одном из следующих двух взаимоисключающих случаев:

1. существует элемент n|A|, не равный ни одной из констант из множества [0,n 1], такой, что A Sc_n-1n;
   
2. A Sc_n-10.
   

Аксиома поддерживается только в случае (i). □

Для случая естественное требование A Snn приводит к арифметике с переполнением с |A|=E_n+1. В случае также выбирается |A|=E_n+1, однако требуется A SnS0, интерпретация арифметического равенства отождествляет 0 и n, и получается арифметика по модулю, в которой значение n соответствует флагу переноса (carry flag). Особенностью арифметики по модулю является отсутствие поддержки аксиомы монотонности естественного числового порядка. Арифметические операции определяются через символы сигнатуры _ согласно стандартным рекурсивным схемам.

Рассмотрены продолжения машинных арифметик на множество целых чисел, для спецификации которых построены следующие алгебраические системы.

1. Начальные отрезки неотрицательных целых чисел с переполнением:
   

OA_n+1  áE_n+1, 0, 1, …, n-1, =, |+|, ||, ||ñ,

x |+| y  min(n, x+y),

x || y  mах(0, x-y),

x || y  min(n, xy).

2. Симметричные отрезки целых чисел с переполнением:
   

SA_n+1  á{+,}E_n+1, -(n-1), …, n-1, ||=||, ||+||, ||||, ||||ñ

с «симметричными продолжениями» операций системы OA_n+1.

3. Отрезки целых чисел, содержащие нуль, с переполнением и сдвигом:
   

BA_n+1,m  áE_n+1, -(m-1), …, -m+n-1, =, [+]_m, []_m, []_mñ,

x [+]m y 	{	n, x=n либо y=n,
		max(0, min(n, x+y-m)), 0<x<n, 0<y<n,
		0 в остальных случаях,
x []m y 	{	n, x=n либо y=0,
		max(0, min(n, x-y+m)), 0<x<n, 0<y<n,
		0 в остальных случаях,

умножение []_m строится по стандартной рекурсивной схеме.

4. (Почти) симметричные отрезки целых чисел по модулю:
   

MA_n+1  áE_n+1, 0, 1, …, -1, (=), (+), (), (), Carryñ,

x (=) y  (x=y)(x,y){(0,n),(n,0)},

x (+) y  (x+y) mod n,

() x  n-x,

x () y  xy mod n,

Carry(x)  (x=n).

Деление (нацело) определяется соотношением

x {/} y 	{	n, y=0 либо x=n
		[x/y] в остальных случаях.

Рассмотрено представление целых чисел в позиционной системе счисления. Поскольку одноразрядные операции в b-ичной системе счисления осуществляется по модулю b (причем перенос учитывается в следующем разряде), арифметика q-разрядных чисел должна содержать флаг переноса, соответствующий значению b^q. Поэтому она интерпретируется на универсуме E_bq, где bq  b^q+1, с помощью изоморфного вложения :E_bqE_b+1^q, которое задается разложением числа x на слагаемые вида b_j(x)=x_jb^j, j=0,1,…,q-1, где

bj(x) 	{	x mod bj+1 - x mod bj, 0j<q-1,
		x - x mod bq-1, j=q-1.

Произвольная функция f:E_bq^kE_bq может быть задана посредством квазипостовского представления (к.п.п.) – совокупности функций {f_j:E_b+1^qkE_b+1| j=0,…,q 1} такой, что если разложение каждого x_i по основанию b имеет вид x_i=∑_jx_i,jb^j, то разложение f(x₁,…,x_k) имеет вид f(x₁,…,x_k)=∑_jf_j(x_1,0,…,x_1,q 1,…,x_k,0,…,x_k,q 1)b^j. Регулярным (р.к.п.п.) называется представление посредством семейства, отображающего множество codom  = E_b^q({0}^q 1{b}) в себя. Если функция f:E_bq^kE_bq строится посредством р.к.п.п. из некоторой функции g:E_b+1^kE_b+1 по правилу f_j(x_1,0,…,x_k,q 1)=g(x_1,j,…,x_k,j), то она называется функцией поразрядной логики; если f имеет такое р.к.п.п., в котором каждая f_j зависит только от (x_1,j,…,x_k,j)E_b+1^k, то она называется поразрядной; а если такое, в котором каждая f_j зависит только от (x_1,0,…,x_1,j,…,x_k,0,…,x_k,j)E_b+1^(j+1)k, то прогрессивной.

При частичной интерпретации поля рациональных чисел наибольшие трудности доставляет аксиома плотности порядка, поскольку обеспечить ее поддержку при конечном объеме ресурсов невозможно. Описываются такие решения, как машинная арифметика с фиксированной запятой (fixed point), в которой C(₀)={ab^-R| a[a₁,a₂]} для некоторых целых чисел a₁<a₂ и R>0, и с плавающей запятой (floating point) с C(₀)=FP_b, где

FP_b {ab^r-N| a[b^N-1,b^N-1],r[-R,R]}  {ab^-(R+N+1)| a[0,b^N-1-1]}

для некоторых целых N>0 и R>N, так что арифметика мантисс реализуется на базе SA_bN, а порядков – на базе BA_2R+2,R+N, с привлечением дополнительных операций денормализации аргументов и нормализации значений.

Моделирование архитектуры машинной арифметики. Спецификации моделей вычислений требуются в качестве входных данных при выполнении фазы технологического цикла. Дело в том, что в дополнение к собственно построению и оценке алгоритмов с применением методов вычислительной математики, в ходе этой фазы выполняется их адаптация к технологической процедуре, известной как отображение на архитектуру компьютерных систем. Именно при отображении осуществляется обеспечение требований эффективности, причем ресурсы многих высокопроизводительных вычислительных платформ задействуются в полную силу только при учете их специфических конструктивных особенностей. Для того чтобы при развертывании системы по узлам гетерогенной вычислительной сети обеспечить гибкость и адаптивность, необходим математический метод моделирования архитектуры вычислительных систем, не зависящий от конкретных моделей вычислений, а также предоставляющий технику верификации посредством формального доказательства. Этим критериям удовлетворяют методы проверки на моделях () и компонентного проектирования ().

Характерными особенностями архитектуры современных компьютеров являются уменьшенный набор команд, конвейеризация, параллелизм, многоуровневый доступ к данным. С целью учета таких особенностей предложен формальный проблемно-ориентированный язык ADŁ (Architecture Description by Łukasiewicz logic) для построения моделей архитектуры вычислительных систем типа , основанный на многозначной логике Лукасевича. Архитектурными компонентами машинных арифметик служат единицы хранения числовых данных (переменные), значениям (состояниям) которых отвечают логические константы. Связками служат суперпозиции базисных функций, задающие правила вычисления значений компонентов-результатов по значениям компонентов-аргументов. Свойство слабой полноты логики Лукасевича, рассмотренное ниже, обеспечивает формальную основу для концептуального разделения компонентов и связок. Явные выражения связок в различных базисах этой логики и ее обогащений составляют предложения языка ADŁ, так что при его использовании отображение вычислительных алгоритмов сводится к построению архитектурных конфигураций. Характеризация выразимости арифметических операций в различных базисах создает формальную основу для применения известных методов оценки мощности и эффективности моделей вычислений и алгоритмов^3,4.

Логика Лукасевича описывается алгебраической системой вида

Ł_n+1 F áE_n+1, ~, , {n}ñ,

~x F n-x,

xy F min(n, n-x+y).

Через ее связки выражаются дизъюнкция и конъюнкция многозначной логики:

xy F max(x, y) = (xy)y,

xÙy F min(x, y) = ~(~x~y) = ~(x~(xy)).

Поскольку истинностное логическое значение n соответствует переполнению в машинных арифметиках, для верификации отсутствия переполнения в вычислительных программах можно использовать технику доказательств логики Лукасевича. Основой для ее применения служит следующий факт. Пусть

Ji(x) F	{	n, x=i,
		0, x≠i.

Предложение 3.11. Выражение, вычисление которого задается формулой A, не дает переполнения тогда и только тогда, когда ~J_n(A) – тавтология Ł_n+1. □

При характеризации логики Лукасевича как класса функций на E_n+1, замкнутого относительно суперпозиции, используются следующие обозначения. Пусть P_n+1 – класс всех функций на E_n+1, образующий логику Поста. Для произвольного непустого подмножества XE_n+1 положим C^X_n+1 F {fP_n+1| f(X,…,X)X}. Согласно теореме Яблонского, при XE_n+1 класс C^X_n+1 является предполным в P_n+1, т.е. он замкнут и замыкание его объединения с любой функцией, не выразимой в нем, равно P_n+1.

Определение 3.1 (И. Розенберг). Класс функций K_n+1 называется слабо полным, если система функций, получающаяся в результате объединения K_n+1 с множеством всех константных функций на E_n+1, полна в P_n+1. Слабым штрихом Шеффера называется такая функция f, что класс {f} является слабо полным. □

Определение 3.2. Замкнутый класс функций, содержащий связки матрицы Лукасевича, называется Ł-замкнутым. Для произвольного класса K_n+1 замыкание его объединения со связками Ł_n+1 будет обозначаться Ł[K_n+1]. Замкнутый класс, состоящий из всех суперпозиций связок матрицы Лукасевича и некоторой функции f на E_n+1, будем обозначать через Ł[f]_n+1. Будем также говорить, что класс K_n+1 (функция f) обогащает матрицу Лукасевича до класса Ł[K_n+1] (Ł[f]_n+1). □

Слабая полнота Ł_n+1 была доказана Эвансом и Шварцем⁵. А.С. Карпенко доказал⁶, что для всякого Ł-замкнутого класса K_n+1 существует такое YE_n+1, что K_n+1 совпадает с классом F_n+1(Y) F _uY C^V(u)_n+1, где V(u) F {vE_n+1| uD(v)}, а D(x) – множество делителей числа x. В частности, Ł_n+1 содержится в предполном классе T_n+1 F C^{0,n}_n+1. Более того, любые арифметические отношения выражаются в Ł_n+1 функциями вида f:E_n+1^k{0,n}. Например, имеет место

Предложение 3.12. Обычное арифметическое равенство на E_n+1 представляется в виде

(x=y) = J_n((xy)Ù(yx)). □

Исследование моделей вычислений сводится к выражению арифметических операций и отношений в подходящих Ł-замкнутых классах с последующим анализом их функциональных свойств. Приведем результаты применения этого метода к машинным арифметикам -.

Теорема 3.1. Верны следующие утверждения.

1. Функции |+|, ||, ||, ||+||, ||||, |||| выразимы в Ł_n+1.
   
2. Система функций {|+|, ||} образует базис в классе Ł_n+1C^{0}_n+1, предполном в Ł_n+1.
   
3. Системы функций {~, |+|}, OAŁ_n+1 F {n, ||} являются базисами в Ł_n+1. □
   

Следствие 3.1.1. Система констант и функций арифметики с переполнением OA_n+1 полна в P_n+1. □

Предложение 3.13. Операция {/} обогащает Ł_n+1 до класса T_n+1. □

Положим

Nm(x) F	{	m, xEIn+1,
		~x, x{0,n},

где E^I_n+1  E_n+1\{0,n}.

Теорема 3.2. Для всякого mE^I_n+1 класс Ł[[]_m]_n+1 совпадает с Ł[N_m]_n+1, где символом []_m обозначается любая из функций [+]_m или []_m. □

Следствие 3.2.1. Функции []_m, mE^I_n+1, выражаются в Ł_n+1, если и только если n=p^s и m=tp^s-1, где p – простое число, s>0, 0<t<p. □

Следствие 3.2.2. Класс Ł[[]_m]_n+1 совпадает с T_n+1, если и только если n и m взаимно просты. □

Обозначим через M_n+1 класс функций, сохраняющих отношение равенства по модулю (=) системы MA_n+1 . Известно, что класс M_n+1 является предполным, но не слабо полным.

Теорема 3.3. Верны следующие утверждения.

1. Функции (+), (), () выразимы в Ł_n+1.
   
2. Система функций {(+), (), (), J_n} образует базис в некотором собственном подклассе класса Ł_n+1M_n+1.
   
3. Система функций
   

MAŁn+1 F	{	{(), J2, }, n=2
		{(+), (), Jn, }, n>2

образует базис в Ł_n+1. □

Следствие 3.3.1. Система констант и функций арифметики по модулю MA_n+1 неполна в P_n+1, но становится полной при добавлении функции max(x,y), (x,y)E_n+1E_n+1. □

Операции системы MA_n+1 можно рассматривать также как функции из P_n, поскольку E_n+1/(=)E_n, так что {f/(=)| fM_n+1}P_n. Положим F(+)/(=), F()/(=).

Предложение 3.15. Верны следующие утверждения.

1. Ни одна из функций системы {,} не является слабым штрихом Шеффера в P_n.
   
2. (С.В. Яблонский) Система {,} является слабо полной в P_n, если и только если n – простое число.
   
3. Система {,,}, где  – фактор-функция деления, согласованного с умножением по модулю n, является слабо полной в P_n. □
   

Рассмотрены логические структуры, возникающие при использовании представления чисел и операций в позиционных системах счисления. Р.к.п.п. рассматривается как отображение, ставящее в соответствие замкнутому классу K_b+1 функций на E_b+1 замкнутый класс K_b+1q функций на E_bq, имеющих р.к.п.п. функциями из K_b+1. Определяются также классы K_b+1^–q и K_b+1⁺q, состоящие из поразрядных и прогрессивных функций из K_b+1q соответственно.

Теорема 3.4. Верны следующие утверждения.

1. Класс K_b+1 совпадает с T_b+1, если и только если класс K_b+1q совпадает с T_bq для всякого q1.
   
2. Для всякого q>1 класс Ł[Ł_b+1q] совпадает с T_bq.
   
3. Для всякого q>1, если b=p^s, где p – простое число и s>0, то все прогрессивные функции из класса Ł_b+1⁺q (в частности, все функции b_j, j=0,…,q-1), выразимы в Ł_bq; в противном случае ни одна b_j не выразима в Ł_bq, а совокупность всех b_j обогащает Ł_bq до класса Ł⁺_bq F Ł[Ł_b+1⁺q] = Ł[Ł_b+1^–q] = F_bq({db^j| dD(b), j=0,…,q-1}).
   
4. Если b не является степенью простого числа, то для всякого q>1 система функций QPŁ_bq = {,b₀,b₀(+)b₁,…,b₀(+)…(+)b_q-2} образует базис в Ł⁺_bq. □
   

Следствие 3.4.1. Следующие утверждения эквивалентны:

1. b является простым числом;
   
2. класс Ł_b+1q совпадает с T_bq для всякого q1;
   
3. для всякого q>1 и всякой функции, выразимой в Ł_bq, существует к.п.п, все члены которого выразимы в Ł_b+1. □
   

Следствие 3.4.2. Функция g^q, получающаяся из функции g, выразимой в Ł_b+1, по правилу построения поразрядной логики, выразима в Ł_bq при всех q>1, если и только если b является степенью простого числа. □

Архитектурная декомпозиция распределенных систем. Когда алгоритмы спроектированы, выполняется фаза , в ходе которой они распределяются на отдельные вычислительные компоненты, и разрабатывается дисциплина обмена данными между ними. При этом надо учесть зависимости между отдельными шагами алгоритмов, обусловленные обменом данными, а также характеристики доступной вычислительной и коммуникационной аппаратуры. Для эффективного выполнения этой фазы предложены формальные методы архитектурной декомпозиции системы на базе ее алгоритмической модели.

Эти методы основаны на моделировании сценариев исполнения системы посредством счетных частично упорядоченных множеств TN,<, обладающих свойством фундированности (обрыва убывающих цепей). Частичный порядок порождается потоком актов обмена данными между различными состояниями компонентов и представляет коммуникационное время системы. На фундаментальный характер такого представления времени распределенных систем впервые указал В. Пратт⁷. Оно позволяет строить абстрактные «протомодели», не содержащие деталей структуры состояний и содержания данных. Такие протомодели подлежат обогащению с целью получения полноценных моделей архитектуры типа , или , для представления которых имеется ряд формальных нотаций (например, PVS, AsmL и ADŁ соответственно). Многие такие формализмы поддерживают различные методы декомпозиции и распараллеливания. На уровне абстрактных протомоделей результатом декомпозиции является их разбиение на протомодели отдельных компонентов, формализуемое в виде представления TN = _iTA_i. Анализ протомоделей позволяет выявить основные закономерности компонентной структуры систем, а также учесть требования к производительности.

Так, подсистемы, не взаимодействующие между собой в рамках данного сценария, естественным образом определяются как компоненты порядковой связности TN:

Определение 4.1. Отношением сравнимости ~ называется рефлексивное симметричное замыкание отношения порядка на TN:

t~t'  t=t't<t't'<t. □

Определение 4.2. Отношением порядковой связности ~^ называется транзитивное замыкание отношения сравнимости. □

В ходе декомпозиции также требуется выявлять последовательные подсистемы – максимальные интервалы жизненного цикла системы, в течение которых она ведет себя как изолированная последовательная программа. Установлено, что любая протомодель может быть разбита на непересекающиеся подмножества, представляющие последовательные подсистемы. Для их выявления разработаны следующие формальные конструкции.

Определение 4.3. Эквиотношением ## произвольного бинарного отношения # на множестве Y называется отношение

t##t'  t"Y ((t#t"t'#t")  (t"#tt"#t')). □

Определение 4.4. Отношением эквисравнимости  называется эквиотношение отношения сравнимости на TN. Симметричность отношения сравнимости сокращает формальное определение:

tt'  t"TN (t~t"t'~t"). □

Как обычно, (симметричный замкнутый) интервал определяется как множество вида [t,t']  {t}{t"TN| t<t"t"<t'}{t"TN| t'<t"t"<t}{t'}.

Определение 4.5. Отношение интервальной эквисравнимости _[] задается на TN следующим образом:

t_[]t'  t₁,t₂[t,t'] (t₁t₂). □

Показано, что интервальная эквисравнимость является отношением эквивалентности, усиливающим эквисравнимость. Кроме того, она сохраняет порядковую структуру TN, поскольку справедлива

Теорема 4.1. Любые две интервально неэквисравнимых точки относятся друг к другу так же, как их классы интервальной эквисравнимости, причем всякое отношение эквивалентности, обладающее этим свойством и не являющееся усилением интервальной эквисравнимости, отождествляет некоторые несравнимые точки. □

Определение 4.6. Отношение линейной эквисравнимости _L задается на TN следующим образом:

t_Lt'  tt't₁,t₂[t,t'] (t₁~t₂). □

Теорема 4.2. Линейная эквисравнимость совпадает с интервальной. □

Будем говорить, что отношение эквивалентности сохраняет ординально-предельную структуру TN, если любой его класс эквивалентности конечен либо изоморфен  (т.е. может представлять последовательный процесс).

Пусть  X – предикат, истинный, если X[0,n] для некоторого n.

Определение 4.7. Отношение полной эквисравнимости _ задается на TN следующим образом:

t_t'  tt'[t,t']. □

Теорема 4.3. Фактор-множество

TS(TN)  TN/_

имеет такую же порядковую и ординально-предельную структуру, что и TN. □

Таким образом, факторизация по отношению _ задает разбиение протомодели на последовательные подсистемы.

Более общая характеризация дисциплины обмена данными получается при выделении асинхронных подсистем, способных функционировать независимо (по времени) от своего окружения. Как невзаимодействующие, так и последовательные подсистемы асинхронны. Асинхронные подсистемы общего вида представляются подмножествами TN, отделимыми в следующем смысле.

Отношение #⁰ называется порождающим отношение #, если (#⁰)^=#. Сужением #| _X отношения # на подмножество X называется отношение #XX.

Определение 4.8. Подмножество X множества Y называется отделимым (относительно транзитивного отношения #), если сужение на него любого отношения, порождающего данное, коммутирует с транзитивным замыканием:

_#X  #⁰YY ((#⁰)^=#  (#⁰|_X)^=#|_X). □

Будем говорить, что конечное множество T_n+1(#,t,t')  {t₀,t₁,…,t_n} связывает две данные точки t и t' некоторым отношением # (не обязательно транзитивным), если t₀=t, t_n=t', и для всякого i=1,…,n выполнено t_i-1#t_i. Доказан следующий интервальный критерий отделимости.

Теорема 4.4. Подмножество X отделимо тогда и только тогда, когда для любых двух его точек, входящих в данное отношение, существует связывающее их множество, такое, что интервал между любыми соседними точками из этого множества содержится в X:

_#X  t,t'X (t#t'  T_n+1(#,t,t') (_i=1,…,n [t_i-1,t_i]X)). □

Отделимость относительно отношения порядка на TN тесно связана с понятием максимального пути. Как обычно, путем из t в t' называется линейно упорядоченное подмножество интервала [t,t'], содержащее его конечные точки, а максимальным называется путь, не содержащийся ни в каком другом пути.

Теорема 4.5. Подмножество X частично упорядоченного множества TN является отделимым тогда и только тогда, когда для любых двух его сравнимых точек существует связывающее их множество, такое, что любой максимальный путь, соединяющий эти точки и содержащий это множество, содержится в X. Точки такого множества называются узловыми точками интервала, соединяющего данные точки. □

Уровень абстрактности, присущий представленной технике, позволяет применить ее для формального описания и анализа различных шаблонов проектирования (design patterns), задающих типовые дисциплины обмена данными в распределенных системах. Например, протомодель многоопорной (multi-tier) архитектуры, являющейся расширением широко используемой коммуникационной архитектуры клиент-сервер, имеет вид TN = (_iTS_i)(_kTC_k)TD, где:

• TS_i, i=1,… – бесконечные процессы, выполняющие функции серверов-исполнителей;
  
• TC_k, k=1,… – клиенты, являющиеся связными совокупностями процессов, каждая из которых инициирует как начало, так и окончание взаимодействия с серверами, т.е. для каждого k выполняется условие
  

t_s,t_fTC_k tTC_k t'TS (t~t'  [t,t'][t_s,t_f]TS),

где TS  _iTS_i;

• TD – отделимый бесконечный процесс-диспетчер, который организует взаимодействие клиентов с исполнителями конкретных запросов: для каждого k выполняется условие
  

tTC_k t'TS (t<t'  t*TC_k (t*<t'  [t,t*]TD)).

Другим распространенным шаблоном проектирования является кластерная архитектура. Протомодель простейшего кластера, соответствующая массивно-параллельной организации вычислений (array computing), задается интервалом [t_s,t_f], который можно представить в виде {t_s}(_i_i){t_f}, где _i – счетные (как правило, конечные) ординальные числа, причем _i и _j являются порядково изолированными при всех ij, т.е. выполняется условие

t_i_i t_j_j (¬t_i~t_j).

По результатам архитектурной декомпозиции проектируется развертывание системы по доступным аппаратным единицам с учетом требований к производительности (PERF). Эти требования формализуются путем построения гомоморфного вложения τ:TN→ коммуникационного времени в континуум вещественных чисел с естественным порядком, который представляет физическое (реальное) время. Известно, что такое вложение существует для любого счетного TN. Оно позволяет описать длительность акта передачи данных между состояниями t<t' положительным вещественным числом d(t,t')  τ(t')-τ(t). Представление TN в виде графа, ребра которого помечены значениями длительности, позволяет использовать известные алгоритмы прокладки путей в графах⁸, оптимизирующие архитектуру системы с точки зрения производительности.

Реализация распределенных вычислительных систем. По завершении проектирования осуществляются программная реализация и тестирование системы, составляющие фазы - базового технологического цикла. Исходя из опыта автора по созданию распределенных вычислительных систем, проанализированы приемы обеспечения эффективности в ходе этих фаз.

Например, основной моделью целочисленных вычислений, реализованной в современных аппаратных средствах и воспроизводимой языками программирования, является арифметика MA_2q с побитовым хранением чисел. На аппаратном уровне выбор основания 2 оправдывается следствием 3.4.1 и утверждением теоремы 3.3; кроме того, к.п.п., посредством которого строятся операции, реализуется «бесплатно», путем коммутации входных и выходных линий. Однако на программном уровне отсутствие реализации предиката Carry в стандартных арифметических библиотеках усложняет контроль целочисленных переполнений, а функциональная неполнота системы MA_n+1 приводит к потребности в таких неэффективных операциях, как условный переход (следствие 3.3.1) или деление (предложение 3.15). Поэтому следует использовать специальные средства оптимизации моделей вычислений, предоставляемые различными аппаратными средствами. В частности, функциональная полнота обеспечивается многозначными арифметико-логическими устройствами, основанными на реализации операции || (см. арифметику с переполнением OA_n+1 ), достаточность которой вытекает из утверждения теоремы 3.1.

Для верификации соответствия программ формальным спецификациям применяется инспектирование текстов, в ходе которого идентифицируются структурные расхождения между фрагментами текста и конструкциями спецификации. Ключевым фактором эффективного инспектирования является высокий уровень логической структурированности текста. Для его обеспечения предложен подход, основанный на прагматической интерпретации законов традиционной логики в форме утверждений о фрагментах программ. В рамках этого подхода обоснованы такие технологические рекомендации, как недопустимость дублирования кода, нецелесообразность перманентного улучшения программ, однотипность реализационных решений.

Реализацию дисциплины обмена данными в работе рекомендовано выполнять из крупных структурных блоков, соответствующих подходящим шаблонам проектирования. Элементарным блоком такого рода является удаленный вызов процедуры (метода), поскольку он в точности воспроизводит характеристические свойства последовательной подсистемы (определение 4.7). Отмечается, что такой подход к реализации систем приводит к самоподобной структуре гомоморфизма τ. Кроме того, в силу статистического характера функционирования аппаратуры отображение τ оказывается случайным процессом. Поэтому для обеспечения надежности (RELY) в систему включаются модули самотестирования в ходе исполнения. Эффективность достигается в условиях случайных колебаний загрузки аппаратных ресурсов путем оснащения системы средствами динамической подстройки конфигурации развертывания. Подобные средства являются ключевыми при реализации динамических технологий распределенных вычислений, таких как GRID.

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

ОСНОВНЫЕ ВЫВОДЫ И РЕЗУЛЬТАТЫ РАБОТЫ

В диссертационной работе предложены новые теоретико-модельные методы анализа распределенных вычислительных систем, ориентированные на обеспечение требований эффективности в ходе разработки. Основные научные результаты, выводы и рекомендации состоят в следующем:

1. Построена модель качества на базе стандарта ISO/IEC 9126, в рамках которой формализованы нефункциональные требования к алгебраической абстрактности, производительности, ресурсоемкости и надежности, характеризующие эффективность распределенных вычислительных систем. Проанализированы подходы к обеспечению этих требований в ходе разработки.
   
2. Для построения формальных спецификаций моделей вычислений с учетом ресурсных ограничений разработан теоретико-модельный метод частичной интерпретации. С его помощью проанализированы модели вычислений в целых и рациональных числах.
   
3. Для обеспечения эффективного отображения вычислительных задач на архитектуру гетерогенных компьютерных систем предложен язык моделирования и анализа алгоритмов ADŁ, основанный на аппарате многозначной логики Лукасевича и ее обогащений. Модели вычислений представляются средствами этого языка в виде базисов логических функций.
   
4. Разработаны математические методы компонентной декомпозиции распределенных систем с учетом требований к производительности, основанные на моделировании сценариев обмена данными посредством частично упорядоченных множеств. Проанализированы такие шаблоны проектирования распределенных систем, как многоопорные и кластерные архитектуры.
   
5. Проанализированы следующие приемы обеспечения эффективности в ходе реализации распределенных вычислительных систем: оптимизация моделей вычислений и дисциплин обмена данными, инспектирование текстов программ, динамическая подстройка развертывания.
   

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Belov S.D., Bredikhin S.V., Kovalyov S.P., Kulagin S.A., Musher S.L., Scherbakova N.G., Shabalnikov I.V. The emerging Internet landscape in Siberia // Computer Networks, 30, 1998. P. 1657-1662.
   
2. Ковалев С.П. Принципы профессионального программирования // Смирновские чтения. 3 Международная конференция. М.: ИФРАН, 2001. С. 42-44.
   
3. Ковалев С.П. Применение законов логики к решению инженерных задач // Труды научно-исследовательского семинара Логического центра Института Философии РАН. Вып. XV. М.: ИФРАН, 2001. С. 46-56.
   
4. Ковалев С.П. Архитектура времени в распределенных информационных системах // Вычислительные технологии. Т. 7, №6, 2002. С. 38-53.
   
5. Ковалев С.П. Аналитические модели машинной арифметики // Сибирский журнал индустриальной математики. Т. 6, №3, 2003. С. 88-102.
   
6. Ковалев С.П. Логика Лукасевича как архитектурная модель арифметики // Сибирский журнал индустриальной математики. Т. 6, №4, 2003. С. 32-50.
   
7. Kovalyov S.P. On foundations of software engineering // 5th Intl. Conf. PSI'03. Bull. Workshop “Science Intensive Software”. Novosibirsk: IIS SB RAS, 2003. P. 34-38.
   

1 ISO/IEC 9126. Information Technology – Software Quality Characteristics and Metrics. Parts 1-4. Geneva: ISO/IEC, 1998.

2 Botella P., Burgués X., Franch X., Huerta M., Salazar G. Modeling non-functional requirements // Proc. JIRA'2001. Sevilla: 2001.

3 Воеводин В.В., Воеводин Вл.В. Параллельные вычисления. СПб.: БХВ-Петербург, 2002.

4 Смелянский Р.Л. Методы анализа и оценки производительности вычислительных систем. М.: МГУ, 1990.

5 Evans T., Schwartz P.B. On Słupecki T-functions // J. Symbolic Logic. Vol. 23, 1958. P. 267-270.

6 Карпенко А.С. Логики Лукасевича и простые числа. М.: Наука, 2000.

7 Pratt V.R. Modeling concurrency with partial orders // Intl. Journal of Parallel Programming. 15(1), 1986. P. 33-71.

8 Касьянов В.Н., Евстигнеев В.А. Графы в программировании: обработка, визуализация и применение. СПб.: БХВ-Петербург, 2003.