Ada的任務和安全

Question

我不喜歡編碼，但我真的很喜歡Ada，我對它很陌生。那麼你能否向我澄清這些問題？

如果您的計算機使用單個非線程CPU，任務仍然是單CPU。同樣適用於C或C++的分叉。

問題：你認爲Ada任務在這種情況下提供了分叉的任何好處嗎？

我也想知道爲什麼SPARK禁止任務（我知道這是爲了安全，但如何exactely，怎麼能禁止任務提高了安全性。）

我的第三個和最後一個問題，如果我想提供「安全任務「（在Ada中），我可以設想對使用它們（任務）」安全「需要什麼限制。

謝謝，

Answer 1

1）是的。最簡單的理由是Ada任務運行在相同的進程上下文中，使得任務/線程比單獨的進程稍快。語言級別的任務間通信和同步功能是另一個原因。

2）只有一些SPARK版本禁止任務。 RavenSPARK（2005）允許任務分配，並允許對任務進行正式的推理。任務的問題在於，很難正式推理，尤其是SPARK團隊的野心（證明正確性）。

3）您可以考慮限制自己的Ravenscar配置文件。但簡單的Ada任務已經相對安全了（即使它不能阻止你編寫好的死鎖）。