理论计算机科学电子笔记174（2007）139-150www.elsevier.com/locate/entcs通过线程验证1John Regehr2 Nathan Cooprider3犹他大学计算机学院摘要大部分的研究都集中在多线程代码上。另一方面，低端嵌入式系统中的并发主要基于中断。低端嵌入式系统在安全关键应用中无处不在，例如支持交通和医疗自动化的应用;它们的验证非常重要。虽然中断在表面上类似于线程，但这两种抽象之间存在微妙的语义差异。本文从验证是否存在竞争条件的角度对线程和中断进行了比较和对比。 我们确定了一个小的扩展集，允许线程验证工具，也验证中断驱动的软件，我们提出的源到源转换的例子，把中断驱动的代码变成语义等价的基于线程的代码，可以检查的线程验证。最后，我们展示了一个概念验证程序转换工具，将中断驱动的传感器网络应用程序转换为多线程代码，我们使用现有的工具来查找这些应用程序中的竞争条件保留字：竞争条件，中断，线程，嵌入式软件1引言对于在PC级硬件上的通用操作系统上运行的程序另一方面，中断是低端嵌入式系统（如基于微控制器单元（MCU）的系统）中表示并发性的主要方法所有主要的MCU架构都支持中断，并且大量此类芯片部署在嵌入式系统中：根据Gartner的报告，2003年共出货了35亿个8位MCU和10亿个16位MCU。中断驱动软件的正确性非常重要：这45亿MCU中有相当一部分部署在安全关键型应用中，如车辆控制和医疗自动化。例如，一些非常严重的Therac-25错误[17，应用程序。A]是由涉及中断处理程序的竞争条件直接引起的1 这项工作得到了国家科学基金会职业奖CNS-0448047的支持。2电子邮件地址：regehr@cs.utah.edu3 电子邮件地址：coop@cs.utah.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.002140J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139大多数验证并发软件的工作都集中在基于线程和基于进程的并发上，中断受到的关注相对较少。本文的论点是：在中断驱动的系统中，没有竞争条件是很重要的，但这方面的技术还很原始。我们必须理解中断和它们的语义，以便理解线程验证器可以和不可以应用于中断驱动的系统。特别是，我们希望为基于线程的程序确定一组最小的扩展验证器，允许它们也检查基于中断的程序。第二个目标是利用中断的语义，使检查更快、更精确。当然，线程有很多种。在本文中，我们假设POSIX风格线程语义的常见情况[5]：抢先调度阻塞线程，在内核或用户级别调度。然而，本文中的源代码示例使用了简化的语法，而不是使用冗长的POSIX调用。2中断和线程本节概述了线程区别于中断的重要方式见[21]更详细的处理中断和他们的使用。2.1阻挡线程编程模型的一个关键部分是它们的阻塞能力：操作系统透明地挂起执行，直到满足某些条件。阻塞很重要，原因有几个。首先，它支持时间切片。其次，它为编程模型增加了一个重要的冗余度：开发人员不需要检查要使用的资源是否繁忙-操作系统透明地阻止请求线程，直到资源可用。中断不能阻塞：除非被其他中断抢占，否则它们会一直运行到结束。无法阻塞是非常不方便的，并且使得中断无法使用高级操作系统服务。另一方面，非阻塞执行也有一些引人注目的优点.首先，除了非中断执行上下文之外，所有中断都当然，线程需要自己的堆栈，这使得它们不适合通常只有几KB RAM的低端MCU。其次，由于中断从不阻塞，它们的内部状态对非中断代码是不可见的换句话说，中断相对于在非中断上下文中运行的代码以原子方式执行。第三，非阻塞执行意味着中断可以具有高度可预测的定时。最后，中断处理程序不受大多数形式的死锁的影响2.2抢占和调度线程通常具有对称的抢占关系：对于任何给定的线程对，任何一个都可以抢占另一个。一般来说，即使对于线程也J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139141因为即使是高优先级的线程也可能由于进行阻塞内核或库调用而被自动阻塞，或者由于页面错误而被自动阻塞。相反，非对称抢占关系是中断的规范。首先，所有中断都可以抢占非中断代码，而非中断代码永远不能抢占任何中断。其次，中断是使用固定优先级调度的，导致中断处理程序之间的不对称抢占某些硬件平台，如PC上的可编程中断控制器，强制中断的优先级调度。在其他系统中，优先级中断调度必须在软件中实现。例如，Atmel AT-mega 128 [2]，一种流行的MCU，是Mica 2传感器网络节点的基础[7]，仅在并发挂起的中断之间执行优先级调度。一旦中断开始在ATmega128上执行，如果中断被使能，它可以被任何优先级的中断抢占。为了在该平台上实现基于优先级的抢占式调度，软件必须操纵与各种中断相关联的各个使能位。2.3并发控制线程锁使用阻塞来防止线程通过给定的程序点，直到锁资源变得可用。由于中断一旦开始执行就不能被阻止，因此并发控制包括防止中断首先开始执行。这可以通过禁用所有中断或选择性地仅禁用可能干扰特定计算的中断来实现。前者更便宜，而后者避免了不相关代码的延迟。由于基于中断的系统中的抢占是不对称的，所以锁定策略也是不对称的。换句话说，虽然非中断上下文必须禁用中断以便相对于中断原子地执行，但是在中断模式中运行的代码不需要采取任何特殊动作来相对于非中断代码原子地运行。2.4再进入如果同一个处理程序可能有多个并发调用，则中断是可重入的可重入中断有两种：偶然中断和故意中断。当开发人员对在中断处理程序中启用中断的后果感到不安时，会发生意外重入我们提到这种类型的重入，因为它通常会导致错误的系统，因为根据我们的经验，它在实际的嵌入式系统中很常见。故意重入是一种复杂的技术，可用于减少中断延迟。当靠近长时间运行的中断处理程序的开始的代码受到时间约束时，它很有用。通过允许处理程序的后续调用在前一个调用完成执行之前触发，可以减少处理程序早期部分的平均延迟例如，计时器142J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139AvrX系统[4]中的中断处理程序是可重入的，以避免丢失节拍。重返有两个不可避免的成本。 首先，处理程序的后面部分的平均延迟将增加，而不是减少，因为工作保存系统中的总延迟是零和游戏。第二，在实践中，创建正确的可重入中断代码，即使是专家开发人员。2.5调用样式有些中断是自发的：它们可能在任何时候触发。例如，由网络接口生成的中断是自发的。其他中断是被请求的：它们只在响应运行中的程序所采取的动作时发生。例如，定时器中断请求，是模拟数字转换器（ADC）完成中断。中断请求和子中断之间的因果关系只能通过理解底层硬件的语义来理解2.6延迟呼叫中断通常受到时间约束：它们需要在成为挂起后的有限时间内执行。确保满足这些约束的最好方法是缩短中断处理程序。一个常见的习惯用法是中断执行与中断请求相关的最小计算，例如确认硬件条件并可能将与中断相关的数据移动到内存缓冲器中。然后，中断处理程序在一个延迟的上下文中启动一个长时间运行的计算，比如一个bottom-half处理程序或线程。3中断本节介绍如何使用源到源转换将中断驱动程序转换为语义上等效的基于线程的程序，以便可以使用线程验证工具来查找原始系统中的错误考虑一个包含两个中断处理函数的C程序：irq5（）和irq7（）。我们进一步假设中断是使用优先级来调度的：中断5可以抢占中断7，但不能反过来。一个不可移植的语言扩展中断函数的序言和结尾代码，而不是使用标准调用约定。从中断处理程序调用的任何函数都可以使用标准调用约定。这个系统的代码框架publicvoid run（）{...代码...}publicvoid run（）{J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139143...代码...}public intfindDuplicate（）{...代码...}当然，这些代码不能被理解线程的验证工具按原样检查;它需要被源代码到源代码的翻译工具重写。要将中断视为线程，验证工具必须将中断视为在无限循环中调用：void irq5_thread（void）{ while（1）irq5（）;}第77章类似此外，中断线程必须在引导时产生：public intfindDuplicate（）{...初始化代码：运行中断禁用. return（irq5_thread）;return（irq7_thread）;...主循环代码：运行中断启用.}产生模拟中断处理程序的线程的程序点应该对应于中断首次启用的点。一个典型的嵌入式系统运行系统初始化代码时中断被禁用，然后在运行主程序循环之前启用中断3.1阻塞、抢占和调度在预期的情况下，两个线程可以在任何指令边界处各自抢占彼此，其中抢占不被锁抑制。另一方面，中断通常不受动态优先级调整的影响，并且决不能因页面错误或任何其他原因而阻塞。因此，最高优先级的可运行中断总是执行：优先级是严格执行的。应该在模型检查器中添加对“严格优先级”的支持，以便支持对基于中断的代码的分析。第一个好处是，这将消除误报：实际上不可能发生的竞争条件。第二个好处是可以通过考虑更少的抢占点来减小状态空间这一见解被Hatterygal等人[11]在固定优先级线程的上下文中加以利用，但不清楚他们是如何处理通过页面错误的优先级反转的问题的-在他们的论文中没有解决这个问题用于对中断进行建模的线程必须具有优先级，验证工具将优先级解释为严格：public intfindDuplicate（）{144J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139...初始化代码：运行中断禁用.创建线程（irq5_thread，HIGHEST_STRICT_PRIORITY）;创建线程（irq7_thread，SECOND_HIGHEST_STRICT_PRIORITY）;...主循环代码：运行中断启用.}分配给中断处理程序的优先级范围不要与线程可用的优先级范围重叠，这一点3.2并发控制为了模拟中断类型的并发控制，必须创建线程锁来模拟处理器的中断使能位。在原始的基于中断的程序中，用于原子执行的函数看起来像这样：void begin_critical_section（void）{//用于禁用中断的}临界截面（void）{//非可移植的中断使能代码}实际上，这些函数是以这样一种方式编写的，即当递归使用递归锁是那些可以安全地多次获取的这里我们忽略递归锁的问题;它们的语义在线程化和基于中断的代码中是相同的。为了创建线程检查工具可以使用的这些函数的版本，我们将它们翻译如下：void begin_critical_section（void）{获取互斥量（irq5_lock）;获取互斥量（irq7_lock）;}临界截面（void）{release_mutex（irq5_lock）;release_mutex（irq7_lock）;}为了完成支持并发控制的转换，我们需要通过要求每个“中断线程”总是在持有适当锁的情况下运行，将非对称中断式同步转换为对称线程式J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139145public void run（）{run（1）{mysql（）;mysql（）;release_mutex（irq5_lock）;}}public void run（）{run（1）{public int findDuplicate（）;release_mutex（irq7_lock）;}}有必要为每个中断处理程序设置一个锁，而不是一个全局锁，以模拟中断处理程序可以相互抢占的情况3.3再进入可重入中断是可以同时在堆栈上进行多个调用的中断。由于并发调用的数量通常不能是有界的，因此只有能够对无限数量的线程进行建模的验证器，例如Henzinger等人。Blast [12]的CIRC扩展，适用于可重入中断的推理。3.4调用样式到目前为止，给出的代码对可能在任何时刻触发的自发中断进行了建模;它也可以用于对请求中断进行建模，但这会丢失有关请求和后续中断之间因果关系的信息。我们知道没有一个分析中断的工具可以利用请求和中断之间的因果关系要对中断请求建模，必须手动或自动插入显式中断请求调用。中断请求可以使用条件变量暴露给线程检查工具：void request_irq5（void）{ cond_signal（irq5_request）;}然后，相关联的中断仅允许在请求之后触发：public void run（）{run（1）{cond_wait（irq5_request）;acquire_mutex（irq5_lock）;146J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139return（）;release_mutex（irq5_lock）;}}3.5延迟呼叫由于中断请求导致中断触发，中断导致延迟代码运行。延迟线程模式代码不需要特殊支持，因为中断将使用标准线程原语向等待线程发出信号。Linux内核中的下半处理程序或Windows内核中的DPC（延迟过程调用）必须建模为运行到完成代码，其优先级严格高于任何实际线程，严格低于任何中断。3.6总结线程验证工具可用于在三种情况下检查中断驱动的软件(i) 使用源代码到源代码转换工具将中断代码转换为语义等效的线程代码。(ii) 线程检查工具支持一个单独的严格优先级类，它（1）比任何实际线程的优先级都高，（2）对中断相对于低优先级中断和非中断代码以原子方式运行的事实进行(iii) 如果中断驱动的代码包含任何可重入中断，则线程检查工具必须能够对单个中断处理程序的多个未完成调用进行建模。4初步结果本节报告使用本文中的技术的概念验证实现的结果4.1方法我们为CIL编写了一个插件[19]，它将TinyOS应用程序[13]转换为POSIX线程程序，然后我们使用Locksmith [20]检查竞争条件。TinyOS应用程序的nesC编译器[10]包括一个竞争条件检测器，但由于没有遵循指针，它是不可靠的。这个转换与第3节中概述的转换非常相似。转换工具并不难实现，其中一位作者花了大约五个小时。4.2结果表1显示了此实验的结果，使用了一组针对Mica2传感器网络平台的TinyOS 1.0应用程序。The “LOC” columnJ. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139147应用LOC中断锁匠种族cXprop 种族眨眼1920110CntToLedsAndRfm804353711ECC885153911GenericBase69415301示波器558741620SenseTask3490220激增1102254613Fig. 1. TinyOS应用程序在经过nesC编译器处理后，应用程序中的C代码行数，“Interrupts”列表示中断处理程序的数量，Mica2节点所基于的Atmel ATmega128处理器最多支持34个中断处理程序。表1中的第四列显示了Locksmith检测到的竞争变量的数量，第五列显示了cXprop [6]检测到的竞争数量，这是我们开发的一种工具，可以很好地分析TinyOS应用程序的竞争条件。4.3分析很难直接比较Locksmith和cXprop发现的种族数量，因为这两种工具的操作非常不同。在这里，我们研究的主要分歧。首先，cXprop假设临界区是词法嵌套的-这是nesC编译器提供的保证，例如，TinyOS应用程序不能在中断锁保持的情况下进入函数，然后在锁释放的情况下退出它。这个程序属性大大简化了并发分析。当cXprop用于分析嵌入式程序而不是TinyOS应用程序时，必须手动验证词法嵌套临界区的假设。其次，Locksmith还不支持递归锁：那些可以安全地多次获取的锁。TinyOS代码大量使用嵌套锁，导致Locksmith报告不存在的竞争条件。这个问题反映了TinyOS和Locksmith之间真正的阻抗不匹配，使用源到源转换无法轻松解决第三，cXprop运行相当积极的数据流分析，试图找到死代码和数据，以减少报告的竞争条件的数量。最后，请注意，许多检测到的种族不是错误。其他可能性包括：• 没有竞争条件：分析器不可见的程序属性确保变量实际上不会被并发访问。• 没有竞争条件：用户定义的同步习惯用法确保在没有显式锁定的情况下满足数据不变量。148J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139• racing变量保存非关键信息，如性能计数器，开发人员不关心它是否偶尔被损坏5今后工作5.1把翻译并发无论是线程还是中断的形式都很难推理。我们想提出一个正式的论点，即第3节中提出的翻译保留了嵌入式系统的语义一个重要的障碍是我们所知道的任何基于中断的平台都缺乏正式的语义。更糟糕的是，在编译器和硬件平台之间，中断语义有很大的差异;参见[21，§2]。另一方面，多线程C和C++语义的必要性是很好理解的，并且正在进行该方向的工作[1，24]。5.2混合并发模型许多系统不仅支持中断和线程，而且还支持延迟调用，例如Windows中的DPC和Linux中的tasklet，它们具有自己的语义。通常，可以使用各种锁，每种锁都针对这些并发抽象的某个子集提供保护。在大型代码库（如Windows或Linux内核）中，并发和同步抽象的多样性成为创建正确代码的障碍。需要一种原则性的方法来推理异构我们以前的工作包括TSL [22]，这是朝着这个方向迈出的第一步。5.3其他中断bug除了竞争条件之外，中断还容易产生许多错误这些包括堆栈溢出、活锁、中断上下文中的阻塞、错误使用不可重入函数以及错误的可重入中断处理程序。不幸的是，没有明显的方法可以通过转换为线程代码并使用现有的线程检查工具来检查大多数这些类型的错误。6相关工作本节简要介绍了中断语义和中断驱动程序验证的文献。6.1语义学大多数将中断融入系统语义的尝试都例如，Hills [14]提供了可能是与中断相关的问题的最清晰的现有描述，并提出了一种解决方案，其中中断处理程序只是一个原子存根，它唤醒一些J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139149螺纹.这些线程执行通常在中断上下文中运行的处理。类似地，Leyva-del-Foyo和Mejia-Alvarez6.2中断驱动系统nesC [10]是TinyOS应用程序的编程语言，它通过查找由中断处理程序访问且不受原子执行保护的变量来检查中断驱动应用程序中的竞争条件Henzinger等人[12]使用分析来改进nesC的竞争检查，该分析可以表明某些非原子变量访问是安全的。Mercer和Jones [18]利用GDB的状态保存和恢复功能来模型检查中断驱动的嵌入式代码。SLAM [3]模型检查器和RacerX [9]竞争条件检测器用于查找内核代码中的错误，包括中断处理程序。7结论本文的贡献是一个通用的使能技术的中断驱动的嵌入式软件的验证，利用现有的多线程代码的验证工具这是有用的，因为绝大多数的研究都集中在基于线程的应用程序上。我们的技术包括离开一个应用程序在很大程度上保持不变，而把状态与中断语义到语句与等价的线程语义。这很有趣，也可能很棘手，因为这两种语义之间存在微妙的差异。我们已经通过将中断驱动的TinyOS应用程序转换为线程代码，然后使用现有的竞争条件检测器来查找潜在的错误，从而证明了我们的技术的实用性。引用[1] Alexandrescu，A.，H. Boehm，K. Henney，D. Lea和B. Pugh，多线程C++（2004年），http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2004/n1680.pdf的 网 站 。[2] Atmel公司 ATmega128系列（2002），http://www.atmel.com/atmel/acrobat/doc2467.pdf。[3] 鲍尔，E.布尼莫娃湾Cook，V. Levin，J. Lichtenberg，C.麦加维湾Ondrusek，S. K. Rajamani和A.Ustuner，设备驱动程序的全面静态分析，在：第一届EuroSys大会上。，Leuven，Belgium，2006.[4] 巴雷洛湖AvrX实时内核（2004），http://barello.net/avrx。[5] Butenhof，D.，“Programming with POSIX Threads,” Addison Wesley,[6] Cooprider，N.和J.Regehr，Pluggable abstract domains for analyzing embedded software，in：Proc.ofthe 2006 Conf.on Languages， Builderers， and Tools for Embedded Systems（ LCTES） ， Ottawa，Canada，2006，pp. 44比53[7] Crossbow Technology，Inc. ，http://xbow.com.[8] 德尔福约湖E. L.和P. Mejia-Alvarez，Custom interrupt management for real-time and embedded systemkernels，in：Proc. of the Workshop on Embedded and Real-Time Systems Implementation（ERTSI），Lisbon，Portugal，2004。150J. Regehr，N.Cooprider/Electronic Notes in Theoretical Computer Science 174（2007）139[9] Engler，D.和K. Ashcraft，RacerX：竞争条件和死锁的有效静态检测，在：第19届ACM Symp. 操作系统原理（SOSP），Bolton Landing，NY，2003年。[10] 盖伊，D.，P. Levis，R. von Behren ，M. Welsh ，E. Brewer和D. Culler，The nesC language：Aholisticapproach to networked embedded systems，Proc. 的Conf. 编程语言设计和实现（PLDI），圣地亚哥，加利福尼亚州，2003年，页。1比11[11]Hatterygal，J.，X.邓，M. B. Dwyer，G. Jung和V.P. Ranganath，Cadena：基于组件的系统的集成开发，分析和验证环境，第25届国际会议论文集。Conf. on Software Engineering（ICSE），Portland，OR，2003，pp. 160-173。[12] Henzinger，T.一、R.贾拉河Majumdar和G. Sutre，Blast软件验证，第10届国际会议论文集。软件模型检测研讨会（SPIN），波特兰，OR，2003年，pp。235-239.[13] 希尔，J.，R. Szewczyk，A.吴，S。Hollar，D. Culler和K. Pister，网络传感器的系统架构方向，在：Proc.第九届国际Conf. 编程语言和操作系统的架构支持（ASPLOS），剑桥，马萨诸塞州，2000年，页。93比104[14] 希尔斯，T.，结构化中断，ACM SIGOPS Operating Systems Review27（1993），pp. 51比68[15] Kleiman ， S. 和 j.Eykholt ， Interrupts as threads ， ACM SIGOPS Operating Systems Review29（1995）。21-26号。[16] 莱斯利岛D.麦考利河布莱克，T。Roscoe，P. Barham，D.埃弗斯河 Fairbairns和E. 许文龙，多媒体应用系统的设计与实现，国立成功大学计算机科学研究所硕士论文，1996年。公元1280-1297年。[17] Leveson，N.，[18] Mercer，E. G.和M. D. Jones，Model checking machine code with the GNU debugger，in：Proc. of theSPIN Workshop on Model Checking of Software，San Francisco，CA，2005.[19] Necula、G. C.的方法，S. McPeak，S. P. Rahul和W. Weimer，CIL：Intermediate language and tools foranalysis and transformation of C programs ， in ： Proc. of the Intl.Conf. on Concrete Construction（CC），Grenoble，France，2002，pp. 213-228[20] Pratikakis，P.，J. S.福斯特和M。 Hicks，Context-sensitive correlation analysis for detecting races，in ： Proc. of the ACM SIGPLAN 2006 Conf. on Programming Language Design and Implementation（PLDI），2006。[21] Regehr，J.，在实时和嵌入式软件中中断的安全和结构化使用。Lee，J. Y.- T. Leung和S. Son，编者，《实时与嵌入式系统手册》，CRC出版社，2007年。[22] Regehr，J.，A. Reid，K. Webb，M. Parker和J.Lepreau，使用分层调度和并发分析的实时系统，在：第24届IEEE实时系统研讨会上。（RTSS），墨西哥坎昆，2003年。[23] 所罗门，D. A.和M. E. Russinovich，[24] 萨特，H.，Prism：一个基于原则的微软本机代码平台（2006年），http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2075.pdf的 网 站 。[25] TimeSys Corporation，TimeSys Linux，http://timesys.com/。
我的内容管理
展开
