thread-safety - エイダのタスクと安全性

Question

コーディングは好きではありませんが、Ada はとても好きで、まったくの初心者です。これらの点を明確にしていただけますか？

単一のスレッド化されていない CPU を搭載したコンピューターを使用している場合でも、タスクはシングル CPU のままです。もちろん、同じことがC または C++ でのforkにも当てはまります。

質問: このシナリオで、Ada タスクは fork よりも利点があると思いますか?

また、SPARK がタスクを禁止する理由も知りたいです (安全のためであることはわかっていますが、正確には、タスクを禁止することで安全性がどのように向上するのでしょうか)。

3 番目で最後の質問です。「安全なタスキング」(Ada で) を提供したい場合、タスク (タスク) を「安全」にするためには、タスクにどのような制限が必要になると思いますか。

ありがとうございました、

Answer 1

1) はい。最も簡単な議論は、Ada タスクが同じプロセス コンテキストで実行され、タスク/スレッドが個別のプロセスよりもいくらか高速になるということです。もう 1 つの理由は、言語レベルのタスク間通信および同期機能です。

2) SPARK の一部のバージョンのみがタスクを禁止します。RavenSPARK (2005) は、タスクを許可し、タスクについての正式な推論を許可します。タスクの問題は、特に SPARK チームの野心 (正しさの証明) に関して、正式に推論するのが難しいことです。

3) Ravenscar プロファイルに限定することを検討できます。しかし、単純な Ada タスクはすでに比較的安全です (たとえ、適切なデッドロックを作成することを妨げられなくても)。