安全性と活性特性

コンピュータプログラムの実行の特性、特に並行システムや分散システムにおける特性は、安全性（「悪いことは起こらない」）と活性性（「良いことが起こる」）を与えることによって長い間定式化されてきました。^[1]

を満たす状態で開始された実行がを満たす状態で終了する場合、プログラムは前提条件と事後条件に関して完全に正しい。完全な正しさは安全性と活性性の結合である: ^[2] ${\displaystyle P}$ ${\displaystyle Q}$${\displaystyle P}$${\displaystyle Q}$

• 安全性プロパティは、 を満たす状態で開始し、 を満たさない最終状態で終了する実行などの「悪いもの」を禁止します。プログラムの場合、この安全性プロパティは通常、 Hoare トリプルを使用して記述されます。${\displaystyle P}$${\displaystyle Q}$${\displaystyle C}$ ${\displaystyle \{P\}C\{Q\}}$
• 活性特性、つまり「良いこと」は、条件を満たす状態で開始された実行が終了することです。${\displaystyle P}$

悪いことは実行中に特定の場所で起こるため、 ^[3]離散的であることに注意してください。「良いこと」は離散的である必要はありませんが、終了の活性特性は離散的です。

^{最終的に安全性プロパティ[4]}と活性プロパティ^[5]に対して提案された正式な定義は、この分解が直感的に魅力的であるだけでなく完全であることも実証しました。実行のすべてのプロパティは、安全性プロパティと活性プロパティの結合です。^[5]さらに、分解を行うことは、正式な定義により、安全性プロパティの検証と活性プロパティの検証には異なる方法を使用する必要があることを証明できるため、役立ちます。^{[6] [7]}

安全特性は、実行中に個別の悪いことが起こることを禁止します。 ^[1] 安全特性は、何が禁止されているかを述べることによって、何が許可されるかを特徴付けます。悪いことが個別であるという要件は、実行中に起こる悪いことが必ず何らかの識別可能な時点で起こることを意味します。^[5]

安全性を定義するために使用できる個別の悪いものの例としては、次のものがある: ^[5]

• 特定の前提条件を満たす状態で開始された実行は終了しますが、最終状態は必要な事後条件を満たしません。
• 2 つの同時プロセスの実行。両方のプロセスのプログラム カウンターがクリティカル セクション内のステートメントを指定します。
• 2 つのプロセスが同時に実行され、各プロセスが別のプロセスの状態が変化するのを待機する状態 (デッドロックと呼ばれます)。

プログラムの実行は、実行の進行に伴って生じるプログラム状態の無限シーケンスを与えることによって形式的に記述することができる。この場合、終了プログラムの最後の状態は無限に繰り返される。対象のプログラムについて、可能なプログラム状態の集合を 、プログラム状態の有限シーケンスの集合を 、プログラム状態の無限シーケンスの集合を とするとする。シーケンスと の関係は、がの接頭辞であるか に等しい場合に限り成立する。^[5]${\displaystyle S}$${\displaystyle S^{*}}$${\displaystyle S^{\omega}}$${\displaystyle \sigma \leq \tau}$${\displaystyle \sigma}$${\displaystyle \tau}$${\displaystyle \sigma}$${\displaystyle \tau}$${\displaystyle \sigma}$${\displaystyle \tau}$

プログラムのプロパティは、許可される実行のセットです。

安全性プロパティの本質的な特性は次の通りです。何らかの実行がを満たさない場合、 その安全性プロパティの定義上の悪いことがのいずれかの時点で発生します。このような悪いことの後に、さらに実行を実行して が実行される場合 、の悪いことがにも発生するため、も を満たさないことに注意してください。悪いことの修復不可能性に関するこの推論を、が安全性プロパティであるための定義上の特性とします。これを述語論理で形式化すると、安全性プロパティの正式な定義が得られます。^[5]${\displaystyle SP}$${\displaystyle \sigma}$${\displaystyle SP}$${\displaystyle \sigma}$${\displaystyle \sigma ^{\prime}}$${\displaystyle \sigma ^{\prime}}$${\displaystyle SP}$${\displaystyle \sigma}$${\displaystyle \sigma ^{\prime}}$${\displaystyle SP}$${\displaystyle SP}$

${\displaystyle \forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))}$

