Exponenta Banner

Number of Protected Shared Variables

Количество защищенных совместно используемых переменных

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

Описание

Эта метрика измеряет количество переменных со следующими свойствами:

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

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

Примеры

развернуть все


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

ОпцияЗначение
Tasks (-entry-points)

task

interrupt_handler

Temporally exclusive tasks (-temporal-exclusions-file)temporal_exclusion.txt

В командной строке задайте эти опции, чтобы запустить пример:

-entry-points task,interrupt_handler  -temporal-exclusions-file temporal_exclusion.txt
temporal_exclusion.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 защищенная совместно используемая переменная, если вы задаете следующее:

ОпцияЗначение
Entry points

task

interrupt_handler

Critical section detailsStarting routineEnding routine
take_semaphoregive_semaphore

В командной строке задайте эти опции, чтобы запустить пример:

-critical-section-begin  take_semaphore:cs1
-critical-section-end give_semaphore:cs1   
-entry-points task,interrupt_handle

Переменная совместно используется task и interrupt_handler. Однако, потому что операции на переменной между вызовами запуска и конечной процедуры того же критического раздела, они не могут прервать друг друга.

Метрическая информация

Группа: проект
Акроним: PSHV
Метрика HIS: нет

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

| | |

Введенный в R2018b

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

Поддержка