Rao J.R. — Extensions of the UNITY Methodology: Compositionality, Fairness and Probability in Parallelism :: Электронная библиотека попечительского совета мехмата МГУ

Главная Ex Libris Книги Журналы Статьи Серии Каталог Wanted Загрузка ХудЛит Справка Поиск по индексам Поиск Форум

Авторизация

Поиск по указателям

Rao J.R. — Extensions of the UNITY Methodology: Compositionality, Fairness and Probability in Parallelism

Обсудите книгу на научном форуме

Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Extensions of the UNITY Methodology: Compositionality, Fairness and Probability in Parallelism

Автор: Rao J.R.

Аннотация:

This monograph extends and generalizes the UNITY methodology, introduced in the late 1980s by K. Mani Chandy and Jayadev Misra as a formalism aiding in the specification and verification of parallel programs, in several directions. This treatise further develops the ideas behind UNITY in order to explore and understand the potential and limitations of this approach: first UNITY is applied to formulate and tackle problems in parallelism such as compositionality; second, the logic and notation of UNITY is generalized in order to increase its range of applicability; finally, paradigms and abstractions useful for the design of probabilistic parallel algorithms are developed. Taken together the results presented reaffirm the promise of UNITY as a versatile medium for treating many problems of parallelism.

Язык:

Рубрика: Computer science/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Год издания: 1995

Количество страниц: 178

Добавлена в каталог: 05.12.2010

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID

Предметный указатель

"."      12
$co_{l}$       53
$co_{m}$       35 53
$dec_{ens}$       34 45
$dec_{prog}$       34 43
$dec_{safe}$       34 46
$dec_{safe}$ , intuitive significance      48
$lco_{l}$       35 53
$L_{\infty\omega}$       11
$rco_{l}$       35 53
$wdec_{ens}$       34 50
$wdec_{prog}$       34 49
$wdec_{safe}$       34 51
$\alpha$ -fairness      101
$\bar{S}$       64
$\bar{\sqcup}$       18 19 23
$\equiv$       12
$\exists$       11
$\forall$       11
$\geq$       12
$\Leftarrow$       12
$\leq$       12
$\longmapsto$       28
$\mathcal{E}$       82
$\models$       66 68
$\mu$       14 67
$\mu$ -calculus      7 63 64
$\neg$       12
$\neq$       12
$\not\equiv$       12
$\nu$       14 67
$\rightarrow$       12
$\sim\rightarrow$       82 129
$\vee$       12
$\wedge$       12
$|\Rightarrow$       103 131
:=      20
<      12
<>      12
=      12
>      12
A      65
Algorithm design      8
Always section      18
Assign section      19
Augmentation rule      31 138
Body of a guarded statement      52 59
Branching time temporal logic      63 64
Byzantine agreement problem      151
Calculational proofs      15
Closure      34 38 40
Closure ordinal      97
coin toss      99
Commutativity conditions      6
Commutativity conditions, Lipton      6 33 35 53
Commutativity conditions, Misra      6 33 35 53
Complete lattice      68
Completeness      7
Compositionality      6 8 30 33 62
Conclusion      138
Conditional multiple assignment      20
Conditional properties      138
Conflict-resolution      8 150
Conjunctive      12
CTL*      63 64
Deadlock freedom      8 153
Declare section      17
Decoupling      6 34 38 166
Deterministic      8 19 99
Deterministic correctness      100 113
Dining philosophers problem      8
Dining philosophers problem, Chandy — Misra algorithm      8 153
Dining philosophers problem, Eventually-determinizing algorithm      155
Dining philosophers problem, Lehmann — Rabin algorithm      8 152
Disable      35 52 59
Disjunctive      12
e      65
ENABLE      35 52 53 59
ensures      5 27
Ensures, conjunction      29 112
Ensures, consequence weakening      28 111
Ensures, disjunction      29 112
Ensures, E-continuity      29 112
Ensures, impossibility      28 112
Ensures, reflexivity      28 111
Entails      103 124
entails, conjunction with unless      127
entails, conjunction with upto      127
entails, consequence weakening      126
entails, corollaries about      128
entails, disjunction      128
entails, impossibility      126
entails, reflexivity      126
Euclid's Algorithm      17
Eventual determinism      8 103 149
Everywhere operator      11
execution      64 105
Execution sequence      59 64
Extreme fairness      8 101 102 125
Extremely fair      106
f      65
Fairness      5
Fairness constraint      24 64 105
Finite state      8
Fixpoint operators      67 97
Fork      152
Formal derivation      165
FullPath      66
Function application      12
G      65
Generalized weakest precondition      7 62
Generalized weakest precondition, intuitive significance      80
Goedel's incompleteness theorem      95
Greatest fixpoint      14 67
guard      52 59
Guarded statement      52 59 64
gwp      7 62
Hoare triples      4 7 63 94
Hypothesis      138
Industrial strength programs      166
Infinite computation tree      59 64
Infinitely often      115
Initial condition      26
initially section      18
Invariance      4 25
Junctivity      12
Junctivity, and-continuous      13
Junctivity, denumerably junctive      13
Junctivity, finitely junctive      13
Junctivity, monotonic      13
Junctivity, or-continuous      13
Junctivity, positively junctive      13
Junctivity, relating junctivity properties      13
Junctivity, universally junctive      13
Knaster — Tarski theorem      15 97
Law of the Excluded Miracle      14
leads-to      5 28 60 83
leads-to, cancellation      29 113
leads-to, completion theorem      29 113
leads-to, disjunction      29 112
leads-to, implication      29 112
leads-to, impossibility      29 112
leads-to, induction principle      29 113
leads-to, PSP      29 113
Least fixpoint      14 67
LED      84
Left movers      53
Locality      150
Logic variables      35 57
Loose-coupling      33 37

