SHF: Small: Programming, and Reasoning about, Actors that Share State

SHF：小：共享状态的参与者的编程和推理

• 批准号: 2315884
• 负责人: Matthias Felleisen
• 金额: $ 54万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2026-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2315884&HistoricalAwards=false
• 关键词: SHF; Small; Programming; Reasoning; about

Many software applications consist of many components that must compute in parallel and independently of each other and yet must coordinate their activities to achieve the overarching goal. Developers refer to this scenario as concurrent programming, and they consider the creation of concurrent software as one of the most difficult problems around. The investigator and his team are studying a novel solution to this problem. Their approach is to think of concurrent software systems as a collection of conversing actors. Like in real conversations, these actors exchange words and refer back to the context of ideas that a conversation has established so far. The investigator's key insight is to create a special purpose notation for programming these two aspects of conversations explicitly. Preliminary investigations show that this notation greatly facilitates programming concurrent systems and thinking about their coordination efforts. The project will directly impact the evolution of future programming languages and indirectly affect the lives of working programmers.Technically, the project injects two entirely new ideas into the so-called actor model of computation. The first is an explicitly managed space of shared assertions. Using this space, actors can establish a common state, modify it in a controlled manner, and get informed when changes happen. When an actor crashes, its portion of the shared state is automatically withdrawn, making it possible to easily cope with failures and thus making the system resilient. The second idea is a language for programming actor interactions, including message sending and state sharing. While this new language restricts how actors interact and what they interact about, it will enable language designers to provide type systems and model checkers that statically enforce adherence to protocols and verify that the concurrent software system will achieve its specified goals.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

许多软件应用程序由许多组件组成，这些组件必须并行且彼此独立地计算，但必须协调它们的活动以实现总体目标。开发人员将这种情况称为并发编程，他们认为并发软件的创建是最困难的问题之一。研究人员和他的团队正在研究解决这个问题的新方法。他们的方法是将并发软件系统视为对话参与者的集合。就像在真实的对话中一样，这些参与者交换言语并参考对话迄今为止建立的想法背景。调查员的主要见解是创建一个特殊目的符号来明确编程对话的这两个方面。初步调查表明，这种表示法极大地方便了并发系统的编程和思考它们的协调工作。该项目将直接影响未来编程语言的演变，并间接影响工作程序员的生活。从技术上讲，该项目为所谓的计算参与者模型注入了两个全新的想法。第一个是共享断言的显式管理空间。使用这个空间，参与者可以建立一个公共状态，以受控的方式修改它，并在发生变化时得到通知。当一个actor崩溃时，它的共享状态部分会自动撤回，从而可以轻松应对故障，从而使系统具有弹性。第二个想法是一种用于对参与者交互进行编程的语言，包括消息发送和状态共享。虽然这种新语言限制了参与者的交互方式和交互内容，但它将使语言设计者能够提供类型系统和模型检查器，静态地强制遵守协议并验证并发软件系统将实现其指定的目标。该奖项反映了 NSF 的法定目标使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。