共享变量
由多个任务共享且防止任务并发访问的全局变量
描述
受保护的共享全局变量具有以下属性:
该变量用于多个任务中。
对该变量的所有操作都通过临界区或时序互斥加以保护,以防止中断。对开始和结束临界区的函数的调用必须可达。
在不打算用于多任务的代码中,所有全局变量都是非共享的。
在您的验证结果中,这些变量在源、结果列表和变量访问窗格中被着色为绿色。在源窗格中,仅在声明期间才会向变量应用着色。
示例
#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++ |
MATLAB Command
You clicked a link that corresponds to this MATLAB command:
Run the command by entering it in the MATLAB Command Window. Web browsers do not support MATLAB commands.
选择网站
选择网站以获取翻译的可用内容,以及查看当地活动和优惠。根据您的位置,我们建议您选择:。
您也可以从以下列表中选择网站:
如何获得最佳网站性能
选择中国网站(中文或英文)以获得最佳网站性能。其他 MathWorks 国家/地区网站并未针对您所在位置的访问进行优化。
美洲
- América Latina (Español)
- Canada (English)
- United States (English)
欧洲
- Belgium (English)
- Denmark (English)
- Deutschland (Deutsch)
- España (Español)
- Finland (English)
- France (Français)
- Ireland (English)
- Italia (Italiano)
- Luxembourg (English)
- Netherlands (English)
- Norway (English)
- Österreich (Deutsch)
- Portugal (English)
- Sweden (English)
- Switzerland
- United Kingdom (English)