McMini: A Programmable DPOR-Based Model Checker for Multithreaded Programs
本文提出可扩展的 DPOR 模型检查器 McMini，支持用少量 C 代码定义原语线程操作与唤醒策略，从而减少调度搜索并显著提升多线程程序验证效率。
2023-07-14 cs.LO cs.PL
Dynamic Verification for File Safety of Multithreaded Programs
在本文中，我们提出了一个新的语义检查多线程程序的文件安全性。一个文件安全的程序是一个达到最终配置下提出的语义。我们用文件操作和多线程命令扩展了While语言，并将新语言称为whilef。本文证明了文件的安全性是一个不可判定的性质。在本文给出的一种特殊情况下，文件安全性成为一个可判定的属性。这种情况发生在用户提供指针信息时。如果文件是安全的，我们称之为强安全文件程序。我们修改了语言的语法和语义，并称之为SafeWhilef。
2012-06-05 cs.LO cs.PL
Thread-Modular Static Analysis for Relaxed Memory Models
提出了一种内存模型感知的静态程序分析方法，用于精确分析运行在具有弱一致性模型（如x86-TSO、SPARC-PSO和SPARC-RMO）的处理器上的并发软件的行为。在我们的方法的中心是一个统一的框架，用于决定线程间干扰的可行性，以避免传播虚假的数据流在静态分析，从而提高静态分析器的性能。我们制定的检查干扰的可行性作为一组数据库规则，这是有效的解决和一般足以捕捉一系列的硬件级内存模型。与现有技术相比，我们的方法可以显着减少虚假警报的数量，以及不健全的证据。我们实现了该方法，并评估了一个大的多线程的C程序集。我们的实验表明，该方法显着优于国家的最先进的技术在准确性方面只有适度的运行时开销。
2017-09-28 cs.PL cs.SE
SL: a "quick and dirty" but working intermediate language for SVP systems
阿姆斯特丹大学的CSA小组开发了SVP，这是一个管理和编程众核和硬件多线程处理器的框架。在本文中，我们介绍了中间语言SL，一种通用的工具来编程SVP平台。SL是标准C语言（ISO C99/C11）的扩展。它包括用于批量创建线程、在线程终止时进行批量同步以及在线程之间使用字大小的同步通道进行通信的基本构造。它的目的是用作高级并行编译器的目标语言。SL是一种研究工具;在撰写本文时，它是唯一一种用于编写主要SVP平台（新的微电网芯片架构）的接口语言。本文提供了该语言的概述，以补充单独提供的详细规范。
2012-08-22 cs.DC cs.PL
Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning (Extended Version)
University of California, Santa Cruz（加利福尼亚大学圣克鲁兹分校）；Williams College（威廉姆斯学院）
研究多线程软件正确性推理中RG逻辑函数规范难复用问题，提出移动逻辑，通过原子函数概念扩展RG逻辑，避免稳定化要求，实用验证器已证其优势，移动逻辑为该领域未来工作奠定基础。
2026-07-28 cs.PL
On the Value and Limits of Multi-level Energy Consumption Static Analysis for Deeply Embedded Single and Multi-threaded Programs
降低计算能耗的兴趣越来越大。能量透明是一个概念，它使程序的能量消耗从软件到硬件通过不同的系统层可见。这样的透明性可以在每一层和层之间实现能量优化，并且帮助程序员和操作系统两者做出能量感知决策。提取程序能耗的常用方法是直接测量目标硬件。这通常涉及大多数程序员不具备的专业设备和知识。在本文中，我们将研究如何利用现有的静态资源分析和能源建模方法来执行能源消耗静态分析（ECSA）的深度嵌入式程序。为了研究这一点，我们已经开发了ECSA技术，工作在指令集的水平和更高的水平，LLVM IR，通过一种新的映射技术。我们将ECSA应用于一组全面的主要工业基准测试，包括来自两种常用并发模式（任务农场和管道）的单线程和多线程嵌入式程序。我们比较我们的ECSA结果的硬件测量和预测的基础上获得的模拟痕迹。我们讨论了一些应用场景，ECSA的结果可以提供能源透明度，并得出结论，为今后的工作提出了一系列新的研究问题。
2015-10-24 cs.PL
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs
无数据竞争程序是一类重要的并发程序。在本文中，我们提供了一个框架，设计和证明的正确性数据流分析，针对这一类的程序。这些分析与早期文献中提出的“同步-CFG”分析具有相同的精神。为了实现这一点，我们首先提出了一种新的具体语义DRF程序，称为L-DRF，这是线程本地的性质-每个线程操作自己的副本的数据状态。我们表明，我们的语义抽象，使我们能够减少DRF程序的分析，顺序分析。这有助于将现有的顺序分析快速移植到DRF程序的合理和可扩展的分析中。接下来，我们将L-DRF参数化，将程序变量划分为原子访问的“区域”。区域参数化语义的抽象产生更精确的分析“区域种族”自由并发程序。我们实例化这些抽象设计高效的关系分析种族自由的程序，我们已经实现了一个原型工具，称为RATCOP。在基准测试中，RATCOP能够证明高达65%的断言，相比之下，我们的基线证明了25%。此外，在与最近的并发静态分析器的比较研究中，RATCOP快了5个数量级。
2020-09-06 cs.PL
Program Execution on Reconfigurable Multicore Architectures
基于两个观察，即不同的应用程序在不同的多核架构上执行得更好，以及应用程序的不同阶段可能具有非常不同的资源需求，Jesus等人提出了一种用于执行多线程程序的新的可重构硬件方法。该体系结构不是将并发程序映射到固定的体系结构，而是自适应地重新配置自身以满足应用程序的并发性和通信要求，从而显著提高了性能。基于我们早期的抽象操作框架，多核执行与层次存储器结构，我们描述了多线程程序的可重构架构，支持各种集群配置的执行。由于可能引入由在不同核上运行的线程对共享存储器的并发访问引起的竞争条件，这种重新配置可能不保留程序的语义。我们提出了一个直观的偏序概念的集群配置，并表明，多线程程序的语义总是保留重新配置“向上”的顺序，而语义保存任意重新配置可以保证良好的同步程序。我们进一步表明，一个简单的近似概念的执行效率上的不同配置可以得到使用摊销互模拟的概念，并将其扩展到动态重新配置。
2016-06-20 cs.DC cs.PF cs.PL
Flow-Sensitive Composition of Thread-Modular Abstract Interpretation
我们提出了一个基于约束的流敏感的静态分析并发程序通过迭代组成线程模块化的抽象解释器，通过使用一个系统的轻量级约束。我们的方法是组合的，因为它首先将顺序抽象解释器应用于各个线程，然后组合它们的结果。它是流敏感的，因为干扰的因果关系排序（从全局写入到读取的数据流）是由约束系统建模的。这些干扰约束是轻量级的，因为它们只涉及程序语句的执行顺序，而不是它们的数值属性：它们可以使用现成的数据库引擎有效地决定。我们的新方法的优势是更准确的比现有的，流不敏感的，静态分析，同时保持可扩展性，并提供预期的健全性和终止保证，即使是无限数据的程序。我们实现了我们的方法，并在大量的基准测试中进行了评估，证明了它在提高线程模块化抽象解释的准确性方面的有效性。
2017-09-28 cs.PL
Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version)
Technical University of Munich（慕尼黑工业大学）；CISPA Helmholtz-Zentrum（CISPA亥姆霍兹信息与安全中心）；National University of Singapore（新加坡国立大学）
该研究扩展digest框架以处理静态数据竞争检测中被忽略的并发结构，引入线程屏障、pthread_once等机制，通过litmus测试评估并对比现有工具，发现其缺乏相关支持，提升了数据竞争检测精度。
2026-09-02 cs.PL cs.SE
A family of abstract interpretations for static analysis of concurrent higher-order programs
我们开发了一个框架，计算两个基本的分析并发高阶程序：（控制）流分析（CFA）和可能发生的并行分析（MHP）。我们特别关注的独特挑战所带来的不受限制的混合一流的延续和动态生成的线程。为了设置阶段，我们制定了一个具体的模型并发高阶程序：P（CEK*）S机。我们发现，这台机器的系统抽象的解释是能够计算流量和MHP分析。然而，仔细检查发现，MHP的精度很差。作为一种补救措施，我们采用了形状分析技术单例抽象动态产生的线程（而不是堆中的对象）。然后，我们表明，如果MHP分析是不感兴趣的，我们可以大大加快计算流分析单独崩溃线程交织与第二层的抽象。
2011-06-14 cs.PL
Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs
我们提出了一个静态分析的抽象解释检查运行时间错误的并行和多线程的C程序。在我们的工作Astrée，我们专注于嵌入式关键程序没有递归，也没有动态内存分配，但扩展到一个静态的线程集的分析，通过共享内存和显式地使用一组有限的互斥锁隐式通信，并根据实时的【形】调度策略和固定的优先级调度。我们的方法是线程模块化的。它是基于一个稍微修改的非平行分析，当分析一个线程，应用和丰富的一组抽象的线程冲突。然后迭代器依次重新分析每个线程，直到冲突稳定下来。我们证明了我们的方法的可靠性顺序一致性语义，但也相对于一个合理的弱一致的内存语义。我们还展示了如何考虑互斥和线程优先级，通过分区的抽象调度状态。我们展示了使用原型Thésée分析工业程序的初步实验结果，并展示了我们方法的可扩展性。
2012-03-22 cs.LO cs.PL
A Comparative Study of the Usability of Two Object-oriented Concurrent Programming Languages
并发性在通用计算中的重要性正在迅速增加，这是由于最近转向多核处理架构。因此，越来越多的开发人员不得不学习编写并发程序，这是一项即使对专家来说也很难的任务。因此，语言设计者们正在致力于使并发编程比使用传统线程库“更容易”的语言。然而，一种新语言比另一种语言更有用的说法不能由纯粹的理论考虑来支持，而需要实证研究。在本文中，我们提出了一个研究的设计，比较并发程序设计语言方面的理解和调试现有的程序和编写正确的新程序。这种研究的一个关键挑战是避免在培训阶段和解释参与者的解决方案时可能引入的偏见。我们通过使用自学材料和评估方案来解决这些问题，该方案暴露了校正器的任何主观决定，或者完全消除它们。我们应用我们的设计比较两个面向对象的语言的并发性，多线程Java和SCOOP（简单并发面向对象编程），在学术环境。我们得到的结果有利于SCOOP，即使研究参与者以前的Java线程的培训。
2010-11-28 cs.PL
Improving Thread-Modular Abstract Interpretation
我们给线程模块化的非关系值分析作为本地跟踪语义的抽象。语义以及分析制定的全球不变量和副作用的约束系统。我们表明，概括的静态分析仪Goblint提供的分析，以及一个自然的改进安托万Miné的方法，可以得到这个一般计划的实例。我们表明，这两个分析是无与伦比的w.r.t.精确度，并提供在精确度方面都有所改进的细化。我们还报告了一个初步的实验比较给定的分析一套有意义的基准。
2021-08-17 cs.PL
Competitive Parallelism: Getting Your Priorities Right
多线程程序传统上分为两个领域：合作和竞争。这两个领域在传统上大多保持不相交，协作线程用于提高计算密集型应用程序（如科学工作负载）的吞吐量，而协作线程用于提高交互式应用程序（如GUI和游戏）的响应能力。随着多核硬件变得越来越主流，有必要将这两个不相交的世界连接起来，因为许多应用程序将交互和计算混合在一起，并且将从协作线程和竞争线程中受益。在本文中，我们提出了技术的并行交互式应用程序，可以使用合作和竞争线程的编程和推理。我们的技术使程序员编写丰富的并行交互式程序，创建和同步线程需要，并通过分配线程用户定义的和部分有序的优先级。为了确保重要的响应特性，我们提出了一个模态类型系统类似于S4模态逻辑，排除低优先级线程延迟高优先级线程，从而静态地防止一组关键的优先级反转错误。然后，我们提出了一个成本模型，允许推理良好类型的程序的响应和完成时间。成本模型扩展了传统的工作跨度模型的合作线程，以考虑到竞争的调度决策，以确保响应。最后，我们证明了我们提出的技术是现实的，通过将它们实现为标准ML语言的扩展。
2018-07-10 cs.PL
RacerF: Lightweight Static Data Race Detection for C Code
本文提出RacerF，一种基于Frama-C平台的轻量级静态分析工具，通过上下近似方法实现线程模块化数据竞争检测，在保证高精度的同时提升检测速度。
2025-06-18 cs.PL cs.SE
Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap
为了使静态程序分析在软件开发人员的指尖，我们提出了一个框架的交互式抽象解释。虽然提供了合理的分析结果，但抽象解释通常可能非常昂贵。为了实现快速的响应时间，我们增加了分析基础设施，包括后处理，而不需要对分析规范本身进行任何修改。我们依赖于本地通用定点引擎TD，它动态跟踪依赖关系，同时探索有助于回答初始查询的未知数。对受程序变化影响的分析结果采用惰性失效方法。专门的改进支持并发缺陷（如数据竞争）的增量分析。该框架已在静态分析器Goblint中为多线程C实现，使用MagpieBridge将发现中继到IDE。我们评估我们的实施w.r.t.响应时间和一致性的标尺：以前证明的不变量应该被保留-当它们不受变化的影响时。结果表明，与我们的方法，小的变化后的重新分析只需要一小部分的从头开始的分析时间，而大部分的精度被保留。我们还提供了程序开发的例子，突出了整体方法的可用性。
2022-11-25 cs.PL
Sound Static Deadlock Analysis for C/Pthreads (Extended Version)
提出了一种C/pthreads静态死锁分析方法。我们的方法的设计一直遵循的要求，分析现实世界的代码。我们的方法是合理的（即，对于那些根据C标准定义了行为的程序来说，它是没有死锁的），并且足够精确，可以证明大量程序的死锁自由。该方法由一个管道的几个分析，建立在一个新的上下文和线程敏感的抽象解释框架。我们进一步提出了一个轻量级的依赖分析，以确定相关的死锁分析，从而加快整体分析的语句。在我们的实验性评估中，我们在不到11小时的时间内成功地证明了Debian GNU/Linux发行版中262个程序的无死锁性，总共使用了2.6兆字节。
2016-07-23 cs.PL
Delay-Bounded Scheduling Without Delay! (Extended Technical Report)
我们认为，在任意线程交织的异步并发程序的安全性分析的广泛问题。延迟有界的确定性调度，介绍了在以前的工作中，是一个有效的错误发现技术，以遏制与充分的调度不确定性的大成本。在本文中，我们首先提出了一种技术，以解除有限域变量程序的情况下的延迟界，从而增加了效率的错误检测的能力，证明安全的程序在任意线程交织。其次，我们展示了如何，结合谓词抽象，我们的技术可以反驳和验证安全属性的程序与无界的变量域，即使是无限的线程数。以前的工作已经建立，对于非平凡的并发例程，谓词抽象诱导一个高度复杂的抽象程序语义。然而，我们的技术，从来没有静态地构造一个抽象的参数化程序，它只需要一些抽象状态集在某些行动下被关闭，从而消除了对存在的抽象程序的验证算法的依赖。我们证明了我们的技术在以前的工作中使用的许多例子的效率，并展示其简单性相比，早期的方法在无限线程票锁协议。
2021-05-15 cs.PL
Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)
National University of Singapore（新加坡国立大学）
本文提出通过摘要驱动的抽象解释方法，结合锁集摘要和线程ID推理，显著提升数据竞争检测的准确性。
2025-11-25 cs.PL cs.SE
Symbolic Reasoning for Automatic Signal Placement (Extended Version)
线程之间的显式信号传递是并发程序中错误的一个长期原因。虽然存在若干运行时技术来在某些共享资源可用时自动通知线程，但是由于它们的运行时开销，这些技术没有被广泛采用。本文提出了一种新的解决方案，基于静态分析自动生成一个显式信号的程序，从其相应的隐式信号的实现。其关键思想是生成验证条件，使我们能够最大限度地减少所需的信号和不必要的上下文切换的数量，同时保证源程序和目标程序之间的语义等价。我们已经实现了我们的方法，在一个名为Experiment的工具，并从以前的论文和开源软件具有挑战性的基准进行评估。expresso生成的代码显著优于过去的自动信号机制（avg. 1.56倍加速），并且与手动优化的显式信号代码的性能非常接近。
2018-04-07 cs.PL
Datalog-based Scalable Semantic Diffing of Concurrent Programs
当修改演进程序以解决与线程同步相关的问题时，需要确认改变是正确的，即，它不会引入意外的行为。然而，手动比较两个程序以识别语义差异是劳动密集型的并且容易出错，而基于模型检验的技术在计算上是昂贵的。为了填补这一空白，我们开发了一种快速的近似静态分析来计算两个程序的同步差异。该方法是快速的，因为它不依赖于重量级模型检验技术，而是利用基于多项式时间数据日志的程序分析框架来计算差分数据流边缘，即，一个程序允许的边缘，而另一个程序不允许。虽然使用近似，我们的方法是足够准确的，由于精心设计的数据流推理规则和迭代增加所需的数据流边缘表示的差异。我们已经实现了我们的方法，并在大量的多线程C程序上对其进行了评估，以确认其通常在几秒钟内产生与人类获得的相同差异的能力;相比之下，基于模型检验的现有技术需要几分钟甚至几小时，因此可能会慢10倍到1000倍。
2018-07-16 cs.PL cs.SE
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
本文提出一种基于幽灵的并发程序正确性见证格式，使交错语义与线程模块化语义下的见证有效性一致，并在SV-COMP基准上验证了其可行性。
2024-11-25 cs.PL
Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities (Extended Version)
Technical University of Munich（慕尼黑工业大学）；National University of Singapore（新加坡国立大学）；University of Tartu（塔尔图大学）
本文提出了一种可灵活调整粒度的固定点引擎并行化方法，通过两种不同哲学实现，提升了静态分析效率。
2026-02-06 cs.DC cs.PL
Fencing off Go: Liveness and Safety for Channel-based Programming (extended version)
Go是一种生产级静态类型的程序设计语言，其设计特点是显式的消息传递原语和轻量级线程，使（并鼓励）程序员能够开发并发系统，其中组件通过通信进行交互，而不是基于锁的共享内存并发。Go语言只能在运行时检测全局死锁，但不能提供编译时保护来防止所有常见的通信不匹配或部分死锁。这项工作开发了一个静态验证框架，在Go程序的活性和安全性，能够检测通信错误和部分死锁在一般类的现实并发程序，包括那些与动态通道创建，无限线程创建和递归。我们的方法从Go程序中推断出其通信模式作为行为类型的忠实表示。通过检查通道使用的语法限制，被称为围栏，我们确保程序是由许多不同的通信模式，可以重复无限多次。这个限制允许我们实现过程来检查类型中的活性和安全性，这反过来又近似于Go程序中的活性和安全性。我们已经在一个工具链中实现了类型推断、活性和安全检查，并在公开的Go程序中进行了测试。注：这是POPL 2017中发表的一篇论文的修订扩展版本，详情请参见第13页。
2017-02-28 cs.LO cs.PL
Static Application-Level Race Detection in STM Haskell using Contracts
编写并发程序是一项艰巨的任务，即使使用高级同步原语（如事务存储器）和具有良好控制副作用的函数式语言（如Haskell），因为进程之间产生的干扰可能发生在不同的级别，并且以非常微妙的方式发生。当线程将共享数据保留或公开为与应用程序逻辑或数据的真实含义不一致的状态时，就会出现问题。在本文中，我们建议将合同与交易相关联，并定义了一个程序转换，使得在STM Haskell的上下文中扩展静态合同检查成为可能。因此，我们能够静态地检查STM Haskell程序的每个事务处理共享数据的方式，即以用户定义的布尔函数的形式表示的给定一致性属性被保留。这确保了在并发程序的执行过程中不会发生不良干扰。
2013-12-10 cs.DC cs.LO cs.PL
