PlusCal
Direct Edit
\( \def\ldef{≜} \) \( \def\globally{□} \) \( \def\eventually{◇} \) \( \def\openleftarrowplus{\overset{+}{⇾}} \) \( \def\equalv{⫤} \)

翻訳: A PlusCal User's Manual

Takami Torao 2020年の論文 #PlusCal #TLA+
  • このエントリーをはてなブックマークに追加
P-Syntax* Version 1.8
Leslie Lamport
15 December 2020
  • *このマニュアルには C-Syntax 版もある。２つの構文の詳細については 3 ページ参照。

Table of Contents

  1. Preface
  2. The Two Syntaxes
  3. 1 Introduction
  4. 2 Getting Started
    1. 2.1 Typing the Algorithm
    2. 2.2 The TLA+ Module
    3. 2.3 Translating and Executing the Algorithm
    4. 2.4 Checking the Results
    5. 2.5 停止の確認
    6. 2.6 A Multiprocess Algorithm
    7. 2.7 Where Labels Must and Can't Go
  5. 3 The Language
    1. 3.1 Expressions
    2. 3.2 The Statements
      1. 3.2.1 Assignment
      2. 3.2.2 If
      3. 3.2.3 Either
      4. 3.2.4 While
      5. 3.2.5 Await (When)
      6. 3.2.6 With
      7. 3.2.7 Skip
      8. 3.2.8 Print
      9. 3.2.9 Assert
      10. 3.2.10 Call and Return
      11. 3.2.11 Goto
    3. 3.3 Processes
    4. 3.4 Procedures
    5. 3.5 Macros
    6. 3.6 Definitions
    7. 3.7 Labels
    8. 3.8 The Translation's Definitions and Declarations
  6. 4 Checking and Algorithm
    1. 4.1 Running the Translator
    2. 4.2 Specifying the Constants
    3. 4.3 Constants
    4. 4.4 Understanding TLC's Output
    5. 4.5 不変性チェック
    6. 4.6 終了, Liveness, 公平性
    7. 4.7 Additional TLC Features
      1. 4.7.1 Deadlock Checking
      2. 4.7.2 Multithreading
      3. 4.7.3 Symmetry
  7. 5 TLA+ Expressions and Definitions
    1. 5.1 Numbers
    2. 5.2 Strings
    3. 5.3 Boolean Operators
    4. 5.4 Sets
    5. 5.5 Functions
    6. 5.6 Records
    7. 5.7 The Except Construct
    8. 5.8 Tuples and Sequences
    9. 5.9 Miscellaneous Constructs
    10. 5.10 Temporal Operators
      1. 5.10.1 Fairness
      2. 5.10.2 Liveness
      3. 5.10.3 One Algorithm Implementing Another
  8. References
  9. A The Grammar
  10. B The TLA+ Translation
  11. C Translator Options
  12. Useful Tables
  13. Index
  14. 翻訳抄

Preface

The Two Syntaxes

1 Introduction

2 Getting Started

2.1 Typing the Algorithm

2.2 The TLA+ Module

2.3 Translating and Executing the Algorithm

2.4 Checking the Results

2.5 停止の確認

アルゴリズム EuclidAlg が常に停止 (終了) することを確認するには -termination オプションを付けて変換を実行する。またはファイルのコメントまたはモジュールの前後に

PlusCal options (-termination)

の行を配置することでも行える (options ステートメントに入れるときはオプション名から "-" を省略できる)。これにより停止を保証する適切な変換が生成される。次に新しいモデルを生成すると Model Overview ページの What to check? セクションの Properties 部分に Termination が追加されるだろう。これにより TLC は取りうるすべての実行が停止することを確認する (Termination プロパティはすべての PlusCal アルゴリズムのツールボックスに含まれているが、そのボックスはモデル作成時にルートモジュールに Termination プロパティが指定されている場合にのみ確認される)。

TLC が非停止実行 (non-terminating execution) を検出すると、プロパティ Termination に違反していることを示すエラーメッセージが生成され、ツールボックスのエラートレースウィンドウに非停止のトレースが表示される。36 ページのセクション 4.4 ではこのトレースの解釈方法について説明している。

2.6 A Multiprocess Algorithm

1. \( ncs: noncritical \ section; \)
2. \( start: \)
3. \( \hspace{12pt}\langle b[i] := true \rangle; \)
4. \( \hspace{12pt}\langle x := i \rangle; \)
5. \( \hspace{12pt}{\bf if} \ \langle y \ne 0 \rangle \ {\bf then} \ \langle b[i] := false \rangle; \)
6. \( \hspace{24pt}{\bf await} \ \langle y = 0 \rangle; \)
7. \( \hspace{24pt}{\bf goto} \ start \ {\bf fi}; \)
8. \( \hspace{12pt}\langle y := i \rangle \)
9. \( \hspace{12pt}{\bf if} \ \langle x \ne i \rangle \ {\bf then} \ \langle b[i] := false \rangle; \)
10. \( \hspace{24pt}{\bf for} \ j := 1 {\bf to} N \ {\bf do \ await} \ \langle \lnot b[j] \rangle \ {\bf od}; \)
11. \( \hspace{24pt}{\bf if} \ \langle y \ne i \rangle \ {\bf then \ await} \ \langle y = 0 \rangle; \)
12. \( \hspace{36pt}{\bf goto} \ start \ {\bf fi \ fi}; \)
13. \( \hspace{12pt}critical \ section; \)
14. \( \hspace{12pt}\langle y := 0 \rangle; \)
15. \( \hspace{12pt}\langle b[i] := false \rangle; \)
16. \( \hspace{12pt}{\bf goto} \ ncs \)
Figure 1: もとの説明に基づく高速相互排除アルゴリズムのプロセス \(i\)。

2.7 Where Labels Must and Can't Go

3 The Language

3.1 Expressions

3.2 The Statements

3.2.1 Assignment

3.2.2 If

3.2.3 Either

3.2.4 While

3.2.5 Await (When)

3.2.6 With

3.2.7 Skip

3.2.8 Print

3.2.9 Assert

3.2.10 Call and Return

3.2.11 Goto

3.3 Processes

3.4 Procedures

3.5 Macros

3.6 Definitions

3.7 Labels

3.8 The Translation's Definitions and Declarations

4 Checking and Algorithm

4.1 Running the Translator

4.2 Specifying the Constants

4.3 Constants

4.4 Understanding TLC's Output

4.5 不変性チェック

セクション 2 の例では TLC を使って数式の不変性をチェックする方法 - つまりアルゴリズムが到達可能なすべての状態で式が true となることを説明している。不変性の重要な例は型の正確さである。通常の型付きプログラミング言語では型の正確さは構文上の条件である。PlusCal は型がないため、型の正確さはアルゴリズムの特性であり、各変数の値が適切な集合の要素であることをアサートする。例えば我々は p の値が常に素数である場合に限り、つまり次の式が不変である場合に限り変数 p が素数型を持つという。ここで \({\it Nat}\) は自然数の集合である。\[ p \in \{i \in {\it Nat}:\forall j \in 2..(i-1): i\ \%\ j \ne 0\} \] (もしいまこの不変性を理解していなくても、セクション 5 を読めば理解できるはずである) TLC はこの式が不変性かどうかを調べることができる。通常のプログラミングの型チェックと同様に、型の正しさをチェックすることは PlusCal アルゴリズムの単純なエラーを発見するのに良い方法である。

アルゴリズムが型と一致しているためには、その変数の初期値が正しい "型" である必要がある。変数に初期値が設定されていない場合、そのデフォルトの初期値は defaultInitValue という名の不定型の定数である。デフォルトでツールボックスのモデルはこれをモデル値として設定する (35 ページ参照)。defaultInitValue が不定型であるため、これは変数に対する型一致値ではない。したがってアルゴリズムは変数が正しく初期化されないと型が正しくないことになる。型をチェックしたくなる変数の中にはプロシジャパラメータがある。アルゴリズムでは以下の例のようにプロシジャの形式パラメータに初期値を割り当てることができる:

procedure Foo (p1 = 0, p2 = {"a", "b"})

プロシジャ変数の宣言と同様に、形式パラメータ \(p\) の初期値宣言は \(p={\it expression}\) でなければならない。

