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

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


Смотрите также:
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени кандидата педагогических наук. М., 2000...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание учёной степени...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени...
Автореферат диссертации на соискание ученой степени...



Загрузка...
скачать
На правах рукописи


КОВАЛЁВ Сергей Протасович


АНАЛИЗ РАСПРЕДЕЛЕННЫХ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ

С ПРИМЕНЕНИЕМ ТЕОРЕТИКО-МОДЕЛЬНЫХ МЕТОДОВ




Специальность: 05.13.11 – математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей


Автореферат

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

кандидата физико-математических наук


Новосибирск – 2003


Работа выполнена в Институте вычислительных технологий СО РАН


Научный руководитель: член-корреспондент РАН

Федотов Анатолий Михайлович


Официальные оппоненты: доктор физико-математических наук

Вирбицкайте Ирина Бонавентуровна

кандидат физико-математических наук

Шрайнер Павел Александрович


Ведущая организация: Институт динамики систем и теории управления СО РАН


Защита состоится 29 декабря 2003 г. в 12 часов на заседании диссертационного совета Д003.060.01 по адресу:

просп. Ак. Лаврентьева, 6,

Новосибирск, 630090,

Россия


С диссертацией можно ознакомиться в читальном зале Отделения вычислительной математики и информатики ГПНТБ и ИВТ СО РАН.


Автореферат разослан 25 ноября 2003 г.


Ученый секретарь

диссертационного совета Л.Б. Чубаров

д.ф.-м.н., проф.

^

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ



Актуальность работы. Объемы вычислений, которые требуются для решения научных и прикладных задач, часто превышают возможности отдельного компьютера. Поэтому вычисления распределяются по нескольким одновременно функционирующим аппаратным единицам, объединенным в вычислительную сеть. При этом возникает ряд факторов, без учета которых не удается добиться реального выигрыша в эффективности: сложные взаимные зависимости между фрагментами задачи, гетерогенность используемой аппаратуры, случайные колебания загрузки аппаратных ресурсов. Имеющиеся подходы к решению таких проблем слабо интегрированы с современными общеупотребительными технологиями программирования, в том числе по причине относительной малочисленности и узкой специализации традиционных крупномасштабных распределенных вычислительных систем. Однако в настоящее время удешевление вычислительной аппаратуры и появление технологий класса GRID, позволяющих распределять вычисления по свободным ресурсам узлов сети Интернет, стимулируют создание распределенных информационно-вычислительных служб для широкого круга потребителей. Примерами таких служб являются прикладные системы обработки текстов и мультимедиа, анализа финансовых или медицинских данных. Намечается массовое возрождение вычислительных технологий, берущих начало еще от кластеров мэйнфреймов (mainframe) с автоматической диспетчеризацией задач, на качественно новом уровне. Для удовлетворения спроса на такие решения необходимо адаптировать современные методы разработки к данному классу систем.

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

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

^ Цель работы: разработать формальные методы анализа распределенных вычислительных систем, ориентированные на обеспечение требований эффективности.

Достижение этой цели требует решения следующих задач:

  • идентификация характеристик эффективности распределенных вычислительных систем и оценка возможности обеспечения ограничений на их значения посредством различных формальных методов;

  • разработка формальной процедуры учета ограничений на объем доступных ресурсов при анализе требований к вычислительным системам;

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

  • построение формальных методов архитектурной декомпозиции распределенных систем с учетом требований к производительности.

Эти задачи решены в работе с использованием методов теории моделей.

^ Научная новизна работы состоит в том, что предложены следующие математические методы анализа распределенных вычислительных систем, ориентированные на обеспечение требований к производительности, ресурсоемкости и надежности в ходе разработки:

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

  • представление модели вычислений слабо полным классом функций подходящей многозначной логики, обогащающей логику Лукасевича;

  • архитектурная декомпозиция распределенной системы на основе моделирования сценариев обмена данными посредством частично упорядоченных множеств.

