Шпаргалка по "Программированию и компьютерам"

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

 

17. Верификация программ

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

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

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

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

Метод установления правильности программ при помощи строгих средств известен как верификация программ.

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

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

спецификацию ввода-вывода (описание данных, не зависящих от процесса обработки);

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

спецификации и свойства структурных подкомпонентов программы;

спецификацию структур данных, зависящих от процесса обработки.

К такому методу доказательства правильности программ относится метод индуктивных утверждений, независимо сформулированный К. Флойдом и П. Науром.

Суть этого метода состоит  в следующем:

1) формулируются входное  и выходное утверждения: входное  утверждение описывает все необходимые  входные условия для программы (или программного фрагмента), выходное утверждение описывает ожидаемый результат;

2) предполагая истинным  входное утверждение, строится промежуточное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями); такое утверждение называется выведенным утверждением;

3) формулируется теорема  (условия верификации):

из выведенного  утверждения следует выходное утверждение;

4) доказывается теорема;  доказательство свидетельствует  о правильности программы (программного  фрагмента).

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

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

из входного утверждения  следует выведенное утверждение.

Такой метод построения условий  верификации моделирует выполнение программы в обратном направлении. Другими словами, условия верификации должны отвечать на такой вопрос: если некоторое утверждение истинно после выполнения оператора программы, то, какое утверждение должно быть истинным перед оператором?

 

18. Синхронизация параллельных процессов на низком   уровне. Параллельная   обработка. Проблемы критических участков. Взаимоисключения.

Блокировка памяти:

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

− одному процессу разрешается выполнить  операцию засылки немедленно;

− другому процессу приходится ждать, пока первый не закончит.

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

Параллельная   обработка.  

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

Можно выделить четыре основных типа архитектуры систем параллельной обработки:

1) Конвейерная и векторная обработка. Основу конвейерной обработки составляет раздельное выполнение некоторой операции в несколько этапов (за несколько ступеней) с передачей данных одного этапа следующему. Производительность при этом возрастает благодаря тому, что одновременно на различных ступенях конвейера выполняются несколько операций.

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

3) Машины типа MIMD. MIMD компьютер имеет N процессоров, независимо исполняющих N потоков команд и обрабатывающих N потоков данных. Каждый процессор функционирует под управлением собственного потока команд, то естьMIMD компьютер может параллельно выполнять совершенно разные программы. 

4)  Многопроцессорные машины с SIMD-процессорами. Многие современные супер-ЭВМ представляют собой многопроцессорные системы, в которых в качестве процессоров используются векторные процессоры или процессоры типа SIMD. Такие машины относятся к машинам класса MSIMD.

Проблемы критических  участков. Задача синхронизации АПП в ОС решается методом взаимоисключения процессов при выполнении их на критических участках. Для взаимоисключения процессов на критических участках существует три средства: примитивы взаимоисключения, семафоры, мониторы.

Синхронизация потоков.  Методы взаимоисключений:

1. Запрещение прерываний при входе в критическую область и разрешение прерываний после выхода из критической области. Достоинства: простота реализации. Недостатки: монополизация процессора, возможный крах ОС при сбое процесса, невозможность использования в многопроцессорных системах.
2. Блокирующие переменные (программный подход)
3. Использование системных функций входа в критическую секцию
4. Семафоры Дийкстры

 

19. Блокировка  памяти, Аппаратная реализация взаимоисключения: команда “проверка и установка” (testandset), Семафоры, двоичные семафоры, мьютексы.

Взаимоисключения могут быть реализованы  аппаратно, если сделать операции над  памятью неделимыми. То есть, если каждый из процессов пытается поместить какие-либо значения в одну и ту же ячейку, то спор разрешается аппаратурой: если одному процессу разрешается выполнить операцию засылки немедленно, то другому приходится ждать пока первый не закончит операцию – такое разрешение спора и называется блокировкой памяти( storage interlock).

Семафор (semaphore) – это целая переменная, значение которой можно опрашивать и менять только при помощи специальных неделимых (как команда testandset) операций P и V. Эти операции являются примитивами относительно семафора, который указывается в качестве параметра операций. Здесь семафор выполняет роль вспомогательного критического ресурса, т.к. операции P и V неделимы при своем выполнении и взаимно исключают друг друга.

Двоичный семафор может принимать только значения 0 или 1. Считающий семафор может принимать целые неотрицательные значения.

Операция Р над семафором S записывается как P(S), алгоритм ее выполнения следующий:

if S>0 then S:=S-1 else <ожидать на S>

Операция V над семафором S , V(S), имеет  следующий алгоритм выполнения:

if <один или несколько процессов ожидают на S>

then <разрешить одному из этих процессов продолжить работу>

else S:=S+1

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

Алгоритм Деккера представляет собой программное решение проблемы взаимоисключения. Наличие аппаратной команды TS (testandset), которая осуществляет чтение переменной; запись ее значения в область сохранения и установку конкретного значения этой переменной, причем выполняет эти действия до конца без прерывания, значительно упрощает решение проблемы критического участка посредством блокировки памяти.

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

Основной недостаток использования  операций типа TS состоит в следующем: находясь в цикле проверки переменной common, процессы впустую потребляют время ЦП и другие ресурсы.

 

 

20. Синхронизация  параллельных процессов на высоком   уровне,  мониторы (50)

Монитор (monitor) – это набор процедур и информационных структур, которым процессы пользуются в режиме разделения, причем в каждый момент им может пользоваться только один процесс.

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

Внутренние данные монитора могут  быть либо глобальными, относящимися ко всем процедурам монитора, либо локальными, относящимися к одной процедуре. Ко всем данным можно обращаться только изнутри монитора. Говорят, что информация спрятана (information hiding).

Команды Wait () и Signal ().

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

 

21. Почтовые ящики,  Конвейеры (программные каналы), очереди сообщений.

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

Однонаправленные: процесс1 может посылать сообщения, пока имеются свободные гнезда. Если все гнезда заполнены, то процесс1 ждет/занимается другими делами.

Двунаправленный: - позволяет подтверждать прием сообщений. Если используется множество гнезд, то каждое из них хранит либо сообщение, либо подтверждение.

+процессу не нужно знать о сущ-и других процессов, пока не получит сообщение от них;

+два процесса могут обмениваться  более чем одним сообщением  за раз;

+ОС гарантирует, что никакой  процесс не вмешивается в работу других процессов;

-появление ресурса, которым  нужно управлять. 

-количество буферов фиксировано.

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