共享变量
由多个任务共享且防止任务并发访问的全局变量
描述
受保护的共享全局变量具有以下属性：
该变量用于多个任务中。
对该变量的所有操作都通过临界区或时序互斥加以保护，以防止中断。对开始和结束临界区的函数的调用必须可达。
在不打算用于多任务的代码中，所有全局变量都是非共享的。
在您的验证结果中，这些变量在源、结果列表和变量访问窗格中被着色为绿色。在源窗格中，仅在声明期间才会向变量应用着色。
示例
#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 是一个受保护的共享变量：
在命令行上，您可以使用以下命令：
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 是一个受保护的共享变量：
在命令行上，您可以使用以下命令：
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进行操作。
如果您选择结果，则结果详细信息窗格会指明访问模式将保护对该变量执行的所有操作。在变量访问窗格中，变量 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 进行保护。结果详细信息窗格和变量访问窗格显示保护类型为 Design Pattern。
互斥锁锁定和解锁机制对另一个共享变量 var 进行保护。结果详细信息窗格和变量访问窗格显示保护类型为 Mutex。
Code Prover 不检测没有名称的共享内存区域。可以通过将绝对地址指定给指针或动态分配内存来创建未命名的内存区域。不存在表示这些区域的命名变量。
例如，在下方示例中，ptr 指向动态分配的内存。
#include <stdlib.h>
int* ptr;
void flip() {
*ptr = 0;
}
void flop() {
if (*ptr == 0) {
*ptr = 1;
}
}
void main() {
ptr = (int*) malloc(sizeof(int));
}flip() 和 flop() 充当您的应用程序的入口函数，Code Prover 也不会显示 ptr（或 *ptr）指向的内存区域可以被并发访问。检查信息
| 语言：C | C++ |
