Verified concurrent memory management on modern processors

现代处理器上经过验证的并发内存管理

• 批准号: DP190102167
• 负责人: Prof Antony Hosking
• 金额: $ 33.7万
• 依托单位: The Australian National University
• 依托单位国家: 澳大利亚
• 项目类别: Discovery Projects
• 财政年份: 2019
• 资助国家: 澳大利亚
• 起止时间: 2019-06-14 至 2024-12-31
• 项目状态: 已结题
• 来源: https://dataportal.arc.gov.au/RGS/Web/Grants/DP190102167
• 关键词: Verified; concurrent; memory; management; modern

This project aims to formally verify automatic memory managers in the presence of concurrency and the weakly ordered memory of modern processors. A new framework for verifying memory managers, reusable for a wide range of managed programming languages, target hardware, policies, and algorithms will be developed. Expected technical outcomes include improved techniques to ensure trustworthiness of the foundations on which critical software infrastructures are built. This will significantly enhance the security of public and private cyber assets, and deliver applications that are more robust and trustworthy, across a range of critical infrastructure such as transportation, communication, energy and defence.

这个项目的目的是正式验证自动内存管理器在并发和弱有序内存的现代处理器的存在。将开发一个新的框架，用于验证内存管理器，可重用的管理编程语言，目标硬件，策略和算法。预期的技术成果包括改进技术，以确保建立关键软件基础设施的基础值得信赖。这将大大增强公共和私人网络资产的安全性，并在交通、通信、能源和国防等一系列关键基础设施中提供更强大、更值得信赖的应用程序。