Формальная модель операционной системы многопроцессорной ЭВМ

Рассмотрим работу блоков ОС в виде формальной модели для абстрактной многопроцессорной ЭВМ. Т=[t₀,t₁], где t₀ –время инициирования, t₁- время уничтожения системы. Структура ОС в некоторый момент времени tєT может быть представлен графом Г_t, где Р={p₀,p₁…p_n}- класс процессов, R ={r₁, r₂,…,r_q} – класс ресурсов. Элементы множеств являются вершинами графа Г_t. Считаем, что P и R конечные и непустые множества. Т.к. ОС является динамически изменяющейся системой, то в некоторый момент времени t₁, t₂ єT; t₁≠t₂ структура может быть представлена графами Г_t1­, Г_t2. Рассмотрим изменение графа Г_t, отражающего структуру ОС в любой момент времени tєT. Выделим в некоторое множество σ все возможные вершины и ребра, которые могут быть получены [t₀,t_k]. Каждый элемент множества σ (вершину или ребро) обозначим через σ_j j≥1. Определим множество Е как совокупность правил, фиксирующих изменение структуры графа Г_t для любого tєT. Каждое правило из множества Е будет иметь вид:

Где номер правила.

означает, что в момент времени tєT заменяется на набор элементов

означает номер правила, на которое осуществляется переход, если активен или блокирован.

Пусть V – множество номеров правил из Е. σ₀ некоторый начальный процесс, инициирующий работу системы. Тогда М – формальная модель ОС, может быть определена:М=<Т,σ, Е, V, σ₀>

5. Математическое определение графа Γ_t, отображающего структуру ОС в момент tєТ.

Рассмотрим работу блоков ОС в виде формальной модели для абстрактной многопроцессорной ЭВМ. Т=[t₀,t₁], где t₀ –время инициирования, t₁- время уничтожения системы. Структура ОС в некоторый момент времени tєT может быть представлен графом Г_t, где Р={p₀,p₁…p_n}- класс процессов, R ={r₁, r₂,…,r_q} – класс ресурсов. Элементы множеств являются вершинами графа Г_t. Считаем, что P и R конечные и непустые множества. Т.к. ОС является динамически изменяющейся системой, то в некоторый момент времени t₁, t₂ єT; t₁≠t₂ структура может быть представлена графами Г_t1­, Г_t2. Рассмотрим изменение графа Г_t, отражающего структуру ОС в любой момент времени tєT. Выделим в некоторое множество σ все возможные вершины и ребра, которые могут быть получены [t₀,t_k]. Каждый элемент множества σ (вершину или ребро) обозначим через σ_j j≥1. Определим множество Е как совокупность правил, фиксирующих изменение структуры графа Г_t для любого tєT. Каждое правило из множества Е будет иметь вид:

Где номер правила.

означает, что в момент времени tєT заменяется на набор элементов

означает номер правила, на которое осуществляется переход, если активен или блокирован.

Пусть V – множество номеров правил из Е. σ₀ некоторый начальный процесс, инициирующий работу системы. Тогда М – формальная модель ОС, может быть определена:М=<Т,σ, Е, V, σ₀>

6. Понятие ориентированного и неориентированного рёбер графа структуры ОС.

Обозначим через граф процессов. При , а класс в некоторый момент времени t. Если р₀ начальный процесс, то . Будем считать, что с каждой вершиной (процессом) связан некоторый граф граф ресурсов, требуемых для нормального развития. Тогда граф Г_t определяется так:

Вершины графа могут быть соединены ориентированными и неориентированными ребрами. Ориентированное ребро указывает, что вершина P_{b ­}находится в подчинении Р_а , т.е Рь является потомком Ра. Неориентированное ребро указывает, что существует связь между Ра и Рь. Считается, что все вершины графа располоагаются по уровням, причем на нулевом уровне находится существенная вершина Р₀. На уровне U i ≥1 находятся вершины, каждая из которых завясят хотя бы от одной вершины предыдущего уровня и не зависят от последующих уровней. одноуровневые вершины не зависят друг от друга. Например, пусть некоторый процесс Ра, расположенный в графе Гt на уровне U₁ порождает процессы Рь и Рс, расположенные на уровне U₂ и U_3­. Для нормальной работы процесса Ра требуются ресурсы r₁, r₂, r₃, где ресурс r₃ ресурс типа «память с сегментами» r₃₁, r₃₂, r₃₃ . для работы процессора требуются ресурсы в виде: для Рь – r₁, r₄, r₅, для Рс – r₁, r₆

Ребра ориентированные, указывают что Рь и Рс являются потомками Ра.

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