Relaxed Memory Model Design for Theory and Practice
理论与实践的松弛记忆模型设计
基本信息
- 批准号:EP/K040561/1
- 负责人:
- 金额:$ 12.56万
- 依托单位:
- 依托单位国家:英国
- 项目类别:Research Grant
- 财政年份:2014
- 资助国家:英国
- 起止时间:2014 至 无数据
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
In the past few years, computer processors have reached a speed limit imposedby semiconductor physics. Before, increased performance came from running asingle program faster, but now it comes from running more programsconcurrently, on multiple "cores". Multi-core processors also supportlow-power applications, and are becoming popular on mobile devices, such assmart phones, where several slow cores use less battery power than a singlefast core. To write software for multi-core processors, programmers mustdecompose tasks into cooperating programs, ideally one per core. However, evenexperts cannot write these programs without tremendous effort, and theprograms often have subtle bugs. Programmers have not been given theintellectual tools necessary for managing the complexity of multi-corecomputation.This project focuses on a critical challenge posed by multi-core processors:their relaxed memory models. Conceptually, the processor's cores are connectedto a single memory, and programs running on different cores communicate bywriting data to the memory for others to read. In reality, the processorachieves good performance by not giving the programmer a globally consistentpicture of the memory: at any point in time the cores can appear to disagreeon its contents. The processor does make some guarantees about the memory, sothat the programmer can write working programs, but it carefully avoids makingothers. A relaxed memory model specifies which guarantees are made and whichare not. Our objectives are to improve the theory of relaxed memory models,and to apply this theory to a new model that is easier to understand inpractice.Most of the time, programming in a high-level language should have advantagesover programming in the processor's low-level assembly language: advantagesin, for example, reliability, security, and cost of development. However, thisis not the case with relaxed memory models: the high-level language is morecomplicated because it has to account for the variety of significantlydifferent processors that the high-level language can be compiled to, and ithas to account for the compiler's optimisations too. The primary tension isbetween usability/security (for example, that sensitive data will not beleaked by a malicious program forging pointers to the data) and efficiency,with the latter driving existing designs. The Java Memory Model attempts togive basic security guarantees, but several underlying flaws have beendiscovered. On the other extreme, the new C and C++ models make no attempt toprovide security guarantees. The design space for relaxed memory models hasnot been thoroughly explored.In this project, we will design a relaxed memory model for a high levellanguage that gives stronger guarantees to programmers, making it easier towrite, reason about, and verify concurrent programs. Our approach to thedesign combines a focus on real-world concurrent algorithms, to ensure that itis practical, with mathematical rigor, to ensure that it supports robustreasoning principles that will ultimately help programmers to understand itand to write high quality concurrent software systems.
在过去的几年里,计算机处理器已经达到了半导体物理学所规定的速度极限。以前,提高性能来自于更快地运行单个程序,但现在它来自于在多个“核心”上并发运行更多程序。多核处理器也支持低功耗应用,并且在移动的设备上越来越流行,比如智能手机,在智能手机上,多个慢核比单个快核使用的电池电量更少。要为多核处理器编写软件,程序员必须将任务分解为协作程序,理想情况下每个核一个。然而,即使是专家也不能不付出巨大的努力就编写这些程序,而且这些程序往往有细微的错误。程序员还没有得到管理多核计算复杂性所必需的智能工具。这个项目关注多核处理器带来的一个关键挑战:它们宽松的内存模型。从概念上讲,处理器的核心连接到单个内存,在不同核心上运行的程序通过将数据写入内存供其他人读取来进行通信。实际上,处理器通过不向程序员提供全局一致的内存图片来实现良好的性能:在任何时间点,内核都可能出现对其内容的不一致。处理器确实对存储器作了一些保证,以便程序员能写出工作程序,但它小心地避免作其他保证。一个宽松的记忆模型规定了哪些保证被做出,哪些不被做出。我们的目标是改进松弛内存模型的理论,并将这一理论应用到一个更容易理解的新模型中。在大多数情况下,用高级语言编程应该比用处理器的低级汇编语言编程更好:例如,在可靠性、安全性和开发成本方面。然而,这并不是宽松内存模型的情况:高级语言更复杂,因为它必须考虑到高级语言可以编译到的各种不同的处理器,并且还要考虑编译器的优化。主要的紧张关系是可用性/安全性(例如,敏感数据不会被伪造数据指针的恶意程序泄露)和效率之间的关系,后者推动了现有的设计。Java内存模型试图提供基本的安全保证,但也发现了一些潜在的缺陷。在另一个极端,新的C和C++模型没有尝试提供安全保证。在这个项目中,我们将为高级语言设计一个宽松的内存模型,为程序员提供更强的保证,使并发程序的编写、推理和验证变得更容易。我们的设计方法结合了对现实世界的并发算法的关注,以确保它的实用性,与数学严谨性,以确保它支持鲁棒的推理原则,这将最终帮助程序员理解它,并编写高质量的并发软件系统。
项目成果
期刊论文数量(6)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Benchmarking weak memory models
- DOI:10.1145/2851141.2851150
- 发表时间:2016-02
- 期刊:
- 影响因子:0
- 作者:Carl G. Ritson;Scott Owens
- 通讯作者:Carl G. Ritson;Scott Owens
A new verified compiler backend for CakeML
CakeML 的新的经过验证的编译器后端
- DOI:10.1145/2951913.2951924
- 发表时间:2016
- 期刊:
- 影响因子:0
- 作者:Tan Y
- 通讯作者:Tan Y
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Scott Owens其他文献
Cakes That Bake Cakes: Dynamic Computation in CakeML
烘焙蛋糕的蛋糕:CakeML 中的动态计算
- DOI:
10.1145/3591266 - 发表时间:
2023 - 期刊:
- 影响因子:0
- 作者:
Thomas Sewell;Magnus O. Myreen;Yong Kiam Tan;Ramana Kumar;Alexander Mihajlovic;Oskar Abrahamsson;Scott Owens - 通讯作者:
Scott Owens
A verified type system for CakeML
CakeML 的经过验证的类型系统
- DOI:
- 发表时间:
2015 - 期刊:
- 影响因子:0
- 作者:
Yong Kiam Tan;Scott Owens;Ramana Kumar - 通讯作者:
Ramana Kumar
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
高阶逻辑子集的证明生成编译器的结构
- DOI:
- 发表时间:
2007 - 期刊:
- 影响因子:0
- 作者:
Guodong Li;Scott Owens;Konrad Slind - 通讯作者:
Konrad Slind
Lem
莱姆
- DOI:
10.1145/2692915.2628143 - 发表时间:
2014 - 期刊:
- 影响因子:0
- 作者:
Dominic P. Mulligan;Scott Owens;Kathryn E. Gray;T. Ridge;Peter Sewell - 通讯作者:
Peter Sewell
A Better x86 Memory Model: x86-TSO (Extended Version)
更好的 x86 内存模型:x86-TSO(扩展版本)
- DOI:
- 发表时间:
2009 - 期刊:
- 影响因子:0
- 作者:
Scott Owens;Susmit Sarkar;Peter Sewell - 通讯作者:
Peter Sewell
Scott Owens的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Scott Owens', 18)}}的其他基金
Verifiably Correct Transactional Memory
可验证正确的事务内存
- 批准号:
EP/R032971/1 - 财政年份:2018
- 资助金额:
$ 12.56万 - 项目类别:
Research Grant
Verifying concurrent algorithms on Weak Memory Models
验证弱内存模型上的并发算法
- 批准号:
EP/M017176/1 - 财政年份:2015
- 资助金额:
$ 12.56万 - 项目类别:
Research Grant
相似国自然基金
CREB在杏仁核神经环路memory allocation中的作用和机制研究
- 批准号:31171079
- 批准年份:2011
- 资助金额:55.0 万元
- 项目类别:面上项目
面向多核处理器的硬软件协作Transactional Memory系统结构
- 批准号:60873053
- 批准年份:2008
- 资助金额:30.0 万元
- 项目类别:面上项目
相似海外基金
A Nonhuman Primate Model for Postoperative Delirium and Working Memory Impairment
术后谵妄和工作记忆损伤的非人类灵长类动物模型
- 批准号:
10592515 - 财政年份:2023
- 资助金额:
$ 12.56万 - 项目类别:
Combined mild intensity exercise and dietary astaxanthin effects on memory function in Alzheimer`s mouse model: the role of leptin signaling in adult hippocampal neurogenesis and neuroinflammation
轻度强度运动和膳食虾青素联合对阿尔茨海默病小鼠模型记忆功能的影响:瘦素信号在成年海马神经发生和神经炎症中的作用
- 批准号:
23K16717 - 财政年份:2023
- 资助金额:
$ 12.56万 - 项目类别:
Grant-in-Aid for Early-Career Scientists
Memory and Recognition Integration Model Inspired by Hippocampus and Cerebral Cortex
受海马体和大脑皮层启发的记忆和识别整合模型
- 批准号:
23K11247 - 财政年份:2023
- 资助金额:
$ 12.56万 - 项目类别:
Grant-in-Aid for Scientific Research (C)
A physics-driven neural network model of working memory
物理驱动的工作记忆神经网络模型
- 批准号:
570263-2022 - 财政年份:2022
- 资助金额:
$ 12.56万 - 项目类别:
Alexander Graham Bell Canada Graduate Scholarships - Doctoral
Circuit mechanisms underlying associative memory impairment in knock-in Alzheimer's model
敲入阿尔茨海默病模型中联想记忆损伤的回路机制
- 批准号:
10538464 - 财政年份:2022
- 资助金额:
$ 12.56万 - 项目类别:
From episodic memory to functioning in schizophrenia and related psychoses: A neurocognitive model
从情景记忆到精神分裂症和相关精神病的功能:神经认知模型
- 批准号:
462727 - 财政年份:2022
- 资助金额:
$ 12.56万 - 项目类别:
Operating Grants
Spatial Capture-recapture with Memory: A New Hidden Markov Model Perspective
空间捕捉-用记忆重新捕捉:新的隐马尔可夫模型视角
- 批准号:
EP/W002248/1 - 财政年份:2022
- 资助金额:
$ 12.56万 - 项目类别:
Research Grant
Towards a computational model of distributed memory
走向分布式内存的计算模型
- 批准号:
546979-2020 - 财政年份:2022
- 资助金额:
$ 12.56万 - 项目类别:
Alexander Graham Bell Canada Graduate Scholarships - Doctoral
"Establishment of a long short-term memory (LSTM) model using the Hilbert-Huang transform (HHT) to forecast the current outputs of biophotovoltaic dev
“使用希尔伯特-黄变换(HHT)建立长短期记忆(LSTM)模型来预测生物光伏开发的当前输出
- 批准号:
2801696 - 财政年份:2022
- 资助金额:
$ 12.56万 - 项目类别:
Studentship
Circuit mechanisms underlying associative memory impairment in knock-in Alzheimer's model
敲入阿尔茨海默病模型中联想记忆损伤的回路机制
- 批准号:
10689059 - 财政年份:2022
- 资助金额:
$ 12.56万 - 项目类别: