Exponenta Banner
exponenta event banner

Shared variable

Глобальные переменные совместно используются несколькими задачами и защищенные от параллельного доступа задачами

расширьте все на странице

Описание

Разделяемая защищенная глобальная переменная имеет следующие свойства:

  • Переменная используется больше чем в одной задаче.

  • Все операции на переменной защищены от прерывания до критических разделов или временного исключения. Вызовы начала функций и окончания критического раздела должны быть достижимыми.

В коде, который не предназначается для многозадачности, все глобальные переменные неразделяемы.

В ваших результатах верификации эти переменные окрашены в зеленый на 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

Временно исключительные задачи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 защищенная совместно используемая переменная, если вы задаете следующее:

ОпцияЗначение
Сконфигурируйте многозадачность вручную
Задачи

task

interrupt_handler

Критические детали разделаStarting routineEnding routine
take_semaphoregive_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 защищенная совместно используемая переменная, если вы задаете следующее:

ОпцияЗначение
Сконфигурируйте многозадачность вручную
Задачи

task1

task2

На командной строке можно использовать следующее: 

 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++

Смотрите также

| | | | | |

Темы

Документация Polyspace Code Prover

Поддержка