Корректность предложенных методов обоснована рядом теорем, снабженных подробными доказательствами.

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

  • выбор формального метода разработки, позволяющего наиболее адекватно учесть нефункциональные требования к создаваемой системе;

  • обеспечение корректности модели вычислений при соблюдении ограничений на объем ресурсов, выделяемых для хранения числовых данных;

  • эффективное отображение алгоритмической модели на архитектуру гетерогенной компьютерной системы;

  • верификация вычислений с использованием техники доказательства теорем многозначной логики (в том числе автоматизированного);

  • архитектурная декомпозиция распределенных систем на основе анализа условий взаимной синхронизации компонентов.

Методы, представленные в работе, использовались автором при разработке распределенных вычислительных систем для задач ядерной физики, обработки мультимедиа-данных, семантического анализа текстов, а также при модернизации Сети Интернет Новосибирского научного центра. Кроме того, сформулированный подход положен в основу общего курса лекций «Сетевые технологии», который читается автором для студентов Факультета информационных технологий Новосибирского государственного университета.

^ Апробация работы. Результаты работы докладывались на следующих международных конференциях: Международная конференция «3 Смирновские чтения» (Москва, 2001); Международная конференция «Мальцевские чтения'2001» (Новосибирск, 2001); Международная конференция «Мальцевские чтения'2002» (Новосибирск, 2002); Международный конгресс «Математика в XXI веке» (Новосибирск, 2003); Семинар «Наукоемкое программное обеспечение» V Международной конференции «Перспективы систем информатики» (Новосибирск, 2003). Также работа была представлена на научных семинарах Института вычислительных технологий СО РАН, Института математики СО РАН, Института автоматики и электрометрии СО РАН, Института физики полупроводников СО РАН.

Публикации. По результатам выполненных исследований опубликовано 7 печатных работ.

^ Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы. Общий объем работы – 123 страницы, библиография содержит 140 наименований.

^

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



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

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

  1. алгебраическая абстрактность (ALG) – ориентация на абстрактный математический язык вычислительных задач, независимость от концепций компьютерных систем;

  2. производительность (PERF) – максимальная длительность выполнения различных вариантов использования;

  3. ресурсоемкость (RES) – объем ресурсов, выделяемых для хранения данных;

  4. надежность (RELY) – способность функционировать в нештатных условиях.

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

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



Формализм

ALG

PERF

RES

RELY



Семантические сети и онтологии

+









Абстрактные типы данных

+









Частичная интерпретация

+



+

+



Денотационное описание поведения



+

+

+



Алгебры процессов







+



Логический (дедуктивный) подход

+









Структуры Крипке



+

+

+



Мутирующие алгебры

+





+



Структурный анализ











Объектно-ориентированный подход







+



Компонентное проектирование



+

+

+

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

      1. формирование спецификации моделей вычислений с учетом требований к диапазону и точности обрабатываемых чисел;

      2. проектирование вычислительных алгоритмов;

      3. компонентная декомпозиция и разработка дисциплины обмена данными с учетом требований к производительности;

      4. реализация и верификация компонентов;

      5. реализация протоколов обмена данными и развертывание системы;

      6. сборочное тестирование;

      7. ввод в эксплуатацию и сопровождение системы.

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

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

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

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

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

Пусть C(0)  {c1,…,cn} – множество константных символов сигнатуры 0. Релятивизацией формулы  на 0 называется формула 0, получающаяся из  заменой всех подформул вида x0(x0,x1,…,xk) конъюнкциями i=1,…,n(ci,x1,…,xk) и вида x0(x0,x1,…,xk) – дизъюнкциями i=1,…,n(ci,x1,…,xk). Будем говорить, что пара áA,0ñ поддерживает предложение , если A 0.

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

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

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

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

  1. x (¬0Sx) (0 является начальным элементом);

  2. xy (SxSyxy) (функция следования S инъективна);

  3. для всякой формулы (x0,x1,…,xk) сигнатуры  верно

