Efficient and Deterministic Record & Replay for Actor Languages
随着并行商用硬件的普及，开发人员转向高级并发模型，如演员模型，以降低并发软件的复杂性。然而，调试并发软件是困难的，特别是对于支持工具集有限的并发模型。这类工具通常只处理底层线程和锁，这是在错误的抽象级别上，甚至可能引入额外的复杂性。为了改善这种情况，我们提出了一个低开销的记录和重放方法的演员语言。它允许根据先前记录的跟踪确定性地调试并发问题。我们的评估表明，在Savina套件的基准测试上进行跟踪的平均运行时开销为10%（最小为0%，最大为10%）。20%）。对于现代Web应用程序Acme-Air，我们看到HTTP请求的延迟最多增加了1%，跟踪数据增加了约1.4 MB/s。这些结果是确定性重放调试的演员系统在生产中的第一步。
2018-08-20 cs.PL
Bestow and Atomic: Concurrent Programming using Isolation, Delegation and Grouping
任何非平凡的并发系统都保证同步，而不管并发模型如何。基于Actor的并发性通过异步消息传递将Actor中的所有计算序列化。相比之下，基于锁的并发通过遵循锁-解锁协议访问某些数据来串行化某些计算。这两个系统都需要对指针和别名进行合理的推理，以排除数据竞争。如果参与者隔离被破坏，那么单线程控制抽象也会被破坏。同样，对于锁，如果可以在锁的作用域之外访问数据，则该数据不受锁的控制。在本文中，我们将讨论如何平衡混叠和同步。在前面的工作中，我们定义了一个类型系统，它保证了基于参与者的并发和基于锁的并发的数据竞争自由。本文通过引入两个编程结构来扩展这项工作;一个用于解耦隔离和同步，另一个用于从较低级别的同步构建更高级别的原子性保证。我们主要关注参与者，特别是Encore程序设计语言，但我们的最终目标是以这样一种方式定义我们的构造，即它们可以与锁和参与者一起使用，因为这两种模型的组合在实际系统中经常发生。我们讨论了设计空间，提供了几种不同的语义形式化，并讨论了它们的属性，并将它们连接到案例研究中，展示了我们提出的构造是如何有用的。我们还报告了一个正在进行的实施，我们提出的结构在安可。
2018-07-26 cs.PL
Fearless Concurrency? Understanding Concurrent Programming Safety in Real-World Rust Software
Rust是近年来在构建各种底层软件时流行的程序设计语言。它旨在通过一套编译器检查规则在实现多线程软件时提供安全并发。不幸的是，人们对检查规则如何影响Rust应用程序中并发编程的安全性的理解有限。本文从并发使用和并发缺陷两个方面对Rust的并发安全性进行了初步研究。我们的研究可以更好地理解Rust的并发性，并可以指导未来的研究人员和从业者编写更好，更可靠的Rust软件，并为Rust开发调试和错误检测工具。
2019-02-05 cs.PL
Automatic Verification of Erlang-Style Concurrency
提出了一种自动验证Erlang式高阶并发程序安全性的方法。受Core Erlang的启发，我们引入了Lambda-Actor，这是一种具有模式匹配代数数据类型的原型函数式语言，并增加了进程创建和异步消息传递原语。我们正式的抽象模型的λ-演员程序称为演员通信系统（ACS），它有一个自然的解释为一个矢量加法系统，其中一些验证问题是可判定的。我们给出了一个参数化的抽象解释框架，并使用它来构建一个多时间可计算的，基于流的，抽象语义的Lambda-Actor程序，然后我们使用它来引导ACS的建设，从而得出一个更准确的输入程序的抽象模型。我们已经构建了Soter，一个验证方法的工具实现，从而获得了第一个全自动的，无限状态的Erlang核心片段的模型检查器。我们发现，在实践中，我们的抽象技术是准确的，足以验证一个有趣的范围内的安全属性。虽然ACS的可覆盖性问题是Expspace完备的，但Soter可以非常有效地分析这些验证问题。
2013-03-09 cs.PL
HIPPODROME: Data Race Repair using Static Analysis Summaries
实现无错误的并发程序是现代软件开发中的一项具有挑战性的任务。最先进的静态分析在生产代码中发现了数百个并发错误，可以扩展到大型代码库。然而，在不断变化的代码库中修复这些错误对程序员来说是一项艰巨的工作，特别是因为并发代码中的修复可能会以微妙的方式引入其他错误。在这项工作中，我们将展示如何利用组合静态分析的并发错误检测，使一个新的自动程序修复（APR）技术的数据竞赛在大型并发Java代码库。我们的工作的关键创新是一个算法，翻译的分析工具推断的程序摘要的错误报告的目的，到小的本地补丁，修复并发错误（不引入新的）。这种协同作用使得将组合静态并发分析的优点扩展到APR成为可能，使我们的方法有效（它可以检测和修复比现有工具更多的错误），可扩展（它需要几秒钟来分析和建议修复相当大的代码库），并且可用（通常，它不需要用户的注释，并且可以执行连续的自动修复）。我们对流行的开源项目进行的研究证实，我们的工具自动生成类似于开发人员过去提出的并发修复。
2021-08-06 cs.PL cs.SE
ActorScript(TM) extension of C sharp (TM), Java(TM), and Objective C(TM): iAdaptive(TM) concurrency for antiCloud(TM) privacy and security
ActorScript（TM）是一种通用程序设计语言，用于实现管理资源和需求的自主、自适应并发。它与以前的语言的区别在于：-通用性 * 指定Actor可以做什么的能力 * 指定硬件和软件之间的接口 * 语言中的一切都是使用消息传递完成的，包括ActorScript本身的定义 * 集成了函数式，命令式，逻辑和并发编程。* 并发动态适应可用资源和当前负载。* 程序不暴露低级别的实现机制，如线程，任务，锁，核心等。* 消息可以直接通信，而无需通过代理，通道，类层次结构，邮箱，管道，端口，队列等间接。* 消除了变量竞争。* 二进制XML和JSON是数据类型。* 提供了应用程序二进制接口，因此在运行时不需要查找标识符符号。- 安全和安全 * 程序是扩展不变的，即，扩展一个程序并不改变它的意义。* 应用程序不能直接相互伤害。- 性能 * 对Actor系统的实现不施加任何开销 * 消息传递的开销与过程调用和循环的开销基本相同。* 允许根据系统负载和容量（例如核心）动态调整执行 * 局部性，因为执行不受顺序全局内存模型的约束 * 固有并发性，因为执行不受通信顺序进程的约束 * 最大限度地减少关键路线上的延迟
2015-03-04 cs.DC cs.PL
libcppa - Designing an Actor Semantic for C++11
并行硬件使得并发性对于高效的程序执行是强制性的。然而，编写并发软件既具有挑战性又容易出错。C++11为多道程序设计提供了标准的工具，例如带有获取/释放语义的原子操作和RAII互斥锁，但这些原语仍然太低级。正确有效地使用它们仍然需要专业知识和手工制作。参与者模型通过使用显式消息传递机制共享来取代隐式通信。它适用于并发和分布，并且在适当的预确定尺寸的线程池中调度所有参与者的轻量级参与者模型实现可以优于等效的基于线程的应用程序。然而，演员模型没有进入本机程序设计语言的领域，除了供应商特定的岛屿解决方案。通过开源库libcppa，我们希望将Actor模型提供的构建可靠分布式系统的能力与C++11的性能和资源效率相结合。
2013-01-04 cs.PL
RaceFixer -- An Automated Data Race Fixer
提出自动化修复单变量原子性违规并发缺陷的工具 RaceFixer，结合 ThreadSanitizer 报告与静态分析生成并合并补丁，提升修复质量、性能与代码可读性。
2024-01-08 cs.PL cs.SE
Capturing High-level Nondeterminism in Concurrent Programs for Practical Concurrency Model Agnostic Record & Replay
由于并发是大多数软件系统不可或缺的一部分，开发人员在同一应用程序中组合高级并发模型，以通过适当的抽象来解决每个问题。虽然语言和库提供了广泛的并发模型，但对结合它们的应用程序的调试支持还没有得到太多的关注。Record & replay通过确定性地重现记录的bug来帮助调试，但通常仅针对单个并发模型设计。本文提出了一种实用的并发模型无关的记录和重放方法的多范式并发程序，即结合并发模型的应用程序。我们的方法跟踪高层次的不确定性事件，使用统一的模型无关的跟踪格式和基础设施。这使得基于排序的记录和重放支持范围广泛的并发模型，从而使调试的应用程序，结合他们。此外，它允许语言实现者添加新的并发模型，并重用与模型无关的记录和重放支持。我们认为，一个并发模型不可知的记录和重放是实用的，使先进的调试支持范围广泛的并发模型。评估表明，我们的方法是表达和灵活的，足以支持记录和重放的应用程序使用线程和锁，通信事件循环，通信顺序进程，软件事务存储器和这些并发模型的组合。对于演员模型，我们通过优化的专用录制和回放解决方案达到了具有竞争力的录制性能。Savina actor基准测试套件的平均录制开销为10%（最小0%，最大10%）。23%）。其他并发模型及其组合的性能处于类似水平。我们相信我们的并发模型无关的方法可以帮助开发人员混合和匹配并发模型的应用程序。我们希望这个基础激发新的工具和语言，使多范式并发应用程…
2021-02-26 cs.PL
NVLang: Unified Static Typing for Actor-Based Concurrency on the BEAM
University of Lisbon（里斯本大学）
NVLang通过统一静态类型为BEAM上的演员并发提供类型安全，利用代数数据类型自然编码消息协议，确保编译时协议符合性。
2025-12-04 cs.DC cs.PL
Conversational Concurrency with Dataspaces and Facets
针对纯消息传递模型难以处理会话上下文和并行子对话的问题，本文提出语言Syndicate，通过数据空间共享上下文和切面组织参与者，减少复杂设计模式，支持健壮的并发应用。
2025-02-27 cs.PL
Modelling Concurrency Bugs Using Machine Learning
Imperial College of Science, Technology and Medicine（帝国理工学院）；Massachusetts Institute of Technology（麻省理工学院）
本研究比较常见与最新的机器学习方法，利用合成数据集模拟并发程序，验证模型类型的基本限制，以支持自动检测并发缺陷并提升工具准确性与语言灵活性。
2023-05-08 cs.LG cs.PL cs.SE
Actor Model of Computation: Scalable Robust Information Systems
Actor模型是一种数学理论，它将“Actor”视为并发数字计算的通用原语。该模型已被用来作为一个框架的理论理解的并发性，并作为理论基础的并发系统的几个实际实现。与以前的计算模型不同，Actor模型受到物理定律的启发。它还受到了程序设计语言Lisp、Simula 67和Smalltalk-72的影响，以及Petri网、基于能力的系统和分组交换的思想。通过客户端云计算和众核计算机体系结构的大规模并发的出现激发了对Actor模型的兴趣。Actor技术将在整合个人、团体和组织的各种数字信息方面得到重要应用，以便他们的信息有效地链接在一起。信息集成需要利用以下信息系统原则：* 持久性。信息被收集并编入索引。* 并发：工作以交互方式并发进行，在时间上重叠。* 准交换性：信息可以被使用，无论它是启动新的工作还是与正在进行的工作相关。* 赞助：赞助者提供计算资源，即，处理、存储和通信。* 多元化：信息是异质的，重叠的，往往不一致。* 出处：Actor模型旨在为不一致鲁棒信息集成提供基础
2015-01-21 cs.DC cs.PL
A Concurrency-Agnostic Protocol for Multi-Paradigm Concurrent Debugging Tools
当今复杂的软件系统结合了高级并发模型。每个模型用于解决一组特定的问题。不幸的是，调试器只支持线程和共享内存的低级概念，迫使开发人员对这些概念进行推理，而不是他们选择的高级并发模型。本文提出了一个并发无关的调试器协议，从目标应用程序所采用的并发模型的调试器。因此，基础语言运行库可以为它支持的每个并发模型定义自定义断点、单步执行操作和执行事件，调试器可以公开它们，而不必专门进行调整。我们评估了协议的通用性，将其应用到SOMns，一个新的实现，它支持多种并发模型，包括通信顺序进程，通信事件循环，线程和锁，fork/join并行，和软件事务内存。我们为这些并发模型实现了21个断点和20个步进操作。对于所有这些，调试器都不需要更改。此外，我们可视化所有并发交互独立于一个特定的并发模型。为了展示特定并发模型的工具是可能的，我们将角色轮换和消息发送分别可视化。
2017-10-29 cs.PL
Compiler Testing With Relaxed Memory Models
针对现有并发编译器测试技术无法兼顾边界内漏洞覆盖与大规模程序可扩展性的问题，提出工业级测试工具Téléchat，通过对比源与架构内存模型下的程序行为发现漏洞，性能优于现有技术且已部署应用。
2024-01-29 cs.AR cs.PL cs.SE
Behavioural Types for Actor Systems
最近的主流程序设计语言（如Erlang或Scala）重新引起了对并发Actor模型的兴趣。然而，对角色系统进行静态分析的文献还缺乏成熟的形式化方法。在本文中，我们提出了一个最小的演员演算，作为原始的Scala的演员API的基本结构。更准确地说，参与者可以发送异步消息，根据模式匹配机制处理接收到的消息，并动态创建新的参与者，可以通过将参与者名称作为消息参数传递来扩展新参与者的作用域。从针对过程演算开发的线性类型和会话类型论中汲取灵感，我们提出了一个行为类型系统，解决了参与者演算的关键问题。然后，我们研究了有限行动者通信的确定性处理的安全性质。更准确地说，我们表明，良好的类型和平衡的演员系统是（i）无死锁和（ii）任何消息最终将由目标演员处理，双重没有演员将无限期地等待预期的消息
2012-06-08 cs.PL
High-Performance Deterministic Concurrency using Lingua Franca
Actor框架和类似的反应式编程技术被广泛用于构建并发系统。它们承诺是高效的，并且可以很好地扩展到分布式系统中的大量核心或节点。然而，它们也使程序员暴露于不确定性，这通常使实现难以理解、调试和测试。最近提出的反应器模型是一个很有前途的替代方案，使高效的确定性并发。在本文中，我们表明，确定性并不意味着损失的表现力，也没有在性能。为了表明这一点，我们评估的通用语言（LF），面向反应器的协调语言，配备主流程序设计语言的并发模型，自动利用机会，利用并行不引入非确定性。我们对Savina基准测试套件的实现表明，在执行时间方面，LF程序的运行时性能甚至超过了流行的高度优化的Actor框架。我们与Akka和CAF进行了比较，LF的表现分别为1.86倍和1.42倍。
2023-01-09 cs.DC cs.PF cs.PL
Conversational Concurrency
本文提出以会话式知识交换为核心的并发编程模型，通过公共数据空间与新型 actor 结构构造形成 Syndicate，并以数学模型、两种语言实现及证据验证其可简化并发编程。
2024-09-06 cs.PL
Towards Composable Concurrency Abstractions
在过去的几十年中，已经提出了许多不同的编程模型来管理应用程序中的并发性，例如Actor模型，通信顺序进程和软件事务存储器。多核处理器的普及使得利用并发变得更加重要。我们观察到，现代语言，如Scala、Clojure或F#，提供的不是一个，而是多个并发模型，帮助开发人员管理并发。大型最终用户应用程序很少只使用单一并发模型构建。程序员需要管理响应式UI、处理文件或网络I/O、异步工作流和共享资源。不同的并发模型支持不同的需求。这就提出了这些并发模型如何交互以及它们是否可组合的问题。毕竟，组合不同的并发模型可能会导致微妙的错误或不一致。在本文中，我们对Clojure语言提供的并发抽象进行了深入的研究。我们研究所有的成对组合的抽象，注意哪些组成没有问题，哪些没有。我们试图从Clojure的细节中抽象出来，识别并发模型的一般属性，这些属性促进或阻碍了组合。
2014-06-13 cs.DC cs.PL cs.SE
LitmusKt: Concurrency Stress Testing for Kotlin
LitmusKt 是首个用于 Kotlin 并发程序的 litmus 测试工具，支持多平台测试，发现并修复了编译器错误，已集成到 CI 流水线。
2025-04-22 cs.PL cs.SE
Two-Phase Dynamic Analysis of Message-Passing Go Programs based on Vector Clocks
理解并发程序的运行时行为是一项具有挑战性的任务。一种流行的方法是通过矢量时钟建立一个发生在之前的关系。因此，我们可以识别错误和性能瓶颈，例如，通过检查两个冲突事件是否可能并发发生。我们采用两阶段的方法来获得向量时钟信息，用于广泛的并发功能，包括Go中的所有消息传递功能。第一阶段（插装和跟踪）生成一个运行时跟踪，记录发生的与消息传递并发相关的所有事件。第二阶段（轨迹重放）在线执行，并重放记录的轨迹以推断矢量时钟信息。跟踪重放对线程本地跟踪进行操作。因此，我们可以观察到可能由某种替代时间表导致的不确定性。我们的方法不依赖于任何特定的语言。我们已经为Go程序设计语言构建了一个原型，并为我们的方法的实用性提供了经验证据。
2018-07-20 cs.PL
Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
Go是一种流行的并发程序设计语言，这要归功于它能够有效地结合并发和系统编程。在Go程序中，许多并发错误可能是由数据竞争和通信问题引起的。在本文中，我们开发了一种基于行为类型的理论来静态检测Go程序中的数据竞争和死锁。我们首先使用Go内存模型中定义的happens-before关系，在Go程序模型上指定锁安全性、活动性和数据竞争属性。我们表示这些属性的程序中的$μ$演算模型的类型，并验证它们使用类型级别的模型检查。然后，我们扩展了框架，以考虑Go的通道，并实现了一个静态验证工具，可以检测并发错误。据我们所知，这是Go语言的第一个此类静态验证框架，统一分析了由共享内存访问和异步消息传递通信混合引起的并发错误。
2021-11-18 cs.LO cs.PL
Parallelism, Concurrency and Distribution in Constraint Handling Rules: A Survey
约束处理规则是一种有效的并发声明式程序设计语言，也是一种通用的计算逻辑形式。可编程逻辑程序由转换多组约束的保护反应规则组成。XML的主要特性之一是其固有的并发性。直观地说，规则可以并行地应用于多重集的各个部分。在这个全面的调查中，我们给出了并发和并行以及分布式语义的概述，标准的和更奇特的，多年来已经提出了在不同层次的细化。这些语义的范围从抽象到具体。它们是由正式的健全性结果。它们的正确性建立在并行计算和顺序计算之间的对应关系上。我们提出了共同的简洁的示例编程，已被广泛用于实验和基准测试。我们审查并行可编程逻辑器件在软件和硬件中的实现。实验结果表明，一致的并行加速比。大多数实现都可以在线获得。并行形式主义也可以用来实现和推理并发模型。为此，软件事务模型，Actor模型，有色Petri网和Join-Calculus已经忠实地编码在CHR中。在逻辑编程理论与实践（TPLP）中考虑。
2018-04-06 cs.DC cs.PL
Actor Capabilities for Message Ordering (Extended Version)
本文提出actor capabilities（Actor能力），通过为Actor引用配备协议限制消息发送的类型与顺序，并在基础类型系统上分层构建效应系统，确保Actor行为能处理任何到达的消息，为更强推理奠定基础。
2025-09-13 cs.DC cs.PL
Slicing Concurrent Constraint Programs
并发约束编程（CCP）是一个声明式的并发模型，其中代理通过告诉和询问共享存储中的约束（信息片段）进行交互。以前的一些作品已经开发了（近似）CCP语言的声明式调试器。然而，调试并发程序的任务仍然很困难。在本文中，我们定义了一个动态切片CCP，我们表明它是一个有用的伴侣工具，现有的调试技术。我们的技术首先考虑一个部分计算（跟踪），显示存在的错误。通常，这种跟踪中的信息量是压倒性的，用户很容易迷失方向，因为她不能专注于bug的来源。我们的切片器允许标记计算状态的一部分，并帮助用户消除大部分冗余信息，以突出错误。我们表明，这种技术可以定制CCP的定时变量。我们还开发了一个原型实现免费提供实验。
2017-02-10 cs.LO cs.PL
Towards Bug-Free Distributed Go Programs
本文针对 Go 分布式程序中的通信竞争问题，提出基于扩展至有缓冲与无缓冲通道的 happens-before 顺序的静态验证框架，以证明程序不存在通信竞争。
2025-07-25 cs.LO cs.PL cs.SE
DR.FIX: Automatically Fixing Data Races at Industry Scale
Uber Technologies（Uber技术公司）；Aarhus University（奥胡斯大学）
本文提出Dr.Fix工具，结合大语言模型与程序分析，在工业规模下自动修复Go语言数据竞争，经Uber实践验证，在404个竞争案例中成功生成224个补丁，其中86%被开发者接受。
2025-04-22 cs.AI cs.DC cs.LG
