翻訳: The PlusCal Algorithm Language

Abstract

Table of Contents

1. Abstract
2. 1 Introduction
3. 2 Some Examples
   1. 2.1 Euclid's Algorithm
   2. 2.2 The Quicksort Partition Operation
   3. 2.3 The Fast Mutual Exclusion Algorithm
   4. 2.4 The Alternating Bit Protocol
4. 3 完全な言語
5. 4 The TLA⁺ Translation
   1. 4.1 An Example
   2. 4.2 Translation as Semantics
   3. 4.3 Liveness
6. 5 Labeling Constraints
7. 6 Conclusion
8. References
9. Appendix: The C-Syntax Grammar
10. 翻訳抄

1 Introduction

2 Some Examples

2.1 Euclid's Algorithm

2.2 The Quicksort Partition Operation

2.3 The Fast Mutual Exclusion Algorithm

2.4 The Alternating Bit Protocol

3 完全な言語

ここまでで PlusCal 言語の構成要素をほぼすべて見てきた。主な省略事項は次のとおりである (p-syntax で書かれている)。

• TLA⁺ にはレコードの表記法がある。レコードは文字列の有限集合を定義域とする関数で \(a.b\) は \(a["b"]\) の糖衣構文である。PlusCal では \[ v.a := 0; A[0].b := 42; \] のようにレコードのフィールドへの通常の割当が可能である。TLC は \(v\) が構成要素 \(a\) を持たなかったり \(A\) の \(A[0]\) が構成要素 \(b\) を持つレコードの配列ではない場合、このコードを実行しようとするとエラーを報告する。これは通常 \(v\) と \(A\) を正しい "型" の値に初期化しなければならないことを意味する。
• if 文には省略可能な elsif 節 (p-syntax のみ) があり、その後に省略可能な else 節が続く。
• PlusCal にはプロシジャ宣言があり call 文と return 文を持つ。call が文であることからプロシジャは値を返さない。プロシジャの呼び出しを式の評価の一部とする慣例的なアプローチではステップの記述が問題となり、返値を認めること翻訳を複雑にする。プロシジャはグローバル変数 (マルチプロセスアルゴリズムの場合はプロセスローカル変数) を設定することで簡単に値を返すことができる。
• PlusCal には TLA⁺ 定義に挿入するためのオプションである define 文がある。define 文はアルゴリズムのグローバル変数宣言の直後に配置され、これらの変数で定義された演算子をアルゴリズムの式で使用することができるようになる。

言語の詳細はラベルが禁止される場合と必要な場合が説明されるセクション 5 で完結する。

4 The TLA⁺ Translation

4.1 An Example

4.2 Translation as Semantics

4.3 Liveness

アルゴリズムのコードは実行可能なステップを記述するものである; 実行するステップを要求するものではない。言い換えれば、コードはアルゴリズムの safety 特性を記述する。最終的に何かが起きることを保証する liveness 特性を推論するには、いつステップが実行されなければならないかを保証する liveness 仮定を追加しなければならない。これらの仮定はアクションに関する公平性仮定 (fairness assumptions) [2] と記述される。公平性仮定の 2 つの一般的なタイプは弱い公平性と強い公平性である。アクション \(A\) の弱い公平性は \(A\) が継続的に有効化されている場合に \(A\) のステップが実行されなければならないことを保証する。強い公平性は \(A\) が繰り返し無効化されても有効化され続けていれば \(A\) のステップが実行されなけれなければならないことを保証する。

ほとんどの逐次 (単一プロセス) アルゴリズムにおいて唯一の liveness 要件は終了 (termination) である。これは、アルゴリズムが可能な限りステップを実行し続けるという仮定のもとで満たされなければならない。つまり、次の状態のアクション全体の弱い公平性の仮定のもとを意味する。(アクションを無効化する他のプロセスが存在しないため、逐次アルゴリズムにおいて弱い公平性は強い公平性と等価である) PlusCal トランスレータは適切な TLA⁺ 翻訳と TLC 構成ファイルを作成することで終了をチェックすることを指示することができる。

マルチプロセスアルゴリズムの場合、liveness 要件には無限の種類がある。終了以外の要件は、ユーザが TLA⁺ モジュールで時相理論式として定義し、TLC 構成ファイルを修正してその要件を満たすかどうかを TLC がチェックするように指示しなければならない。最も一般的な 3 つの公平性仮定は、各プロセスの次の状態アクションの弱い公平性および強い公平性と、次の状態アクション全体の弱い公平性である。後者は、もしどのプロセスもステップを実行できるのであればアルゴリズムは停止しないことを意味しているが、個々のプロセスは飢餓状態になる可能性がある。PlusCal トランスレータはアルゴリズムの TLA⁺ 翻訳にこれら 3 つの公平性仮定の一つを追加するよう指示することができる。しかし、アルゴリズムには他にも様々な衡平性過程が存在する。それらはユーザが時相理論式として記述する必要がある。

例としてセクション 2.4 の ABProtocol アルゴリズムに戻ってみよう。要求される可能性のある liveness 特性は、選択されたすべてのメッセージが最終的に配信されることである。safety 特性は不正なメッセージが配信されないことを意味するため、十分なメッセージが配信されていることをチェックすれば良い。これは以下の時相理論式で表現され、任意の \(i\) に対してもし \({\it input}\) が \(i\) 個の要素を含むことがあれば \({\it output}\) は最終的に \(i\) 個の要素を含むことを保証している: \[ \forall i \in {\it Nat}: ({\it Len}({\it input}) = i) ⤳ ({\it Len}({\it output}) = i) \] このアルゴリズムは以下の操作の強い公平性の仮定のもとでこの特性を満たしている:

