Глобальные переменные, общие между несколькими задачами и защищенные от параллельного доступа задачами
Общая защищенная глобальная переменная имеет следующие свойства:
Переменная используется более чем в одной задаче.
Все операции с переменной защищены от прерывания через критические разделы или временное исключение. Вызовы функций, начинающихся и заканчивающих критический раздел, должны быть доступными.
В коде, который не предназначен для многозадачности, все глобальные переменные являются совместными.
В ваших верификациях результатах эти переменные окрашены в зеленый цвет на 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 mutex, которая pthread_mutex_lock и pthread_mutex_unlock используйте, чтобы заблокировать и разблокировать их мьютексы. Характерные для pthread шаблоны проекта защищают lock. Панель Results Details и панель Variable Access списка Design Pattern как тип защиты.
Механизмы блокировки и разблокировки мьютекса защищают var, другая общая переменная. Панель Results Details и панель Variable Access списка Mutex как тип защиты.
| Язык: C | C++ |
Critical section details (-critical-section-begin -critical-section-end) | Potentially unprotected variable | Show global variable sharing and usage only (-shared-variables-mode) | Tasks (-entry-points) | Temporally exclusive tasks (-temporal-exclusions-file) | Unused variable | Used non-shared variable