プロシジャの形式パラメータはプロシジャが呼び出されたときに対応する引数と同じ値に設定されるため、その初期値は実行には影響を与えない。これらの初期値は TLA+ 仕様の対応する変数が常に正しい型の値を持つことを保証するためだけに使用される。

4.6 終了, Liveness, 公平性

セクション 2.5 では単一プロセスアルゴリズムの終了をチェックする方法を紹介した。終了は liveness 特性と呼ばれる一般的な特性の特殊ケースであり、最終的に何かが起こることを保証している。我々は TLC を使ってより一般的にアルゴリズムの liveness 特性をチェックすることができる。

アルゴリズムはいくつかの仮定 - 通常はアクションの公平性仮定 (fairness assumptions of action) - のもとでのみ liveness 特性を満たす。PlusCal アルゴリズムではラベルごとに対応するアクションが存在する。そのアクションの実行とは、そのラベルから次のラベルまでのすべてのコードの実行で構成される。アクションは実行可能である場合にのみ有効化 (enabled) される。プロセス内の以下のコードについて考える:

a: y := 42;
   z := y + 1;
b: await x > self;
   x := x-1;
c: ...

アクション \(a\) の実行は \(y\) と \(z\) への割り当てを実行することで構成されている。このアクションはプロセスの制御が \(a\) にある場合にのみ有効化される。アクション \(b\) の実行は \(x\) を 1 ずつ減少させる。これは制御が \(b\) にあり \(x\) の値がプロセスの識別子 \({\it self}\) より大きい場合にのみ有効化される。

制御がそのラベルにある場合にのみ有効化される \(a\) のようなアクションはノンブロッキングと呼ばれる。ノンブロッキングではない \(b\) のようなアクションはブロッキングと呼ばれる。

ノンブロッキングアクションに対する公平性は、プロセスがそのアクションで停止できないことを意味している。したがって \(a\) での公平性とは、プロセスの制御が \(a\) にあるときにプロセスは最終的にアクション \(a\) を実行しなければならないことを意味している。

ブロッキングアクションに対する公平性の条件には 2 種類がある。アクション \(\alpha\) の弱い公平性 (weak fairness) は、\(\alpha\) が永遠に有効化されているなら \(\alpha\) を停止できないことを意味している。例えばアクション \(b\) が弱い公平性であるとは、プロセスが \(b\) にある間 \(x \gt {\it self}\) が true のままである場合、アクション \(b\) が最終的に実行されることを意味している。\(\alpha\) の強い公平性 (strong fairness) とは、\(\alpha\) が永遠に true のままであればプロセスは \(\alpha\) で停止できないことに加えて、\(\alpha\) が無効化され続けその後に有効化されても停止できないことを意味する。例えばアクション \(b\) の強い公平性は、\(x \gt {\it self}\) が true になり続ける限り、たとえ false になり続けたとしてもプロセス \({\it self}\) は \(b\) で停止できないことを意味する。

ノンブロッキングアクションの場合、弱い公平性と強い公平性は同等であるため公平性は 1 種類しかない。

ただの process ではなく fair process と書くことで、そのプロセスのすべてのアクションがデフォルトで弱い公平性であることを保証する。プロセスのアクションのデフォルトの公平性条件は、ラベルの後に + または - を追加することで変更できる。a:+ と書くことでアクション \(a\) が強い公平性であることを保証する。a:- と書くことで \(a\) が公平性条件を満たさないことを保証する。

fair+ process とプロセスを書くことで、そのプロセスのすべてのアクションがデフォルトで強い公平性であることを保証する。プロセスのラベルの後に - を追加することでアクションが公平性条件を満たさないことを保証する。fair+ プロセスでラベルの後に + を付けても効果はない。

fair または fair+ ではないプロセスは不公平プロセス (unfair process) と呼ばれ、そのアクションではなんの公平性仮定も持たない。そのようなプロセスのラベルの後に + や - を付けても効果はない。

以下の翻訳オプションは公平性の仮定に影響する。

-wf
任意の不公平プロセス (前に fair または fair+ が付かないもの) を fair プロセスとする。
-sf
任意の不公平プロセス (前に fair または fair+ が付かないもの) を fair+ プロセスとする。
-nof
すべてのプロセスを不公平プロセスとする。