• メッセージを送ることのできる、送信者の第一 or 節
• 確認応答を受信することのできる、送信者の第二 or 節
• 確認応答を送信することのできる、受信者の either 節
• メッセージを受信することのできる、受信者の or 節

翻訳結果は式 Sender を送信者の次の状態アクションとして定義する。これは either / or 文の 3 つの節を記述する 3 つの式の論理和である。最初の or 節は msgC を変更できる唯一の節であるためその節を記述するアクションは \({\it Sender} \land ({\it msgC}' \ne {\it msgC})\) である。同様に送信者の最後の or 節はアクション \({\it Sender} \land ({\it ackC}' \ne {\it ackC})\) で記述される。関連する受信者のアクションも同様に定義される。これら 4 つの強い公平性条件を備えたアルゴリズムの完全な TLA⁺ 仕様は次の式となる: \[ \begin{array}{l} \land {\it Spec} \\ \land SF_{\it vars}({\it Sender} \land ({\it ackC}' \ne {\it ackC})) \\ \land SF_{\it vars}({\it Sender} \land ({\it msgC}' \ne {\it msgC})) \\ \land SF_{\it vars}({\it Receiver} \land ({\it ackC}' \ne {\it ackC})) \\ \land SF_{\it vars}({\it Receiver} \land ({\it msgC}' \ne {\it msgC})) \end{array} \] この仕様では送信者が送信するメッセージを選択する操作や LoseMsg プロセスがメッセージを削除する操作について公平性を仮定していない。これらの操作は決して実行される必要がない。

liveness 特性 \(\forall i \in {\it Nat}...\) をチェックするためには TLC に \({\it Nat}\) の代わりに有限集合を代入するよう指示する必要がある。セクション 2.4 で説明した制約条件では \({\it Nat}\) の代わりに \(0..4\) を代入すれば十分である。そして TLC はアルゴリズムが liveness 特性を満たすかどうかを確認するのに約 3.5 分かかり、これは safety をチェックするのにかかった 7.5 秒の約 30 倍である。この 30 という比率はこのような小さな例としては異例の大きさである; これはチェックされる liveness 特性が本質的に、\(i\) の値ごとに 1 つずつ別々にチェックされる 5 つの式の論理和であるためである。\(i\) の値が 1 つであれば liveness と safety のチェックの比率は Fast Mutual Exclusion Algorithm の場合と同じで 5 倍程度となる。

公平性は繊細である。多くの読者はなぜこの 4 つの公平性仮定がすべてのメッセージの受信を保証するのに十分であるか、あるいは送信者と受信者の完全な次の状態アクションの強い公平性がそうでないのか、理解できないかもしれない。liveness 特性を機械的にチェックする機能は非常に有用である。残念なことに、liveness をチェックすることは safety をチェックすることより本質的に遅く、アルゴリズムの大規模なインスタンスでは実行することができない。幸いなことに、liveness エラーは safety エラーよりも機微な傾向があり、通常はかなり小さなインスタンスで補足することができる。

5 Labeling Constraints

6 Conclusion

References

2. [1] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.
3. [2] Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, New York, Berlin, Heidelberg, Tokyo, 1986.
4. [3] Yuri Gurevich. Can abstract state machines be useful in language theory? Theoretical Computer Science, 376(1–2):17–29, 2007.
5. [4] C. A. R. Hoare. Algorithm 64: Quicksort. Communications of the ACM, 4(7):321, July 1961.
6. [5] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, August 1978.
7. [6] Gerard J. Holzmann. The Spin Model Checker. Addison-Wesley, Boston, 2004.
8. [7] Daniel Jackson. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology, 11(2):256–290, April 2002.
9. [8] Leslie Lamport. The pluscal algorithm language. URL http://research.microsoft.com/users/lamport/tla/pluscal.html. The page can also be found by searching the Web for the 25-letter string obtained by removing the “-” from uid-lamportpluscalhomepage.
10. [9] Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 657–668, Paris, September 1983. IFIP, North-Holland.
11. [10] Leslie Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1–11, February 1987.
12. [11] Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
13. [12] Leslie Lamport. Specifying Systems. Addison-Wesley, Boston, 2003. Also available on the Web via a link at http://lamport.org.
14. [13] Leslie Lamport. Checking a multithreaded algorithm with ⁺cal. In Shlomi Dolev, editor, Distributed Computing: 20th International Conference, DISC 2006, volume 4167 of Lecture Notes in Computer Science, pages 151–163, Berlin, Heidelberg, 2006. Springer-Verlag.
15. [14] Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann, San Mateo, California, 1995.
16. [15] K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.
17. [16] Vaughan R. Pratt. Semantical considerations on Floyd-Hoare logic. In 17th Symposium on Foundations of Computer Science, pages 109–121. IEEE, October 1976.
18. [17] J. T. Schwartz, R. B. Dewar, E. Schonberg, and E. Dubinsky. Programming with sets: An Introduction to SETL. Springer-Verlag, New York, 1986.
19. [18] Robert Sedgewick. Algorithms. Addison-Wesley, 1988.
20. [19] Niklaus Wirth. Algorithms + Data Structures = Programs. PrenticeHall, 1975.
21. [20] Yuan Yu, Panagiotis Manolios, and Leslie Lamport. Model checking TLA⁺ specifications. In Laurence Pierre and Thomas Kropf, editors,

Appendix: The C-Syntax Grammar

翻訳抄

1. The PlusCal Algorithm Language