x1…xk[(0,x1,…,xk)  (x0(x0,x1,…,xk)(Sx0,x1,…,xk)) 

x0(x0,x1,…,xk)]

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

  1. для всякого i>0 выполнено ciSi0, где SiSS (i раз).

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

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

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

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

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

  2. A Scn-10.

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

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

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

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

OAn+1  áEn+1, 0, 1, …, n-1, =, |+|, ||, ||ñ,

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

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

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

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

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

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

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

BAn+1,m  áEn+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 строится по стандартной рекурсивной схеме.

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

MAn+1  áEn+1, 0, 1, …, -1, (=), (+), (), (), Carryñ,

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

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

() xn-x,

x () yxy mod n,

Carry(x)  (x=n).

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

x {/} y

{

n, y=0 либо x=n

[x/y] в остальных случаях.

Рассмотрено представление целых чисел в позиционной системе счисления. Поскольку одноразрядные операции в b-ичной системе счисления осуществляется по модулю b (причем перенос учитывается в следующем разряде), арифметика q-разрядных чисел должна содержать флаг переноса, соответствующий значению bq. Поэтому она интерпретируется на универсуме Ebq, где bqbq+1, с помощью изоморфного вложения :EbqEb+1q, которое задается разложением числа x на слагаемые вида bj(x)=xjbj, 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:EbqkEbq может быть задана посредством квазипостовского представления (к.п.п.) – совокупности функций {fj:Eb+1qkEb+1| j=0,…,q 1} такой, что если разложение каждого xi по основанию b имеет вид xi=∑jxi,jbj, то разложение f(x1,…,xk) имеет вид f(x1,…,xk)=∑jfj(x1,0,…,x1,q 1,…,xk,0,…,xk,q 1)bj. Регулярным (р.к.п.п.) называется представление посредством семейства, отображающего множество codom  = Ebq({0}q 1{b}) в себя. Если функция f:EbqkEbq строится посредством р.к.п.п. из некоторой функции g:Eb+1kEb+1 по правилу fj(x1,0,…,xk,q 1)=g(x1,j,…,xk,j), то она называется функцией поразрядной логики; если f имеет такое р.к.п.п., в котором каждая fj зависит только от (x1,j,…,xk,j)Eb+1k, то она называется поразрядной; а если такое, в котором каждая fj зависит только от (x1,0,…,x1,j,…,xk,0,…,xk,j)Eb+1(j+1)k, то прогрессивной.

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

FPb {abr-N| a[bN-1,bN-1],r[-R,R]}  {ab-(R+N+1)| a[0,bN-1-1]}

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

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

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

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

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

~x F n-x,

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

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

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

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

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

Ji(x) F

{

n, x=i,

0, xi.

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

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

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

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

Слабая полнота Łn+1 была доказана Эвансом и Шварцем5. А.С. Карпенко доказал6, что для всякого Ł-замкнутого класса Kn+1 существует такое YEn+1, что Kn+1 совпадает с классом Fn+1(Y) F uY CV(u)n+1, где V(u) F {vEn+1| uD(v)}, а D(x) – множество делителей числа x. В частности, Łn+1 содержится в предполном классе Tn+1 F C{0,n}n+1. Более того, любые арифметические отношения выражаются в Łn+1 функциями вида f:En+1k{0,n}. Например, имеет место

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

(x=y) = Jn((xy)Ù(yx)). □

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

Теорема 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. Система констант и функций арифметики с переполнением OAn+1 полна в Pn+1. □

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

Положим

Nm(x) F

{

m, xEIn+1,

~x, x{0,n},

где EIn+1En+1\{0,n}.

Теорема 3.2. Для всякого mEIn+1 класс Ł[[]m]n+1 совпадает с Ł[Nm]n+1, где символом []m обозначается любая из функций [+]m или []m. □

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

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

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

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

  1. Функции (+), (), () выразимы в Łn+1.

  2. Система функций {(+), (), (), Jn} образует базис в некотором собственном подклассе класса Łn+1Mn+1.

  3. Система функций

MAŁn+1 F

{

{(), J2, }, n=2

{(+), (), Jn, }, n>2

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

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

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

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

  1. Ни одна из функций системы {,} не является слабым штрихом Шеффера в Pn.

  2. (С.В. Яблонский) Система {,} является слабо полной в Pn, если и только если n – простое число.

  3. Система {,,}, где  – фактор-функция деления, согласованного с умножением по модулю n, является слабо полной в Pn. □

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

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

  1. Класс Kb+1 совпадает с Tb+1, если и только если класс Kb+1q совпадает с Tbq для всякого q1.

  2. Для всякого q>1 класс Ł[Łb+1q] совпадает с Tbq.

  3. Для всякого q>1, если b=ps, где p – простое число и s>0, то все прогрессивные функции из класса Łb+1+q (в частности, все функции bj, j=0,…,q-1), выразимы в Łbq; в противном случае ни одна bj не выразима в Łbq, а совокупность всех bj обогащает Łbq до класса Ł+bq F Ł[Łb+1+q] = Ł[Łb+1q] = Fbq({dbj| dD(b), j=0,…,q-1}).

  4. Если b не является степенью простого числа, то для всякого q>1 система функций QPŁbq = {,b0,b0(+)b1,…,b0(+)…(+)bq-2} образует базис в Ł+bq. □

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

  1. b является простым числом;

  2. класс Łb+1q совпадает с Tbq для всякого q1;

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

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

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

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

Так, подсистемы, не взаимодействующие между собой в рамках данного сценария, естественным образом определяются как компоненты порядковой связности 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"#tt"#t')). □

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

tt'  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'  t1,t2[t,t'] (t1t2). □

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

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

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

tLt'  tt't1,t2[t,t'] (t1~t2). □

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

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

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

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

tt'  tt'[t,t']. □

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

TS(TN)  TN/

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

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

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

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

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

#X  #0YY ((#0)=#  (#0|X)=#|X). □

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

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

#X  t,t'X (t#t'  Tn+1(#,t,t') (i=1,…,n [ti-1,ti]X)). □

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

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

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

    • TSi, i=1,… – бесконечные процессы, выполняющие функции серверов-исполнителей;

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

ts,tfTCktTCkt'TS (t~t'  [t,t'][ts,tf]TS),

где TS  iTSi;

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

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

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

tiitjjti~tj).

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

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

Например, основной моделью целочисленных вычислений, реализованной в современных аппаратных средствах и воспроизводимой языками программирования, является арифметика MA2q с побитовым хранением чисел. На аппаратном уровне выбор основания 2 оправдывается следствием 3.4.1 и утверждением теоремы 3.3; кроме того, к.п.п., посредством которого строятся операции, реализуется «бесплатно», путем коммутации входных и выходных линий. Однако на программном уровне отсутствие реализации предиката Carry в стандартных арифметических библиотеках усложняет контроль целочисленных переполнений, а функциональная неполнота системы MAn+1 приводит к потребности в таких неэффективных операциях, как условный переход (следствие 3.3.1) или деление (предложение 3.15). Поэтому следует использовать специальные средства оптимизации моделей вычислений, предоставляемые различными аппаратными средствами. В частности, функциональная полнота обеспечивается многозначными арифметико-логическими устройствами, основанными на реализации операции || (см. арифметику с переполнением OAn+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.




Скачать 441,38 Kb.
оставить комментарий
Дата17.10.2011
Размер441,38 Kb.
ТипАвтореферат диссертации, Образовательные материалы
Добавить документ в свой блог или на сайт

Ваша оценка этого документа будет первой.
Ваша оценка:
Разместите кнопку на своём сайте или блоге:
rudocs.exdat.com

Загрузка...
База данных защищена авторским правом ©exdat 2000-2017
При копировании материала укажите ссылку
обратиться к администрации
Анализ
Справочники
Сценарии
Рефераты
Курсовые работы
Авторефераты
Программы
Методички
Документы
Понятия

опубликовать
Загрузка...
Документы

наверх