k
(
x)]] удовлетворяет следующей спецификации: если k > 0, то для каждого процесса P
M EM
k
(
x) |
α!m . β!u . γ?y . P
!
\ {α, β, γ}
+
≈
+
≈
(x m
:= u) . M EM
k
(
x) |
(y := x m
) . P
!
\ {α, β, γ}
Операция
• чтения значения, содержащегося в ячейке процесса
[[M EM
k
(
x)]]
по адресу m (без изменения содержимого этой ячейки), и
• занесения этого значения в переменную y процесса P
представляется процессным выражением
M EM
k
(
x) |
α!m . β!0 . γ?y . α!m . β!y . γ?z . P
!
\ {α, β, γ}
(где z 6∈ P )
(9.2)
306
Читателю предлагается самостоятельно доказать, что
(9.2)
+
≈
M EM
k
(
x) |
(y := x m
) . P
!
\ {α, β, γ}
Можно изменить определение процесса [[M EM
k
(
x)]] так, что- бы новый процесс удовлетворял спецификации
M EM
k
(
x)
+
≈
+
≈ α?m.
β?y . (x m
:= y) . M EM
k
(
x) + γ!x m
. M EM
k
(
x)
т.е.
• сначала в процесс [[M EM
k
(
x)]] вводится адрес m,
• а потом, в зависимости от выбора окружающей среды,
– либо в [[M EM
k
(
x)]] записывается новое значение по ад- ресу m
– либо читается значение, хранящееся в [[M EM
k
(
x)]] по адресу m
Для этого надо по-другому определить процесс [[M EM
0
(x)]]:
M EM
0
(x) = β?y . M EM
0
(y) + γ!x . M EM
0
(x)
Работа с новым процессом [[M EM
k
(
x)]] происходит следую- щим образом.
Операция записи значения выражения e в ячейку по адресу m представляется процессным выражением
M EM
k
(
x) | α!m . β!e . 0
Операция чтения процессом P значения, записанного в ячей- ке процесса [[M EM
k
(
x)]] по адресу m, и занесения этого зна- чения в переменную y процесса P , представляется процесс- ным выражением
M EM
k
(
x) | α!m . γ?y . P
307
9.3
СД “стек”
Стек – это СД с точками доступа α и γ, с которой можно вы- полнять следующие операции:
1. положить значение v в стек (действие α ! v)
2.
если стек непуст, то взять головной элемент стека (действие
γ ? x).
СД “стек” представляется совокупностью процессных выра- жений
{P U SH
n
(x
1
, . . . , x n
) | n ≥ 0}
(9.3)
где для каждого n ≥ 0
P U SH
n
– процессное имя, и ПВ
P U SH
n
(x
1
, . . . , x n
)
представляет процесс “стек, хранящий n значений”.
Процессы, соответствующие ПВ из совокупности (9.3) опре- деляются следующим РО:
1. P U SH
0
= α?x . P U SH
1
(x) + γ!$ . 0 2. для каждого n ≥ 0
P U SH
n+1
(x, x
1
, . . . , x n
) =
=
CELL(x) |
P U SH
n
(x
1
, . . . , x n
)[β/α, δ/γ]
!
\ {β, δ}
где ПВ CELL(x) представляет процесс с точками доступа α, β,
γ, δ,
называемый ячейкой памяти, и определяемый следующим образом:
CELL(x) =
=
α?y . β!x . CELL(y) +
γ!x . δ?y .
(y = $) ? P U SH
0
+ (y 6= $) ? CELL(y)
!
Потоковый граф процесса [[P U SH
n
(x
1
, . . . , x n
)]] имеет следу- ющий вид:
308
'
&
$
%
CELL(x
1
)
'
&
$
%
'
&
$
%
e u
e u
u e
e u
e u
u e
α
γ
-
-
-
β
δ
β
δ
β
δ
CELL(x n
)
P U SH
0
Читателю предлагается самостоятельно доказать, что сово- купность процессов, соответствующих ПВ из (9.3), удовлетворя- ет следующей спецификации: для каждого n ≥ 0
P U SH
n+1
(x, x
1
, . . . , x n
)
+
≈
α?y . P U SH
n+2
(y, x, x
1
, . . . , x n
)+
γ!x . P U SH
n
(x
1
, . . . , x n
)
!
9.4
СД “очередь”
Очередь – это СД с точками доступа α и γ, с которой можно выполнять следующие операции:
1. добавить значение v в конец очереди (действие α ! v)
2. если очередь непуста, то взять первый элемент очереди
(действие γ ? x).
СД “очередь” представляется совокупностью процессных выра- жений
{QU EU E
n
(x
1
, . . . , x n
) | n ≥ 0}
(9.4)
где для каждого n ≥ 0
QU EU E
n
– процессное имя, и ПВ
QU EU E
n
(x
1
, . . . , x n
)
представляет процесс “очередь, хранящая n значений”.
Процессы, соответствующие ПВ из совокупности (9.4) опре- деляются следующим РО:
1. QU EU E
0
= α?x . QU EU E
1
(x) + γ!$ . 0 2. для каждого n ≥ 0
QU EU E
n+1
(x, x
1
, . . . , x n
) =
=
CELL(x) |
QU EU E
n
(x
1
, . . . , x n
)[β/α, δ/γ]
!
\ {β, δ}
309
где ПВ CELL(x) представляет процесс с точками доступа α, β,
γ, δ, называемый ячейкой памяти, и определяемый следующим образом:
CELL(x) =
=
α?y .
β!x . CELL(y) + γ!x . CELL(y)
+
γ!x . δ?y .
(y = $) ? QU EU E
0
+ (y 6= $) ? CELL(y)
Потоковый граф процесса [[QU EU E
n
(x
1
, . . . , x n
)]] имеет такой же вид, как и потоковый граф в пункте 9.3.
Читателю предлагается самостоятельно доказать, что сово- купность процессов, соответствующих ПВ из (9.4), удовлетворя- ет следующей спецификации: для каждого n ≥ 0
QU EU E
n+1
(x, x
1
, . . . , x n
)
+
≈
+
≈
α?y . QU EU E
n+2
(x, x
1
, . . . , x n
, y) +
γ!x . QU EU E
n
(x
1
, . . . , x n
)
!
310
Глава 10
Семантика языка параллельного программирования
Семантика языка программирования представляет собой пра- вило, сопоставляющее каждой конструкции этого языка некото- рый математический объект. В качестве такого объекта может выступать, например, логическая формула или процессное вы- ражение.
Главной целью определения семантики языка программиро- вания является сведение задач анализа свойств программ на этом языке к задачам анализа математических утверждений, соответ- ствующих этим свойствам.
В этой главе мы рассмотрим в качестве примера определе- ние семантики простейшего языка параллельного программиро- вания в терминах теории процессов.
10.1
Описание
языка параллельного про- граммированияВ этом параграфе мы описываем простейший язык параллельно- го программирования, который мы будем обозначать символом
L.
311
10.1.1
Конструкции языка L
Конструкции языка L делятся на следующие три класса.
1. Выражения.
Понятие выражения языка L совпадает с аналогичным по- нятием, определённым в параграфе 7.2.3. Выражения стро- ятся из переменных, констант и ФС. Каждому выражению e сопоставлен некоторый тип type(e).
2. Декларации.
Каждая декларация D имеет один из следующих трёх ви- дов:
(a) объявление локальной переменной:
VAR x
(10.1)
где x – имя переменной
(b) объявление ресурса:
RESOURCE R
(10.2)
где R - имя ресурса, который может представлять со- бой, например, устройство ввода или вывода
(c) описание процедуры:
PROCEDURE G(u, v) IS C
(10.3)
где
• G – имя процедуры,
• u – переменная, изображающая аргумент проце- дуры
• v – переменная,
изображающая результат проце- дуры• C – оператор (тело процедуры), в который пере- менные u и v входят как формальные параметры этой процедуры.
312
3. Операторы.
Каждый оператор представляет собой описание некоторого алгоритма.
Ниже
• операторы обозначаются символом C
• декларации обозначаются символом D
• переменные обозначаются символами x, y, z, u, v, . . .
• выражения обозначаются символом e
• формулы (т.е. выражения типа bool) обозначаются сим- волом b причём при всех этих символах могут быть индексы.
Операторы имеют следующий вид.
(a) присваивание:
x := e где type(x) = type(e)
(b) условный переход:
if b then C
1
else C
2
(c) цикл:
while b do C
(d) ввод:
input x
(e) вывод:
output e
(f) пустой оператор:
skip
(g) последовательная композиция:
C
1
; C
2 313
(h) параллельная композиция:
C
1
par C
2
(i) блок:
begin {D
1
, . . . , D
k
; C} end
Блок “связывает” все вхождения объектов, объявлен- ных в декларациях D
1
, . . . , D
k
: эти объекты являются видимыми только внутри этого блока.
(j) вызов процедуры:
call G(e, z)
где
• G – имя вызываемой процедуры,
• e – выражение, значение которого является аргу- ментом процедуры G, и
• z – переменная, в которую будет занесён результат выполнения процедуры G.
(k) связывание оператора с ресурсом:
with R do C
где R – имя некоторого ресурса.
10.1.2
Программы на языке L
Программа на языке L представляет собой оператор begin {D
1
, . . . , D
k
; C} end где все переменные, ресурсы, и процедуры, имена которых вхо- дят в C, объявлены
• в декларациях D
1
, . . ., D
k
,
• или в тех декларациях, которые содержатся в C.
Программа может взаимодействовать с окружающей средой только путём выполнения операторов ввода и вывода.
314
10.2
Семантика языка L
В этом параграфе мы определяем семантику языка L, которая представляет собой правило, сопоставляющее каждой конструк- ции Q языка L некоторое ПВ h|Q|i, называемое семантикой кон- струкции Q.
При определении этой семантики мы будем использовать сле- дующие обозначения и соглашения.
1. В каждом ПВ B, соответствующем какой-либо конструк- ции языка L, знакосочетания
δ!,
ρ!,
i?
и o!
обозначают действия, имеющие заранее предопределённый смысл:
(a) δ! обозначает сигнал о завершении исполнения процес- са, соответствющего процессному выражению B
(b) ρ! обозначает вывод значения, являющегося результа- том работы процесса, соответствующего процессному выражению B
(c) i? обозначает ввод значения в программу
(d) o! обозначает вывод значения из программы
2. Символ done обозначает ПВ δ! . 0 3. Для каждой пары ПВ B
1
, B
2
(a) знакосочетание B
1
before B
2
обозначает ПВ
B
1
[β/δ] | β?.B
2
\ {β}
где β не входит в B
1
и B
2
(b) знакосочетание B
1
result B
2
обозначает ПВ
(B
1
| B
2
) \ {ρ}
315
(c) знакосочетание B
1
par B
2
обозначает ПВ
B
1
[δ
1
/δ] |
B
2
[δ
2
/δ] |
δ
1
!.δ
2
!.done + δ
2
!.δ
1
!.done
\ {δ
1
, δ
2
}
где δ
1
и δ
2
не входят в B
1
и B
2 4. Для каждого объекта с именем n, объявленного в неко- торой декларации D, символ L
n обозначает подмножество множества N ames, состоящее из точек доступа к этому объекту:
L
n def
=
{α
x
, γ
x
, π
x
, ϕ
x
}, если D = (10.1)
{π
R
, ϕ
R
},
если D = (10.2)
{α
G
, γ
G
},
если D = (10.3)
Если имена n
1
и n
2
таких объектов различны, то
L
n
1
∩ L
n
2
= ∅
10.2.1
Семантика выражений
Каждому выражению e языка L соответствует ПВ h|e|i, опреде- ляемое индукцией по построению выражения e:
• для каждой переменной x ∈ V ar h|x|i def
= γ
x
?y. ρ!y. 0
• для каждой константы c ∈ Con h|c|i def
= ρ!c. 0
• для каждого ФС f h|f (e
1
, . . . , e n
)|i def
=
def
=
h|e
1
|i [ρ
1
/ρ] | . . . | h|e n
|i [ρ
n
/ρ] |
ρ
1
?x
1
. . . . ρ
n
?x n
. ρ! f (x
1
, . . . , x n
) . 0
!
\ {ρ
1
, . . . , ρ
n
}
316
10.2.2
Семантика деклараций
При описании семантики деклараций мы будем использовать вспомогательные ПВ, соответствующие процессам, определяемым в виде РО:
• REG
x
(y) = α
x
?z . REG
x
(z) + γ
x
!y . REG
x
(y)
([[REG
x
(y)]] = регистр для хранения значения переменной x)
• LOC
x def
= α
x
?y . REG
x
(y)
(регистр без начального содержания)
• SEM
x
= π
x
! . ϕ
x
! . SEM
x
• SEM
R
= π
R
! . ϕ
R
! . SEM
R
Семантика деклараций имеет следующий вид.
1. Если D = VAR x, то h|D|i def
= LOC
x
| SEM
x
2. Если D = RESOURCE R, то h|D|i def
= SEM
R
3. Если D = PROCEDURE G(u, v) IS C, то процессному выра- жению h|D|i соответствует РО
h|D|i =
LOC
u
|
LOC
v
|
α
G
?x . α
u
!x . ((h|D|i | h|C|i) \ L
G
)
before γ
v
?y . γ
G
!y . h|D|i
\ (L
u
∪ L
v
)
Если в РО для h|PROCEDURE . . . |i вместо
(h|D|i | h|C|i) \ L
G
было бы написано просто h|C|i, то
неправильно транслировались бы такие процедуры, которые рекурсивно вызывают сами себя,
т.е. такие G, в теле которых есть оператор call G.
317
Вышеприведённая семантика деклараций вида (10.3) являет- ся неидеальной. Она неправильно сопоставляет ПВ таким опе- раторам, в которых есть параллельные вызовы одной и той же процедуры, например, оператору вида call G(6, z) par call G(7, w)
Если известно максимальное число n доступных процессоров
(т.е. одновременно n процедур могут быть активными), то семан- тику декларации D вида (10.3) лучше определить в виде РО
h|D|i = h|D|i
1
| . . . | h|D|i n
∀ i = 1, . . . , n h|D|i i
= α
G,i
?x .
LOC
u
|
LOC
v
|
α
u
!x . ((h|D|i | h|C|i) \ L
G
)
before γ
v
?y . γ
G,k
!y . h|D|i i
\ (L
u
∪ L
v
)
(10.4)
где L
G
def
= {α
G,1
, . . . , α
G,n
, γ
G,1
, . . . , γ
G,n
}.
10.2.3
Семантика операторов
1. h|x := e|i def
= π
x
? . h|e|i result (ρ?y . α
x
!y . ϕ
x
? . done)
2. h|C
1
; C
2
|i def
= h|C
1
|i before h|C
2
|i
3. h|if e then C
1
else C
2
|i def
=
def
= h|e|i result ρ?x . (x ? h|C
1
|i + ¬x ? h|C
2
|i)
4. если C = while e do C
0
, то ПВ h|C|i связано со следующим
РО:
h|C|i = h|e|i result (ρ?x.
x ? h|C
0
|i before h|C|i +
¬x ? done
!
)
5. h|begin {D
1
, . . . , D
k
; C} end|i def
=
def
= (h|D
1
|i | . . . | h|D
k
|i | h|C|i) \ (L
D
1
∪ . . . ∪ L
D
k
)
6. h|C
1
par C
2
|i def
= h|C
1
|i par h|C
2
|i
318
7. h|input x|i def
= i?y . α
x
!y . done
8. h|output e|i def
= h|e|i result (ρ?x . o!x . done)
9. h|skip|i def
= done
10. h|call G(e, z)|i def
=
def
= h|e|i result (ρ?x . α
G
!x . γ
G
?z . α
z
!z . done)
11. h|with R do C|i def
= π
R
? . h|C|i before (ϕ
R
? . done)
Если известно максимальное число n доступных процессо- ров (т.е. одновременно n процедур могут быть активными), и семантика деклараций вида (10.3) определяется в соответствии с (10.4), то семантику оператора call G(e, z) следует определить следующим образом:
h|call G(e, z)|i def
=
def
= h|e|i result (ρ?x .
n
P
i=1
α
G,i
!x . γ
G,i
?z . α
z
!z . done)
Читателю предлагается самостоятельно
• определить семантику каких-либо современных языков па- раллельного или распределённого программирования (MPI
и т.п.) или языков проектирования бизнес-процессов (BEPL
и т.п.), и
• разработать на основе этой семантики автоматизирован- ную систему доказательства свойств программ или описа- ний систем на этих языках.
319
Глава 11
Исторический обзор и современное состояние дел
Теория процессов объединяет
несколько направлений исследова- ний, каждое из которых отражает определённый подход к моде- лированию и анализу процессов. Ниже мы рассматриваем наи- более крупные из этих направлений.
11.1
Робин Милнер
Наибольший вклад в теорию процессов внёс выдающийся ан- глийский математик Робин Милнер (см. [1] - [5]).
Робин Милнер родился в 1934 г. в г. Плимуте (Англия) в семье военного офицера. В настоящее время (с 1995 г.) он ра- ботает профессором информатики в университете Кембриджа
(http://www.cam.ac.uk). С января 1996 г. по октябрь 1999 г.
Милнер занимал должность руководителя Компьютерной Лабо- ратории в университете Кембриджа.
В 1971-1973 г. Милнер стажировался в Лаборатории искус- ственного интеллекта в Стэнфордском университете. С 1973 г. по
1995 г. он работал в отделении информатики (Computer Science
Department) Университета Эдинбурга (Шотландия), в котором в 1986 г. он совместно с коллегами основал Лабораторию ос- нов компьютерных наук (Laboratory for Foundation of Computer
Science).
320
С 1971 до 1980, в Стэнфорде и затем в Эдинбурге, он ра- ботал в области автоматизации рассуждений. Совместно с кол- легами он разработал Логику Вычислимых Функций (Logic for
Computable Functions, LCF), развивающую подход Д. Скотта к построению теоретических основ понятия вычислимости, и пред- назначенную для автоматизации формальных рассуждений. Эта работа послужила основой для прикладных систем, разработан- ных под руководством Милнера.
В 1975-1990 Милнер руководил группой, которая разрабаты- вала Standard ML – широко используемый в индустрии и обра- зовании язык программирования, семантика которого была пол- ностью формализована (ML является сокращением словосочета- ния “meta-language”). В языке Standard ML был впервые реали- зован алгоритм вывода полиморфных типов. Главное достоин- ство Standard ML – возможность оперирования с логическими доказательствами и наличие средств автоматизации построения логических доказательств.
Около 1980 г. Милнер разработал Исчисление Взаимодейству- ющих Систем (Calculus for Communicating Systems, CCS), одно из первых алгебраических исчислений для анализа параллель- ных процессов.
В конце 1980-х совместно с двумя коллегами он разработал π–
исчисление, которое является основной моделью поведения мо- бильных взаимодействующих систем.
В 1988 г. Милнер был избран членом Королевского Обще- ства. В 1991 г. ему была присуждена высшая награда в области информатики - премия имени А.М.Тьюринга.
Скачать 1.62 Mb.