Strong Priority and Determinacy in Timed CCS

要約

優先順位を伴うプロセス代数の古典的な理論に基づいて、同期プログラミングの本質を捉えるように設計された「逐次建設的リダクション」と呼ばれる新しいスケジューリング メカニズムを特定します。
この評価戦略の特徴的な特性は、マルチキャスト同時通信の構築による決定性を達成することです。
特に、これはプログラミング言語 Esterel の中核にあるため、不在時の反応を伴う共有メモリのマルチスレッドをモデル化することができます。
クロックと優先順位によって拡張された CCS の技術的設定では、建設的な削減のための合流特性を「構造的に一貫性がある」と呼ぶプロセスの大規模なクラスについて証明しました。
さらに、「ピボット可能」と呼ばれるいくつかの構文上の制限の下では、接頭辞、合計、並列合成、制限、および隠蔽の演算子が構造的一貫性を維持することを示します。
これは、優先順位のないミルナーの古典的な CCS 理論で合流するプロセスと比較して、厳密に大きなクラスのプロセスをカバーします。

要約(オリジナル)

Building on the classical theory of process algebra with priorities, we identify a new scheduling mechanism, called ‘sequentially constructive reduction’ which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinism-by-construction for multi-cast concurrent communication. In particular, it permits us to model shared memory multi-threading with reaction to absence as it lies at the core of the programming language Esterel. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of processes, which we call ‘structurally coherent’ the confluence property for constructive reductions. We further show that under some syntactic restrictions, called ‘pivotable’ the operators of prefix, summation, parallel composition, restriction and hiding preserve structural coherence. This covers a strictly larger class of processes compared to those that are confluent in Milner’s classical theory of CCS without priorities.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google