Глобальные переменные, совместно используемые несколькими задачами и защищенные от параллельного доступа этими задачами
Общая защищенная глобальная переменная имеет следующие свойства:
Переменная используется в нескольких задачах.
Все операции над переменной защищены от прерывания через критические разделы или временное исключение. Вызовы функций, начинающихся и заканчивающихся в критическом разделе, должны быть доступны.
В коде, не предназначенном для многозадачности, все глобальные переменные не являются общими.
В результатах проверки эти переменные окрашиваются в зеленый цвет на панелях Источник (Source), Список результатов (Results List) и Доступ к переменным (Variable Access). На панели Источник раскраска применяется к переменной только во время объявления.
#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 является защищенной общей переменной, если указано следующее:
| Выбор | Стоимость | |
|---|---|---|
| Настройка многозадачности вручную | | |
| Задачи |
| |
| Детали критического раздела | Запуск подпрограммы | Завершение процедуры |
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) отображается, что шаблон доступа защищает все операции над переменной. На панели «Доступ к переменной» строка переменной 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. Панель «Сведения о результатах» и список областей «Доступ к переменным» Design Pattern в качестве типа резервирования.
Механизмы блокировки и разблокировки мьютекса обеспечивают защиту var, другая общая переменная. Панель «Сведения о результатах» и список областей «Доступ к переменным» 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