Ada的任务和安全

Question

我不喜欢编码，但我真的很喜欢Ada，我对它很陌生。那么你能否向我澄清这些问题？

如果您的计算机使用单个非线程CPU，任务仍然是单CPU。同样适用于C或C++的分叉。

问题：你认为Ada任务在这种情况下提供了分叉的任何好处吗？

我也想知道为什么SPARK禁止任务（我知道这是为了安全，但如何exactely，怎么能禁止任务提高了安全性。）

我的第三个和最后一个问题，如果我想提供“安全任务“（在Ada中），我可以设想对使用它们（任务）”安全“需要什么限制。

谢谢，

Answer 1

1）是的。最简单的理由是Ada任务运行在相同的进程上下文中，使得任务/线程比单独的进程稍快。语言级别的任务间通信和同步功能是另一个原因。

2）只有一些SPARK版本禁止任务。 RavenSPARK（2005）允许任务分配，并允许对任务进行正式的推理。任务的问题在于，很难正式推理，尤其是SPARK团队的野心（证明正确性）。

3）您可以考虑限制自己的Ravenscar配置文件。但简单的Ada任务已经相对安全了（即使它不能阻止你编写好的死锁）。