Polyspace产2022世界杯八强谁会赢?品

并发:竞争条件和死锁

为什么并发性很重要?

工程师们越来越多地将多核架构和处理器用于各种高完整性的嵌入式应用程序,如军事航空电子设备或汽车系统,而不仅仅是传统的嵌入式应用程序,如网络和通信系统。这种趋势在一定程度上是由于对ADAS和V2V通信等应用程序的性能要求不断提高。要利用这样的体系结构,您需要考虑多线程。这带来了一系列新的复杂的设计和验证挑战,特别是在确保此类系统的健壮性和安全性时。其中一些挑战甚至出现在只使用单一核心进行多任务处理的系统中。

有哪些挑战?

并发编程最复杂的挑战之一在于并发线程之间交互的不可预测性。这是因为线程交错是不确定的。测试任何这样的系统都会导致测试用例数量的组合爆炸。这导致了另一个关键的挑战:测试用例发现了错误,但不能再现问题,因为没有办法确定和重复事件的确切顺序。这使得跟踪控制和数据流以确定根本原因变得困难,并且调试并发问题变得昂贵和耗时。因此,在现实生活中,软件验证和测试遗漏了并发性错误。

即使是在单线程嵌入式应用程序中,您也可以在以中断形式与外部感知输入的异步交互中看到一些复杂性。当多个任务访问共享资源(如全局变量)时,您会看到一类新的错误,如竞争条件、数据竞争和死锁。

竞争条件的一个经典示例是两个客户机同时修改服务器上的同一资源的场景,如同时进行银行提款的情况。指的是并发计算wiki部分要阅读关于此示例的更多信息。

多空间静态分析解决方案

Polyspace®工具利用抽象解释的形式化方法技术进行语义分析。Polyspace引擎可以静态地检测并发问题,并跟踪控制和数据流,以帮助调试问题的根本原因。在下面的示例中,由于两个任务(bug_deadlock_task1和bug_deadlock_task2)都在等待另一个任务进入相同的临界区(acquire_sensor()),最终导致死锁。事件跟踪突出显示导致死锁的指令的顺序。

死锁img

演示由Polyspace Bug Finder检测到的死锁以及导致死锁的事件跟踪的简单示例。

指的是完整的列表Polyspace Bug Finder™可以检测到的缺陷。另一个关于并发性错误的新问题是它们对嵌入式系统安全性的影响。诸如CERT C和CWE之类的安全指导方针对并发性缺陷(例如竞态条件)给予高度优先级。

多元空间绿色-无竞态条件

在并发性缺陷中,竞争条件可能是最有害的。多年来,比赛条件导致了一些严重的运行时错误故障,例如Therac-25放射治疗机。研究人员发表了一份详细的运行时错误故障调查报告,该故障导致了几名患者的死亡。

Polyspace Code Prover™是一个完善的静态分析工具,它可以帮助解决这种复杂的非确定性运行时故障,因为它详尽地验证了所有可能的交叉。它还通过考虑最坏的情况来强调潜在的竞争条件。更重要的是,它验证共享资源是否得到了关键部分的适当保护(通过用绿色突出显示它们)。

例如,如果您有多个线程使用的共享全局变量,Polyspace Code Prover不仅调用潜在的竞争条件场景(用橙色突出显示它们),而且还以事件跟踪的形式提供特定的事件序列(交错)。

在下面的示例中,全局变量PowerLevel用橙色突出显示,因为它没有受到多个任务(server1、server2和regulation)的并发访问的保护。对变量的读和写操作的顺序以及与事件跟踪相结合的对数据范围的相应更改,在调试这种竞争条件时很有价值。Polyspace Code Prover进一步以并发访问图的形式提供了详细的控制流,突出显示了任务和函数调用的顺序,如下所示。

死锁,img 2

变量访问为您提供全局变量的详细数据范围。

使用Polyspace产品,您可2022世界杯八强谁会赢?以检测和调试并发缺陷,还可以验证多任务操作的可靠性,以确保您的软件是健壮的。这方面的一个例子是分析共享全局变量的使用情况,Polyspace产品可以为您提供详细的见解,并生成工件,以帮助多任务应用程序的开发和验证活动。2022世界杯八强谁会赢?

了解更多关于Polyspace产品的信息。2022世界杯八强谁会赢?

阿莱尼亚·马基公司

“对我们来说,基于模型的设计的一个关键优势是能够专注于设计和开发,而不是低级的编码、验证和认证任务。结果是更高的质量,DO-178B认证的软件,以及更快的迭代。”

Baidu
map