Maximal sequence      69
Measure      115
Message-passing      37
Methodology for proof rule design      68
Metric      29 113 134
Minimal progress      60 69 88
MODE      8 104 149
Model checking      101
Multiple assignment      5 104
Mutual exclusion      8 103 144 153 155
Ordinals      7 63 94 97
Partial correctness      4
Path quantifiers      65
PathForm      65
PCCS      102
Post's correspondence problem      95
Pred      11 12 65
Predicate transformer      7 12 13
Predicate transformer, healthiness conditions      14
Probabilistic      99
Probabilistic correctness      100 113
Probabilistic multiple assignment      102—104
Probabilistic powerdomain of evaluations      102
Probabilistic programs, $\mapsto$       111
Probabilistic programs, completeness of proof rule      139
Probabilistic programs, ensures      111
Probabilistic programs, soundness of proof rule      139
Probabilistic programs, unless      109
Probabilistic transitions      7
probabilistically leads-to      103 115 131
probabilistically leads-to, cancellation      133
probabilistically leads-to, completion theorem      134
probabilistically leads-to, general disjunction      133
probabilistically leads-to, implication      132
probabilistically leads-to, impossibility      132
probabilistically leads-to, induction principle      134
probabilistically leads-to, PSP      134
Producer-consumer      37 42
Program derivation      4
program design      62
Program state      64
Program testing      3
Program verification      4
Program verification, a posteriori      4 102
Program verification, sequential programs      4
Progress properties      5 60 100
prompts      129
prompts, cancellation      130
prompts, completion theorem      131
prompts, disjunction      130
prompts, finite disjunction      130
prompts, implication      129
prompts, impossibility      129
prompts, PSP      130
Proof format      15
Proof rule design      61
Proof rules for fairness      5 61 86
Proper set of equations      18
Propositional variables      67 97
Pure nondeterminism      71 88
Quantification, notation      11
Quantification, state space      11
Quantification, statements      23
Quantification, []      11
race conditions      38
Random walk      8 103 141
Random walk, absorbing and reflecting barrier      143
Random walk, absorbing barriers      141
Random walk, reflecting barriers      142
RANGE      11
Reactive programs      4
READ      57
Recursively enumerable      95
Reduction      33
Relative completeness      7 63 95
Relative completeness in the sense of Cook      94 96
request token      152
Restricted union rule      31 138
Right movers      53
Safety properties      5 100
Schedule      105
Second Borel — Cantelli theorem      106
Self-stabilization      8 150 161
Self-stabilization, Eventually-determinizing algorithm      162
Self-stabilization, probabilistic algorithm      162
Semantics of $\mu$ -calculus      68
Semantics of branching time temporal logic      66
Sentence of $\mu$ -calculus      68
software crisis      3
Soundness      7
sp      13
Specification refinement      4 144
Stability      25
Starvation freedom      8 155
State      104
State space      11
StatForm      65
Strong fairness      60 61 75 89
Strongest postcondition      13
Strongest solution      14 15 67
Substitution axiom      30 135
Substitution operation      12
Superposition      30 31 138
Superposition theorem      31 138
Symmetric random walk      141
Symmetry      99 149 150
Symmetry, breaking      8
Systematic design      165
Temporal logic      7
Temporal modalities      67
Temporal operators      65
Temporal structure      66
Term      11
terminating      19
Termination      4
Tightly-coupled      38
Total correctness      4
Transformational programs      4
Transparency      150
Transparent variables      18
U      65
Unconditional fairness      24 75 89 105 125
Underlying program      31 138
Underlying variables      31 138
Unified theory      165
Uniformity      150
union      30 135
Union theorem, corollaries about      137
Union theorem, ensures      31 136
Union theorem, entails      136
Union theorem, unless      31 135
Union theorem, unless and entails      137
Union theorem, upto      136
UNITY logic      5
UNITY program      115
UNITY program execution      24
UNITY program state      24
UNITY program statements      20
UNITY program, progress properties      24 27
UNITY program, safety properties      24 25
unless      5 25
unless, anti-reflexivity      26 109
unless, cancellation      26 110
unless, consequence weakening      26 109
unless, general conjunction      26 110
unless, general disjunction      26 110
unless, reflexivity      26 109
unless, simple conjunction      26 110
unless, simple disjunction      26 110
Upto      103 118

1 2

О проекте