Previous Page  2 / 18 Next Page
Information
Show Menu
Previous Page 2 / 18 Next Page
Page Background

В.С. Буренков, С.Р. Иванов

50

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1

Решаемую в этой работе задачу можно сформулировать следующим образом.

Дано неформальное описание протокола когерентности наподобие

MOSI

[5], обес-

печивающего согласованность данных в

n

блоках кэш-памяти, каждый из которых

принадлежит отдельному процессорному ядру. Сформулирована спецификация

протокола когерентности в виде множества свойств-инвариантов, запрещающих

определенные комбинации состояний кэш-строки в кэшах системы. Необходимо

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

свойств при любом числе

n

кэшей.

Синтез математической модели для представления протоколов когерент-

ности.

Проведем синтез математической модели.

Модель протоколов когерентности.

Язык описания моделей

Promela

предла-

гает абстракции, представляющие группы устройств, работающих в соответствии с

протоколом когерентности (

процессы

, являющиеся конечными автоматами), и их

асинхронное взаимодействие (

каналы

, являющиеся

FIFO-

очередями). В связи с

этим математическая модель протоколов когерентности, используемая в настоя-

щей работе, основана на формальной семантике

Promela

-моделей и базируется на

модели, применяемой в работе [6].

Модель состоит из нескольких уровней.

Promela

-процессам соответствуют

графы программ. Асинхронная композиция графов программ описывается ка-

нальной системой. Путем «развертывания» канальной системы получается си-

стема переходов — стандартная модель аппаратных и программных систем.

Система переходов.

Системой переходов

TS

называется шестерка

,

, , ,

, ,

TS S Act

I AP L

где

S

— множество состояний;

Act

— множество дей-

ствий;

S Act S

  

— отношение переходов;

I S

— множество начальных

состояний;

AP

— множество атомарных высказываний;

:

2

AP

L S

— функция

пометок. Для краткости под обозначением

s s



будем понимать

, ,

.

s s

 

Если осуществляемое действие в таком контексте неважно, запишем

.

s s

 

Граф программы.

Поведение процессов описывается с помощью операто-

ров языка

Promela

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

,

Var

множество каналов модели —

.

Chan

Обозначим через

 

dom x

тип переменной

,

x

а через

 

dom c

— тип перемен-

ных, которые могут быть переданы через канал

.

c

Емкость канала

c

— максималь-

ное число сообщений, которое он способен хранить, — обозначим через

 

.

cap c

Интерпретацией

переменных называется отображение, ставящее в соот-

ветствие каждой переменной

v Var

значение

 

 

.

v dom v

 

Через

:

v r

 

обозначим интерпретацию переменных, присваивающую значение

r

перемен-

ной

v

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

через

Eval Var

множество интерпретаций переменных.

Интерпретация

каналов — отображение, ставящее в соответствие каждо-

му каналу

c Chan

последовательность

 

 

*

c dom c

 

такую, что

 

len c

 

 

,

cap c

где

 

len

— длина последовательности;

*

— звезда Клини.

Запись