权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

CAREER: Distributed System Synthesis on Certified Middleware

职业：认证中间件上的分布式系统综合

基本信息

批准号：
1942711
负责人：
Mohsen Lesani
金额：
$ 52.38万
依托单位：
University of California-Riverside
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-04-01 至 2025-03-31
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1942711&HistoricalAwards=false
关键词：
CAREER Distributed System Synthesis Certified

项目摘要

Distributed systems are the backbone of modern computing. However, they are complicated and prone to bugs due to their combinatorially large state-spaces, and node and network failures. Recent occurrences of data, currency and service loss have shown that reliability of distributed systems remains elusive. The inherent complication is faced by not only protocol and system designers that provide interfaces but even distributed application programmers that use these interfaces. This project addresses programmer productivity and reliability of distributed systems that spans both the client applications and the supporting distributed middleware. This project includes both novel automatic synthesis techniques for client applications and novel verification techniques for distributed middleware. Distributed stores provide a spectrum of consistency choices that impose a dilemma for clients between correctness, responsiveness and availability. Given the high-level integrity properties of the application, this project automatically decides the minimum required coordination that guarantees integrity and convergence and automatically synthesizes protocols for replicated objects. The reliability of these applications is crucially dependent on the correctness of the underlying middleware of subtle protocols such as broadcast and consensus. The middleware is classically designed as stacks of layers, and its correctness is often stated compositionally as intuitive arguments on temporal precedence of the events exchanged between each layer and its sub-layers. This project builds a development and verification framework in a proof assistant to design a mechanically verified middleware stack. The framework is based on a compositional and temporal program logic so that the proofs match the intuitive arguments.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.

分布式系统是现代计算的支柱。然而，由于其组合的大状态空间以及节点和网络故障，它们很复杂并且容易出现错误。最近发生的数据、货币和服务损失表明，分布式系统的可靠性仍然难以捉摸。不仅是提供接口的协议和系统设计人员，甚至是使用这些接口的分布式应用程序编程人员都面临着固有的复杂性。该项目解决了跨越客户机应用程序和支持分布式中间件的分布式系统的程序员生产力和可靠性问题。该项目包括用于客户端应用程序的新型自动合成技术和用于分布式中间件的新型验证技术。分布式存储提供了一系列一致性选择，使客户机在正确性、响应性和可用性之间陷入两难境地。给定应用程序的高级完整性属性，该项目自动决定保证完整性和收敛所需的最小协调，并自动为复制对象合成协议。这些应用程序的可靠性在很大程度上取决于微妙协议（如广播和共识）的底层中间件的正确性。中间件通常被设计为层堆栈，其正确性通常被组合为每一层及其子层之间交换的事件的时间优先级的直观参数。本项目在证明助手中构建一个开发和验证框架，设计一个机械验证的中间件栈。该框架基于组合和时序程序逻辑，因此证明与直观的论点相匹配。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

期刊论文数量（12）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Hamband: RDMA replicated data types

DOI：
10.1145/3519939.3523426
发表时间：
2022-06
期刊：
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
0
作者：
F. Houshmand;Javad Saberlatibari;M. Lesani
通讯作者：
F. Houshmand;Javad Saberlatibari;M. Lesani

Learning quantitative representation synthesis

学习定量表示综合

DOI：
10.1145/3394450.3397467
发表时间：
2020
期刊：
Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages
影响因子：
0
作者：
Patil, Mayur;Houshmand, Farzin;Lesani, Mohsen
通讯作者：
Lesani, Mohsen

Hampa: Solver-Aided Recency-Aware Replication

DOI：
10.1007/978-3-030-53288-8_16
发表时间：
2020-06-13
期刊：
Computer Aided Verification
影响因子：
0
作者：
Li X;Houshmand F;Lesani M
通讯作者：
Lesani M

Cross-Chain Swaps with Preferences

具有偏好的跨链交换

DOI：
10.1109/csf57540.2023.00031
发表时间：
2023
期刊：
IEEE
影响因子：
0
作者：
Chan, Eric;Chrobak, Marek;Lesani, Mohsen
通讯作者：
Lesani, Mohsen

C4: verified transactional objects

C4：经过验证的交易对象

DOI：
10.1145/3527324
发表时间：
2022
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Lesani, Mohsen;Xia, Li-yao;Kaseorg, Anders;Bell, Christian J.;Chlipala, Adam;Pierce, Benjamin C.;Zdancewic, Steve
通讯作者：
Zdancewic, Steve