安全性プロパティのこの正式な定義は、実行が 安全性プロパティを満たす場合、 のすべてのプレフィックス(最後の状態が繰り返される) も を満たすことを意味します。 ${\displaystyle \sigma}$${\displaystyle SP}$${\displaystyle \sigma}$${\displaystyle SP}$

活性特性は、すべての実行に対して良いことを規定するか、または同等に、実行中に必ず起こることを説明します。^[1]良いことは離散的である必要はなく、無限の数のステップを含む可能性があります。活性特性を定義するために使用される良いことの例は次のとおりです。 ^[5]

• 適切な状態で開始された実行の終了。
• 適切な状態で開始された実行が終了しない。
• エントリが試行されるたびに、クリティカル セクションへの最終的なエントリが保証されます。
• 競合がある場合でもリソースに公平にアクセスできます。

最初の例の良い点は離散的ですが、他の例ではそうではありませ ん。

指定されたリアルタイム境界内で回答を生成することは、活性特性ではなく安全性特性です。これは、離散的な悪影響が禁止されているためです。つまり、回答がまだ生成されておらず、クロックの値 (状態変数) が境界に違反する状態に達する部分的な実行です。デッドロックの自由は安全性特性です。「悪影響」とはデッドロック(離散的) です。

ほとんどの場合、プログラムが最終的に何らかの「良いこと」を行うことを知るだけでは十分ではありません。プログラムが一定のステップ数以内、または期限までに「良いこと」を実行することを知りたいのです。「良いこと」に特定の制限を与えるプロパティは安全性プロパティ (前述のとおり) ですが、制限が存在することを単に主張する弱いプロパティは活性プロパティです。このような活性プロパティを証明することは、より厳密な安全性プロパティを証明することよりも簡単である可能性が高いです。なぜなら、活性プロパティを証明するには、安全性プロパティを証明するために必要な種類の詳細な説明が必要ないからです。

安全性プロパティと異なり、活性プロパティは実行の有限プレフィックス ^[8]を排除できません (そのようなことは「悪いこと」であり、安全性プロパティを定義することになるため)。これにより、活性プロパティは有限プレフィックスを排除しないプロパティとして定義されます。^[5]${\displaystyle LP}$${\displaystyle \alpha \in S^{*}}$${\displaystyle \alpha}$${\displaystyle LP}$

${\displaystyle \forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \in LP)}$

この定義は、良いものが離散的であることに 限定されません。良いものはのすべてを含む可能性があり、これは無限長の実行です。 ${\displaystyle \tau}$

ランポートは、マルチプロセス（並行）プログラムの正しさを証明する 1977年の論文^[1]で、安全性特性と活性特性という用語を使用しました。彼はこれらの用語をペトリネット理論から借用しました。ペトリネット理論では、ペトリネットの「トークン」をその「場所」に割り当てる方法を説明するために、活性と有界性という用語を使用していました 。ペトリネットの安全性は、有界性の特定の形式でした。ランポートはその後、ミュンヘンでの分散システムに関するNATOの短期コースで安全性の正式な定義を開発しました^{[9] 。この定義では、特性は}スタッター に対して不変であると想定されていました。上記の安全性の正式な定義は、アルパーンとシュナイダーの論文に記載されています^[5] 。安全性特性の2つの形式化の関係は、アルパーン、デマーズ、シュナイダーの論文に記載されています^{[10] 。}

Alpern と Schneider ^[5]は、活性の正式な定義を示し、すべてのプロパティは安全性プロパティと活性プロパティを使用して構築できることの証明を伴っています。その証明は、安全性プロパティは閉集合に対応し、活性プロパティはプログラム状態の無限シーケンスの集合上の自然な位相における稠密集合に対応するという Gordon Plotkin の洞察に触発されました。^[11]その後、Alpern と Schneider ^{[12]は、安全性プロパティと活性プロパティの正式な定義に}Büchi オートマトンの特徴付けを与えただけでなく、これらのオートマトン定式化を使用して、安全性プロパティの検証には不変量が必要であり、活性プロパティの検証には根拠の整った議論が必要であることを示しました。プロパティの種類 (安全性 vs 活性) と証明の種類 (不変量 vs 根拠の整った議論) との対応は、プロパティを安全性と活性に分解すること (他の分割ではなく) が有用であるという強力な議論でした。つまり、証明するプロパティの種類がわかれば、必要な証明の種類が決まるのです。 ${\displaystyle S^{\omega}}$