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
ЕГО Метрика: Нет

См. также

| | |

Введенный в R2018b

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

Поддержка