アルゴリズムの個々のアクションの公平性に加えてアルゴリズム全体の公平性も存在する。この特性はプロセスが少なくとも 1 つの有効化されたアクションを持つならアルゴリズムは停止できないことを保証する。この特性はアルゴリズムを --fair algorithm で開始するか、または -wfNext 翻訳オプションによって保証される。

単一プロセスまたは逐次アルゴリズムの場合、--fair algorithm で開始したり -wfNext, -wf または -sf オプションを使用することは同等である (他のプロセスがなければ、有効化されていないアクション \(\alpha\) に制御がある場合、\(\alpha\) が有効化されることはない)。逐次アルゴリズムの弱い公平性はアルゴリズムの本体を開始する { の前に fair (または fair+) を書くkとによって指定することもできる。ラベルの後に + や - を付けても逐次アルゴリズムでは効果がない。

11 ページのセクション 2.5 で論議した -termination オプションは、上述の公平性オプションがどれも指定されていない場合、事実上 -wf を追加することになる。

アルゴリズムが満たすべき liveness プロパティは、公平性と liveness を表すために使われる TLA+ 時相演算子を使った時相式として記述することができる。これについては 51 ページのセクション 5.10 で詳述する。時相特性は繊細で理解が難しいかもしれない。TLA+ 本のチャプター 8 はこれらの特性をより詳しく説明している。ここでは、非常に便利なある一つの演算子 \(⤳\), タイプは ~>、発音 Leads to についてのみ説明する。

式 \(P ⤳ Q\) は、もし \(P\) が true となることがあれば \(Q\) はその時に true であるか、または後に true となることを保証する。例としてページ 13 の Figure 2 のアルゴリズム FastMutex を考えてみよう。プロセスが公平であると仮定して process の前にキーワード fair を追加する。我々はプロセスが非クリティカルセクションの中に永遠にとどまることを許している。そのためラベル ncs: と cs: の後に - を追加する。

このアルゴリズムが満たしている liveness 条件とは、あるプロセスがそのクリティカルセクションに入ろうとしているとき、あるプロセス (必ずしも同じプロセスではない) がそのクリティカルセクションに入っているか、または最終的に入るというものである。\({\it pc}[i]\) が集合 \(\{{\tt "start"},{\tt "l1"},\ldots,{\tt "l10"}\}\) の中にある場合、プロセス \(i\) はそのクリティカルセクションに入ろうとしている。\({\it pc}[i]\) が集合 \(\{{\tt "ncs"},{\tt "cs"},{\tt "l11"},{\tt "l12"}\}\) に入っていないとき、と表現するほうがわかりやすいかもしれない。それで、我々がチェックしたい特性は、この条件があるプロセスをそのクリティカルセクションに導くことである。この特性は \[ (\exists i \in 1 .. N : {\it pc}[i] \not\in \{{\tt "ncs"}, {\tt "cs"}, {\tt "l11"}, {\tt "l12"}\}) \\ ⤳ (\exists i \in 1 .. N : {\it pc}[i] = {\tt "cs"}) \] と書く。TLC は 3 つのプロセス (\(N=3\)) に対するこの特性を約 1 分でチェックすることができる。

ここで説明した言語構造と変換オプションにより、必要と考えられるアルゴリズムの公平性に関する仮定を全て表現することができるようになる。もしも他の種類の公平性仮定が必要となった場合は 51 ページのセクション 5.10 で説明している TLA+ 時相演算子を使用して自分で書くことができる。

liveness チェック (終了を含む) は不変性チェックよりも遅く、TLC は不変性チェックのような大きなモデルで liveness をチェックすることができない。

4.7 Additional TLC Features

4.7.1 Deadlock Checking

4.7.2 Multithreading

4.7.3 Symmetry

5 TLA+ Expressions and Definitions

5.1 Numbers

5.2 Strings

5.3 Boolean Operators

5.4 Sets

5.5 Functions

5.6 Records

5.7 The Except Construct

5.8 Tuples and Sequences

5.9 Miscellaneous Constructs

5.10 Temporal Operators

5.10.1 Fairness

5.10.2 Liveness

5.10.3 One Algorithm Implementing Another

References

A The Grammar

B The TLA+ Translation

C Translator Options

Useful Tables

Index

(省略)

翻訳抄

  1. A PlusCal User's Manual
↑ページの先頭