Глобальные переменные совместно используются несколькими задачами и защищенные от параллельного доступа задачами
Разделяемая защищенная глобальная переменная имеет следующие свойства:
Переменная используется больше чем в одной задаче.
Все операции на переменной защищены от прерывания до критических разделов или временного исключения. Вызовы начала функций и окончания критического раздела должны быть достижимыми.
В коде, который не предназначается для многозадачности, все глобальные переменные неразделяемы.
В ваших результатах верификации эти переменные окрашены в зеленый на Source, Results List и панелях Variable Access. На панели Source окраска применяется к переменной только во время объявления.
#include <limits.h>
int shared_var;
void inc() {
shared_var+=2;
}
void reset() {
shared_var = 0;
}
void task() {
volatile int randomValue = 0;
while(randomValue) {
reset();
inc();
inc();
}
}
void interrupt() {
shared_var = INT_MAX;
}
void interrupt_handler() {
volatile int randomValue = 0;
while(randomValue) {
interrupt();
}
}
void main() {
}В этом примере shared_var является защищенной совместно используемой переменной, если вы задаете следующие многозадачные опции:
| Опция | Значение | |
|---|---|---|
| Сконфигурируйте многозадачность вручную |  | |
| Задачи |
| |
| Временно исключительные задачи | task interrupt_handler | |
На командной строке можно использовать следующее:
polyspace-code-prover -entry-points task,interrupt_handler -temporal-exclusions-file "C:\exclusions_file.txt"
C:\exclusions_file.txt имеет следующую строку: task interrupt_handler
Переменная совместно используется task и interrupt_handler. Однако, потому что task и interrupt_handler временно исключительны, операции на переменной не могут прервать друг друга.
#include <limits.h>
int shared_var;
void inc() {
shared_var+=2;
}
void reset() {
shared_var = 0;
}
void take_semaphore(void);
void give_semaphore(void);
void task() {
volatile int randomValue = 0;
while(randomValue) {
take_semaphore();
reset();
inc();
inc();
give_semaphore();
}
}
void interrupt() {
shared_var = INT_MAX;
}
void interrupt_handler() {
volatile int randomValue = 0;
while(randomValue) {
take_semaphore();
interrupt();
give_semaphore();
}
}
void main() {
}В этом примере shared_var является защищенной совместно используемой переменной, если вы задаете следующее:
| Опция | Значение | |
|---|---|---|
| Сконфигурируйте многозадачность вручную | | |
| Задачи |
| |
| Критические детали раздела | Starting routine | Ending routine |
take_semaphore | give_semaphore | |
На командной строке можно использовать следующее:
polyspace-code-prover -entry-points task,interrupt_handler -critical-section-begin take_semaphore:cs1 -critical-section-end give_semaphore:cs1
Переменная совместно используется task и interrupt_handler. Однако, потому что операции на переменной между вызовами запуска и конечной процедуры того же критического раздела, они не могут прервать друг друга.
struct S {
unsigned int var_1;
unsigned int var_2;
};
volatile int randomVal;
struct S sharedStruct;
void task1(void) {
while(randomVal)
operation1();
}
void task2(void) {
while(randomVal)
operation2();
}
void operation1(void) {
sharedStruct.var_1++;
}
void operation2(void) {
sharedStruct.var_2++;
}
int main(void) {
return 0;
}В этом примере sharedStruct является защищенной совместно используемой переменной, если вы задаете следующее:
| Опция | Значение | |
|---|---|---|
| Сконфигурируйте многозадачность вручную | | |
| Задачи |
| |
На командной строке можно использовать следующее:
polyspace-code-prover
-entry-points task1,task2
Программное обеспечение решает, что sharedStruct защищен потому что:
task1 работает только с sharedStruct.var_1.
task2 работает только с sharedStruct.var_2.
Если вы выбираете результат, панель Result Details указывает, что схема доступа защищает все операции на переменной. На панели Variable Access строка для переменной sharedStruct перечисляет Access pattern как тип защиты.
#include <pthread.h>
#include <stdlib.h>
pthread_mutex_t lock;
pthread_t id1, id2;
int var;
void * t1(void* b) {
pthread_mutex_lock(&lock);
var++;
pthread_mutex_unlock(&lock);
}
void * t2(void* a) {
pthread_mutex_lock(&lock);
var = 1;
pthread_mutex_unlock(&lock);
}
int main(void) {
pthread_create(&id1, NULL, t1, NULL);
pthread_create(&id2, NULL, t2, NULL);
return 0;
}var является разделяемым, защитил переменную, если вы задаете следующие опции:
| Имя опции | Значение |
|---|---|
| Включите автоматическое обнаружение параллелизма | |
На командной строке можно использовать следующее:
polyspace-code-prover
-enable-concurrency-detectionВ этом примере, если вы задаете опцию обнаружения параллелизма, Polyspace® Code Prover™ обнаруживает, что ваша программа использует многозадачность. Две задачи, lock и var, совместно используют две переменные. lock является pthread взаимоисключающей переменной, который pthread_mutex_lock и использование pthread_mutex_unlock, чтобы заблокировать и разблокировать их взаимные исключения. Свойственные pthread шаблоны разработки защищают lock. Панель Results Details и панель Variable Access перечисляют Design Pattern как тип защиты.
Взаимное исключение блокирующие и разблокировавшие механизмы защищает var, другую совместно используемую переменную. Панель Results Details и панель Variable Access перечисляют Mutex как тип защиты.
| Язык: C | C++ |