Ада Tasking и Безопасность

Question

Я не люблю кодирование, но мне очень понравилась Ада, и я очень новичок в этом. Не могли бы вы разъяснить мне эти моменты?

Если у вас есть компьютер с одним непотоковым процессором, задача по- прежнему будет однопроцессорной. То же самое относится и к разветвлению в C или C++.

Вопрос: Как вы думаете, Ada Tasking дает какие-то преимущества по сравнению с разветвлением в этом сценарии?

Я также хочу знать, почему SPARK запрещает выполнение задач (я знаю, что это для безопасности, но насколько точно, как запрет задач может повысить безопасность).

Мой третий и последний вопрос: если я хочу предоставить "безопасное выполнение задач" (в Ada), какие ограничения для задач я мог бы представить, чтобы сделать использование (задач) "Безопасным".

Спасибо,

Answer 1

1) да. Самый простой аргумент в том, что задачи Ada выполняются в одном и том же контексте процесса, делая задачи / потоки несколько быстрее, чем отдельные процессы. Функции межуровневого общения и синхронизации на уровне языка являются еще одной причиной.

2) Только некоторые версии SPARK запрещают выполнение задач. RavenSPARK (2005) позволяет ставить задачи и формально рассуждать о задачах. Проблема с заданиями заключается в том, что трудно формально рассуждать, особенно с амбициями команды SPARK (доказательство правильности).

3) Вы можете рассмотреть возможность ограничить себя профилем Ravenscar. Но простые задачи Ады уже относительно безопасны (даже если они не могут помешать вам писать хорошие тупики).