Shared variable

Global variables shared between multiple tasks and protected from concurrent access by the tasks

Description

A shared protected global variable has the following properties:

• The variable is used in more than one task.

• All operations on the variable are protected from interruption through critical sections or temporal exclusion. The calls to functions beginning and ending a critical section must be reachable.

In code that is not intended for multitasking, all global variables are non-shared.

In your verification results, these variables are colored green on the Source, Results List and Variable Access panes. On the Source pane, the coloring is applied to the variable only during declaration.

Examples

Shared Variables Protected Through Temporal Exclusion

#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() {
}

In this example, shared_var is a protected shared variable if you specify the following multitasking options:

Option	Value
Configure multitasking manually
Tasks (-entry-points)	task interrupt_handler
Temporally exclusive tasks (-temporal-exclusions-file)	task interrupt_handler

For more information on analysis options, see the documentation for Polyspace^® Code Prover™ or Polyspace Code Prover Server™.

On the command-line, you can use the following:

 polyspace-code-prover
   -entry-points task,interrupt_handler
   -temporal-exclusions-file "C:\exclusions_file.txt"

where the file C:\exclusions_file.txt has the following line:

task interrupt_handler

The variable is shared between task and interrupt_handler. However, because task and interrupt_handler are temporally exclusive, operations on the variable cannot interrupt each other.

Shared Variables Protected Through Critical Sections

#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() {
}

In this example, shared_var is a protected shared variable if you specify the following:

Option	Value
Configure multitasking manually
Tasks (-entry-points)	task interrupt_handler
Critical section details (-critical-section-begin -critical-section-end)	Starting routine	Ending routine
	take_semaphore	give_semaphore

For more information on analysis options, see the documentation for Polyspace Code Prover or Polyspace Code Prover Server.

On the command-line, you can use the following:

 polyspace-code-prover 
   -entry-points task,interrupt_handler
   -critical-section-begin take_semaphore:cs1
   -critical-section-end give_semaphore:cs1

The variable is shared between task and interrupt_handler. However, because operations on the variable are between calls to the starting and ending procedure of the same critical section, they cannot interrupt each other.

Shared Structure Variables Protected Through Access Pattern

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;
}

In this example, sharedStruct is a protected shared variable if you specify the following:

Option	Value
Configure multitasking manually
Tasks (-entry-points)	task1 task2

For more information on analysis options, see the documentation for Polyspace Code Prover or Polyspace Code Prover Server.

On the command-line, you can use the following:

 polyspace-code-prover 
    -entry-points task1,task2

The software determines that sharedStruct is protected because:

• task1 operates only on sharedStruct.var_1.

• task2 operates only on sharedStruct.var_2.

If you select the result, the Result Details pane indicates that the access pattern protects all operations on the variable. On the Variable Access pane, the row for variable sharedStruct lists Access pattern as the protection type.

Shared Variables Protected Through Design Pattern and Mutex

#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 is a shared, protected variable if you specify the following options:

Option Name	Value
Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)

For more information on analysis options, see the documentation for Polyspace Code Prover or Polyspace Code Prover Server.

On the command-line, you can use the following:

 polyspace-code-prover
    -enable-concurrency-detection

In this example, if you specify the concurrency detection option, Polyspace Code Prover detects that your program uses multitasking. Two task, lock and var, share two variables. lock is a pthread mutex variable, which pthread_mutex_lock and pthread_mutex_unlock use to lock and unlock their mutexes. The inherent pthread design patterns protect lock. The Results Details pane and Variable Access pane list Design Pattern as the protection type.

The mutex locking and unlocking mechanisms protect var, the other shared variable. The Results Details pane and Variable Access pane list Mutex as the protection type.

Check Information

Language: C | C++